From f21eeb4373b9da94a68c0d21044f2002c9ba03ab Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Mon, 1 Jun 2020 14:50:52 -0400 Subject: [PATCH] Add proof for RegFileArray --- src/soc/regfile/formal/proof_regfile_array.py | 123 ++++++++++++++++++ 1 file changed, 123 insertions(+) create mode 100644 src/soc/regfile/formal/proof_regfile_array.py diff --git a/src/soc/regfile/formal/proof_regfile_array.py b/src/soc/regfile/formal/proof_regfile_array.py new file mode 100644 index 00000000..b35c51eb --- /dev/null +++ b/src/soc/regfile/formal/proof_regfile_array.py @@ -0,0 +1,123 @@ +# This is the proof for Regfile class from regfile/regfile.py + +from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl, + signed, ResetSignal, Array) +from nmigen.asserts import (Assert, AnySeq, Assume, Cover, Initial, + Rose, Fell, Stable, Past) +from nmigen.test.utils import FHDLTestCase +from nmigen.cli import rtlil +import unittest + +from soc.regfile.regfile import RegFileArray + + +class Driver(RegFileArray): + def __init__(self): + super().__init__(width=8, depth=4) + for i in range(1): # just do one for now + self.read_port(f"rd{i}") + self.write_port(f"wr{i}") + + def elaborate(self, platform): + m = super().elaborate(platform) + comb = m.d.comb + sync = m.d.sync + + width = self.width + depth = self.depth + _rdports = self._rdports + _wrports = self._wrports + + comb += _wrports[0][1].data_i.eq(AnySeq(8)) + comb += _wrports[0][1].wen.eq(AnySeq(depth)) + comb += _rdports[0][1].ren.eq(AnySeq(depth)) + + rst = ResetSignal() + + init = Initial() + + # Most likely incorrect 4-way truth table + # + # rp.ren wp.wen rp.data_o reg + # 0 0 zero should be previous value + # 0 1 zero wp.data_i + # 1 0 reg should be previous value + # 1 1 wp.data_i wp.data_i + + # Holds the value written to the register when a write happens + register_data = Array([Signal(self.width, name=f"reg_data{i}") + for i in range(depth)]) + register_written = Array([Signal(name=f"reg_written{i}") + for i in range(depth)]) + comb += Cover(_rdports[0][1].ren == 0b0001) + + with m.If(init): + comb += Assume(rst == 1) + + for i in range(depth): + comb += Assume(register_written[i] == 0) + + with m.Else(): + comb += Assume(rst == 0) + + + # Assume that rd_en is onehot + bitsum = 0 + for i in range(depth): + bitsum = bitsum + _rdports[0][1].ren[i] + comb += Assume(bitsum <= 1) + + + + # If there is no read, then data_o should be 0 + with m.If(_rdports[0][1].ren == 0): + comb += Assert(_rdports[0][1].data_o == 0) + + # One of the rd_enable requests must be active + with m.Else(): + for i in range(depth): + # If there's a read on this register + with m.If(_rdports[0][1].ren[i]): + # Check to see if there's a write on this + # cycle. If so, then the output data should be + # that of the write port + with m.If(_wrports[0][1].wen[i]): + comb += Assert(_rdports[0][1].data_o == + _wrports[0][1].data_i) + comb += Cover(1) + + # Otherwise the data output should be the + # saved register + with m.Elif(register_written[i]): + comb += Assert(_rdports[0][1].data_o == + register_data[i]) + comb += Cover(1) + + for i in range(depth): + # If there's a write to a given register, store that + # data in a copy of the register, and mark it as + # written + with m.If(_wrports[0][1].wen[i]): + sync += register_data[i].eq(_wrports[0][1].data_i) + sync += register_written[i].eq(1) + + + + return m + + +class TestCase(FHDLTestCase): + def test_formal(self): + module = Driver() + self.assertFormal(module, mode="bmc", depth=10) + self.assertFormal(module, mode="cover", depth=10) + + def test_ilang(self): + dut = Driver() + vl = rtlil.convert(dut, ports=[]) + with open("regfile_array.il", "w") as f: + f.write(vl) + + +if __name__ == '__main__': + unittest.main() -- 2.30.2