make explicit the reg_check constant values #54
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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 #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.