[Verif] Make verif.formal parameters an ODS property #7867
Conversation
Instead of using the discardable attributes dictionary of `verif.formal` as vessel for user-defined test parameters, add a dedicated `parameters` field to the op itself. This makes the parameters non-discardable and a proper part of the test.
| @@ -295,7 +295,7 @@ def FormalOp : VerifOp<"formal", [ | |||
|
|
|||
| ### Example | |||
There was a problem hiding this comment.
A short paragraph in the documentation describing what parameters mean for frontends and for backends would be great. E.g., what kind of parameters can a frontend add and what can it expect/what guarantees does it have? What do backends need to do with the parameters? Can they just ignore them at will?
There was a problem hiding this comment.
😁 Yeah we'll definitely need more details in the documentation. The problem right now is that we don't know yet which parameters are relevant or used. I expect us to figure this out as we build out the runners and the circt-test tool. For example, it looks like a "mode" and "bound" parameter makes sense for formal tests. But maybe also not really. My reflex here was to leave this out until we actually know which parameters are guaranteed to be understood by the runners, instead of promising something up front that then doesn't happen. 😬
Instead of using the discardable attributes dictionary of
verif.formalas vessel for user-defined test parameters, add a dedicatedparametersfield to the op itself. This makes the parameters non-discardable and a proper part of the test.