[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 #21 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #20)
> (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.

Ok. Pushed a commit with that. Can you take a look?

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