[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:25:25 BST 2020


--- Comment #10 from Cole Poirier <colepoirier at gmail.com> ---
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.

def elaborate(self, platform):
     m = Module()
     self.reg = reg = Signal(self.width, name="reg")

     # 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? because it doesn't
seem to do any conditional checking. Further, how would I integrate this in
order to finish the proof or register?

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

More information about the libre-riscv-dev mailing list