[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 #20 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cole Poirier from comment #18)
> (In reply to Luke Kenneth Casson Leighton from comment #13)
> > i suggest starting with two utterly different proofs, divided and isolated
> > with "if self.writethru".  yes NOT m.If because python parameters != nmigen
> > AST.A
> > 
> > then, to do a 4 way (dual nested) set of m.If on ren and wen.
> > 
> > then, in EACH quadrant, do completely separate assertions.
> > 
> > but before making those assertions, write out in words the expected
> > behaviour when the 4 way truth table of wen and ren occurs.
> 
> I think I might not understand the functionality of the module enough to
> know the expected behaviour. Is it the case that if not writethru nothing is
> supposed to happen?
> 
> 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?

yyep.

> Is it the case that, if
> Initial() then do rd operations, and else do wr operations?

nnope.  Initial() is just that: the initial conditions.


> Finally, with regard to the 4-way truth table, is this format close to
> correct?
> 
> ```
> rd.ren wr.wen rd.data_o reg
> 0      0      x         y
> 0      1      x         y
> 1      0      x         y
> 1      1      x         y
> ```

yep.  drop that into a comment in the code, so we can edit it before
implementing it.

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