-
Notifications
You must be signed in to change notification settings - Fork 94
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
rvfi_reg_check is possibly broken (picorv32 also fails the assertion) #53
Comments
Checks passed for me today. I changed |
Hi @dvc94ch. Thanks for doing a test of those proofs. I am quite busy at the moment but I will certainly try out the same change as you show here and continue my debugging from there. |
Hi. I am back again.
Indeed this works. I just tried it on picorv32 myself. That seems to resolve the part about picorv32. But to the main question about whether the "reg" check is ok or not. |
It seems the checker is wrong as both
picorv32
andcv32e40x
get failing assertions and the traces look weird.Otherwise, I might be wrong and have misunderstood something here.
If anyone else currently see reg_check working fine then please let me know.
Brief:
Register checks should execute (at least) 2 instructions, then check that the last one reads correctly that which the first one wrote.
What I observe is that the register read is arbitrary (undriven) and does not match the register read.
Example: Write
rd_wdata='hABCD
tord_addr=1
, and then CEX because a read fromrs1_addr=2
(note: different than rd) does not have matching datars1_rdata != 'hABCD
.Evidence 1
picorv32 see failure when running the reg check.
Fresh build/install of yosys/symbiyosys/boolector from:
https://symbiyosys.readthedocs.io/en/latest/install.html
Followed the README in cores/picorv32 to wget the source and launch checks.
Failure reported in "reg" checks.
NB! It was not able to parse by default, so I changed the
const rand reg
macro to justreg
. (this was not changed for cv32e40x using a different formal tool)."logfile.txt" line 63:
"src/rvfi_reg_check.sv" line 44:
The rs2 check fails.
This might also be a bug in picorv32, or it might be a bug in my methodology.
Evidence 2
cv32e40x see failure when running the reg check, and the checker seems to do an arbitrary comparison.
A similar problem is observed here. There is a CEX because the
register_shadow
was set for a different register than the one being read later (rs1).It is also possible to get a trace where only 1 instruction retires, but that seems counter to the purpose of the test. I would think assumes should be in place to not permit this.
Thoughts
I don't fully understand the code,
but it seems that nothing is driving
register_index
and that it should maybe be stored similar to howregister_shadow
is stored.Extra info - Possibly a similar bug in the PC checks
There is a similar issue in
pc_fwd
andpc_bwd
where the expected PC can be stored once, then one or more instructions may follow, and finally the check happens but the expected PC was not updated by the intermediate instructions so the comparison is done against an outdated expectation and gets an errorThe text was updated successfully, but these errors were encountered: