[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
Wed May 27 20:43:34 BST 2020


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

More information about the libre-riscv-dev mailing list