[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 #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")

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