Solver Chosen Constants for Formal Verification

[fayalalebrun]

In SymbiYosys, the anyconst attribute can be used in order to have the solver choose a constant for an input variable. For certain types of designs, this can make proving correctness easier.

Is there currently a way to specify such an attribute with chiseltest?

[ekiwi]

An uninitialized register should essentially be able to emulate the behavior of anyconst.:

val myConst = Reg(UInt(8.W))

Registers without a reset value will start at an arbitrary constant (solver chosen in case of formal) and then, assuming you do not assign anything to them, they will retain their value.

[fayalalebrun]

Would the following have the same effect?

assume(stable(input))

[ekiwi]

Would the following have the same effect?

I think so. The only downside here is that to make an input you need to be in the top-level module. Registers can easily declared independent of module hierarchy.