circt
circt copied to clipboard
[WIP][Verif]Add formal test intent ops
[WIP] The goal of this PR is to introduce a first round of new test intent operations, for formal tests this time, to the verif dialect following this proposal document.
This first PR will start by simply adding the ops with some verifier tests. Future PRs on this will have to then add a PrepareForFormal pass, and make sure that only verif.formal ops are used for formal verification and ignored elsewhere.
The ops that will be added in this PR are:
- [x]
verif.formal - [x]
verif.symbolic_val - [x]
verif.concrete_val
Feel free to let me know what you think!