[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

--- Comment #19 from Michael Nolan <mtnolan2640 at gmail.com> ---
(In reply to Cole Poirier from comment #18)

> Further with regard to Michael's comments about needing to use Initial() and
> ResetSignal() should I wrap the if writethru..else in a "with
> m.If(init)...with m.Else()" similar to proof_fu.py? Is it the case that, if
> Initial() then do rd operations, and else do wr operations?

I don't know specifically for this module, but generally you want to make sure
that the module and control signals are initialized to a default state. 

For instance, you're going to be proving that a write to a register works sort
of like this:

with m.If(Past(rd_en)):
    comb += Assert(data_out == something)

However, on cycle 0, yosys may choose Past(rd_en) to be High, but no data will
be output because it didn't happen during the actual proof (basically, yosys
saves the past state of the signal to a register, which is then read whenever
you call Past(signal). But on cycle 0, that register has a random value)

If you wait one cycle (with m.If(~init)) before doing your assertion, you won't
have that issue because Past(signal) will return the actual value from the
cycle before.

However, if you decide to use the initial cycle to reset your register file,
you'll have other issues because you're resetting it at the same time you're
reading it, so once again your assertion will probably fail. To fix this, you'd
want to use an Assume to force rd_en (or whatever other signals you're using)
to be disabled during reset.

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