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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Thu May 28 21:27:22 BST 2020


--- 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?


> 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.

More information about the libre-riscv-dev mailing list