[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 #18 from Cole Poirier <colepoirier at gmail.com> ---
(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?

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

If not can you help me with a diagram or a link? I've looked for 4-way truth
tables via google and I just get basic boolean logic tutorials in the form of:

```
p q  p AND q
0 0  0
0 1  0
1 0  0
1 1  1
```

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