There are two random constants used in the reg_check, but the verilog code that made them constant were not very reliable.
This PR makes the constness more explicit and uses simple verilog so there shouldn't be any problems with support for "const reg".
On line 12 in https://github.com/SymbioticEDA/riscv-formal/blob/master/checks/rvfi_macros.vh#L12 the definition of "reg" is also not enough to ensure constness. Using "const reg" is not so much better. At least in the tool we are using, this still let the tool produce changing values on that signal. I am not even sure what is legal verilog in this regard, as potentially a constant X value does not have defined formal semantics. Hence I think this simpler solution could be better.
NB. I have not tested this with picorv32 and symbiyosys.
It is tested with the cv32e40x and a different formal tool, but the 40x currently has a bug that was revealed by this checker.
Alternative: Does yosys support "bit"? That could be a better solution.
silabs-robin
commented
3 years ago
There are two random constants used in the reg_check, but the verilog code that made them constant were not very reliable. This PR makes the constness more explicit and uses simple verilog so there shouldn't be any problems with support for "const reg".
On line 12 in https://github.com/SymbioticEDA/riscv-formal/blob/master/checks/rvfi_macros.vh#L12 the definition of "reg" is also not enough to ensure constness. Using "const reg" is not so much better. At least in the tool we are using, this still let the tool produce changing values on that signal. I am not even sure what is legal verilog in this regard, as potentially a constant X value does not have defined formal semantics. Hence I think this simpler solution could be better.
The problem was detected via this issue https://github.com/SymbioticEDA/riscv-formal/issues/53
NB. I have not tested this with picorv32 and symbiyosys. It is tested with the cv32e40x and a different formal tool, but the 40x currently has a bug that was revealed by this checker.
Alternative: Does yosys support "bit"? That could be a better solution.