Solver Chosen Constants for Formal Verification

[fayalalebrun]

Solver Chosen Constants for Formal Verification

[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.