[Verif] Simplify the FormalOp

[fabianschuiki]

Simplify the definition of the verif.formal operation which describes a single formal unit test. This op used to have a "k" parameter which is now gone in favor of more generically using the attributes dictionary to capture execution parameters. As we build out the testing flows, we can reintroduce necessary attributes to this operation.

Rename verif.symbolic_input to verif.symbolic_value.

Remove verif.concrete_input in favor of explicitly describing the concrete input using one of the registers in the Seq dialect. This also makes the associated clock explicit, which was missing from this op.

[seldridge]

This seems reasonable to me!

One footgun with this approach is that the attributes could now be discarded. We can introduce something separate, e.g., a dedicated parameter that contains mandatory arguments so that this is guaranteed to be preserved. However, I don't see a reason to do this now.

[fabianschuiki]

Good point about the discardable arguments. Once we actually rely on them, we could add a dedicated dictionary property that actually contains the parameters. That wouldn't be discardable.

[dobios]

@fabianschuiki the entire point of having concrete_input was to describe alternative clocks in a multi-clock system (which should be encoded relative to some implicit clock in theory to be able to use it in the formal backends) so I think it would be wiser to change it to be driven by an arbitrary LLVM IR function instead of removing it entirely. Just my two cents, we could also to tell the user "hey you need to encode all of your clocks relative to some abstract global clock if you want us to verify you multi-clock system" -- which would be the required approach if we enforce that it's modeled using a register.

[dobios]

damn these PRs are going through at lightning speed, I have yet to have had the time to catch one before it gets merged in ^^"

[dobios]

Also we used the K as an operand because it's mandatory information to know how to perform our bounded model check. Like verif.formal {} without a k in the attributes is unusable -- so shouldn't a mandatory attribute be an operand?

[fabianschuiki]

@dobios was to describe alternative clocks in a multi-clock system

Hmmm yeah the clocking part is challenging. I'm not entirely sure yet whether clocks should get any special treatment during formal verification. It's pretty common for tools to just treat them as regular inputs. In the BMC you would then check for clock toggles to decide whether you use the previous cycle's data input as the current value, or the previous data output (in case of no clock). There's an optimization in there where you detect that the circuit doesn't make any progress without a clock, e.g. when there's one unique clock and no I/O paths. In that case the tool may decide to always assume a clock toggle. This feels like an optimization in the verif tool though.

My plan is to figure out how we can run these verif.formal ops through different tools and then distill the necessary stuff on the op from that. It's often easier to only add something when there is an immediate need for it.

we used the K as an operand because it's mandatory information to know how to perform our bounded model check

I agree, that's true for a BMC. But there are other ways you could formally verify verif.formal, for example through an induction. The induction itself doesn't really have a bound. You can have one just in case, but it's not necessary. If we encounter a verif.formal {}, a reasonable thing to do might be to do an induction on it. It's not entirely clear to me yet what all the different needs are. Again, I'd rather have nothing there and then figure out what we need when we try to run things through a tool 😁

[dobios]

@fabianschuiki The induction itself doesn't really have a bound.

I agree with the other parts of your comment, but in practice when you perform induction you will actually be using k-induction, which is a version that has a stronger induction hypothesis and base-case based on using k steps in your transition system, so I do think that we would need to have this K somewhere. Either way, the only back-ends directly supported in CIRCT for now are BMC-based afaik. But if you want to use this for generating SV then I feel like you should simply specify that k can be ignored at the tool-level, like in circt-test rather than removing it entirely. What I'm getting at is that not having that bound essentially means that we don't have the information needed to run it through the CIRCT formal back-ends, so we would need to make up some default k -- which is ofc also a solution. I just wanted to make sure that this is what you're expecting by making it an optional attribute.

[fabianschuiki]

Great point about a default value for k. That might be a good starting point. And you're right, in practice you'll probably have to specify the k for most of your tests because it's an attribute of the test itself, and you wouldn't want your tests to start breaking just because some default unroll bound got changed.