[Verif] Add formal test intent ops #7145
Conversation
… dev/dobios/new-verif-ops
dobios
changed the title
| let description = [{ | ||
| This operation declares a symbolic input that can then be used to reason | ||
| about `hw.instance` inputs in a symbolic manner in future assertions and | ||
| assumptions. The result type must be explicitly marked. |
There was a problem hiding this comment.
Is this really specific to hw.instance or could it be any instance or a fully inlined design without and instance operation in the verif.formal?
It's probably a good idea to describe a bit more precisely how this symbolic value behaves over time. Is it fixed over all clock cycles, can it change at a clock edge, can it change at any time?
There was a problem hiding this comment.
It's probably a good idea to describe a bit more precisely how this symbolic value behaves over time. Is it fixed over all clock cycles, can it change at a clock edge, can it change at any time?
Agreed. Guessing from when we spoke about it before that it can only change on a clock-edge - we might want to add another op for a value that's fixed over all cycles (e.g. for defining BMC inputs while making sure we're adhering to the right semantics but not having to create a new BV every cycle when it's not necessary), but that's probably a matter for later.
There was a problem hiding this comment.
So would it be a good idea to split this into e.g. symbolic_input and symbolic_const or rather simply have symbolic_input take a boolean attribute const that can be defined using a special const keyword (similar to sync /async for registers?
There was a problem hiding this comment.
Both approaches are fine, but we don't necessarily have to do that right now. I just wanted to make sure that the semantics of the op is well described in the documentation to avoid any confusions in the future.
There was a problem hiding this comment.
Good point - personally I lean in favour of separate ops as a) I wouldn't say symbolic_input isn't a super clear name for a constant value (and it would nice to keep the clear mapping to SMT vs BTOR) and b) having two separate ops may just leave less room for confusion, but I'm very happy to be overruled!
There was a problem hiding this comment.
Wouldn't we also be able to define a value that is only set once by using a symbolic input as the init value of a concrete input and then have the update value being simply constant?
There was a problem hiding this comment.
Good point. By doing the following, right?
%0 = verif.symbolic_input : i32
%1 = verif.concrete_input %0, %1 : i32
There was a problem hiding this comment.
This would work functionally - the disadvantage to me is that we'd have an unnecessary symbolic_input floating around, which I guess semantically in the case of model checking would require a new SMT var to be created for that input each cycle, though it wouldn't actually be used. We could pattern match for this case and optimize it away in VerifToSMT I guess, but it would mean we couldn't immediately reject symbolic_input ops which would be nice to do (since the meaning of that might get a little messy with the init/loop regions). Happy to just worry about this in the future though!
| This operation declares a concrete input that can then be used in the | ||
| reasoning surrounding symbolic inputs, allowing for a form of concolic | ||
| reasoning to take place in a `verif.formal` block. Concrete inputs are | ||
| defined by an initial value and an update function. |
There was a problem hiding this comment.
Can we specify when this update function is executed? Does this op effectively behave like a register with an implicit clock?
There was a problem hiding this comment.
I see this as the op is executed on every "time-step" so it would be converted into a register with an implicit clock yes. I'm open to other ideas if you have any
There was a problem hiding this comment.
In its current state one could argue that it's not really necessary because you could just use the regular register operation, but I think it's still useful to have it so we still know that it is an input and not just part of the design. Also, providing the clock for the regular register would probably require a block argument from verif.formal. So, I'd leave it as is. I just think, it'd just be nice to describe this implicit clock and how the value updating works a bit more in the description. Basically, verif.formal provides an implicit base clock and the symbolic and concrete operations provide values for all inputs (including the actual clocks) based on this implicit clock.
| Additional information about how the test should be conducted can be passed | ||
| using the two supported attributes. These attributes are `k`, which defines | ||
| the bounds of the test, and `type` which defines the type of formal test | ||
| being done, i.e. Bounded Model Checking (BMC) or k-Induction. |
There was a problem hiding this comment.
Nit: happy to be overruled on grounds of repetition but it might be nice to say the syntax here, just makes the docs slightly easier to digest
| let description = [{ | ||
| This operation declares a symbolic input that can then be used to reason | ||
| about `hw.instance` inputs in a symbolic manner in future assertions and | ||
| assumptions. The result type must be explicitly marked. |
There was a problem hiding this comment.
It's probably a good idea to describe a bit more precisely how this symbolic value behaves over time. Is it fixed over all clock cycles, can it change at a clock edge, can it change at any time?
Agreed. Guessing from when we spoke about it before that it can only change on a clock-edge - we might want to add another op for a value that's fixed over all cycles (e.g. for defining BMC inputs while making sure we're adhering to the right semantics but not having to create a new BV every cycle when it's not necessary), but that's probably a matter for later.
dobios
changed the title
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
PrepareForFormalpass, and make sure that onlyverif.formalops are used for formal verification and ignored elsewhere.The ops that have been added in this PR are:
verif.formalverif.symbolic_valverif.concrete_valFeel free to let me know what you think!