-
Notifications
You must be signed in to change notification settings - Fork 276
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
[Verif] Introduce a clocked assertion verif.clocked_assert
#6982
Comments
verif.clocked_assert
verif.clocked_assert
You'd probably want to flip the canonicalization around: canonicalize |
I assume the |
That's an excellent point. I like the idea of having |
The current structure of the
verif
dialect requires the use ofltl.clock
to associate a clock to an assertion (which is required). This means that a use-def analysis is required everytime we want to work withverif.assert
, which leads to thesv.assert
operation being used in most lowerings to Core dialects.As suggested by @fabianschuiki , I propose that we add a
verif.clocked_assert(clock, prop)
that would be the canonicalization ofverif.assert(ltl.clock(clock, prop))
. This would make it easier to use move away fromsv
dialect ops in the core representations.The text was updated successfully, but these errors were encountered: