Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

make explicit the reg_check constant values #54

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

silabs-robin
Copy link

@silabs-robin silabs-robin commented Sep 7, 2021

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.

@silabs-robin
Copy link
Author

See also #45

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant