Skip to content

SVA: replace sva_sequence_concatenation_exprt #1162

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

kroening
Copy link
Member

This replaces the sva_sequence_concatenation_exprt by multi-operand variants of sva_cycle_delay_exprt, sva_cycle_delay_plus_exprt and sva_cycle_delay_star_exprt.

This simplifies the implementation of the SystemVerilog concatenation rules.

@kroening kroening force-pushed the remove-sva-sequence-concatenation branch 2 times, most recently from 72d9130 to 2436062 Compare June 19, 2025 01:27
This adds a PRECONDITION on the starting timeframe to the word-level SVA
sequence encoding.
@kroening kroening force-pushed the remove-sva-sequence-concatenation branch from 2436062 to a86335d Compare June 19, 2025 06:00
This adds parentheses around the arguments of SVA ## to avoid ambiguity.
@kroening kroening force-pushed the remove-sva-sequence-concatenation branch 2 times, most recently from 4a79fd5 to 8544473 Compare June 19, 2025 09:33
This replaces the sva_sequence_concatenation_exprt by multi-operand variants
of sva_cycle_delay_exprt, sva_cycle_delay_plus_exprt and
sva_cycle_delay_star_exprt.

This simplifies the implementation of the SystemVerilog concatenation rules.
@kroening kroening force-pushed the remove-sva-sequence-concatenation branch from 8544473 to cfe36b1 Compare June 19, 2025 09:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant