Skip to content

world-level BMC: implement two empty match rules #1167

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 4 commits into
base: main
Choose a base branch
from

Conversation

kroening
Copy link
Member

This implements two SVA empty match rules in the word-level BMC encoding.

kroening added 4 commits June 19, 2025 14:44
This adds a PRECONDITION on the starting timeframe to the word-level SVA
sequence encoding.
This adds parentheses around the arguments of SVA ## to avoid ambiguity.
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.
This implements two SVA empty match rules in the word-level BMC encoding.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant