[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 #11 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cole Poirier from comment #10)
> Tests now actually run, so I pushed a new commit. In order to formally
> verify class Register(), I think I've done most of it, but there's a part of
> the class's elaborate function that uses sync instead of comb, and I'm not
> sure how to do this in proof form.

one way is to use Past()

> 
> ```
> def elaborate(self, platform):
>      m = Module()
>      self.reg = reg = Signal(self.width, name="reg")
> 
> [snip..] 
>      # write ports, don't allow write to address 0 (ignore it)
>      for wp in self._wrports:
>          with m.If(wp.wen):
>              m.d.sync += reg.eq(wp.data_i)
> 
>      return m
> ```
> 
> Does the above prevent write to address 0, and if so how?

no.  do git pull

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