[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=353

Michael Nolan <mtnolan2640 at gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |mtnolan2640 at gmail.com

--- Comment #17 from Michael Nolan <mtnolan2640 at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #16)
> (In reply to Cole Poirier from comment #15)
> 
> > Spent an hour trying to sense of this but I think my brain has given up for
> > the day. Will make a fresh effort tomorrow.
> 
> did a bit of a reorg.  i think we need to look at how proof_fu.py works.
> the use of "Initial()" may be crucial.

It is. From my experience doing formal stuff in verilog, if you use $past()
without making sure the module is properly reset, the proof engine will make up
values for the signals before the proof even starts. Making sure you have a
reset for the first cycle of the proof, and not examining any Past() signals on
that cycle will avoid this.

-- 
You are receiving this mail because:
You are on the CC list for the bug.