From 1fcbecdab578308e01e7db1fb1928d0f099d7e31 Mon Sep 17 00:00:00 2001
From: colepoirier <colepoirier@gmail.com>
Date: Wed, 27 May 2020 10:25:31 -0700
Subject: [PATCH] First commit of proof of regfile, not working yet

---
 src/soc/regfile/formal/proof_regfile.py | 61 +++++++++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 src/soc/regfile/formal/proof_regfile.py

diff --git a/src/soc/regfile/formal/proof_regfile.py b/src/soc/regfile/formal/proof_regfile.py
new file mode 100644
index 00000000..6ecad092
--- /dev/null
+++ b/src/soc/regfile/formal/proof_regfile.py
@@ -0,0 +1,61 @@
+# This is the proof for Regfile class from regfile/regfile.py
+
+from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
+                    signed, ResetSignal)
+from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial,
+                            Rose, Fell, Stable, Past)
+from nmigen.test.utils import FHDLTestCase
+from nmigen.cli import rtlil
+import unittest
+
+from soc.regfile import Register
+
+
+class Driver(Elaboratable):
+    def __init__(self):
+        pass
+
+    def elaborate(self, platform):
+        m = Module()
+        comb = m.d.comb
+        m.submodules.dut = dut = Register(32)
+
+        width     = dut.width
+        writethru = dut.writethru
+        _rdports  = dut._rdports
+        _wrports  = dut._wrports
+        reg       = dut.reg
+
+        for i in range(8):
+            dut.read_port(f"{i}")
+            dut.write_port(f"{i}")
+
+        comb += reg.eq(AnyConst(32))
+
+        for i in range(0,len(_rdports)):
+            with m.If(_rdports[i].ren & writethru):
+                with m.If(_wrports[i].wen):
+                    comb += Assert(rdports[i].data_o == _wrports[i].data_i)
+                with m.Else():
+                    comb += Assert(rdports[i].data_o == reg)
+            with m.Else():
+                comb += Assert(_rdports[i].data_o == reg)
+
+        return m
+
+
+    def TestCase(FHDLTestCase):
+        def test_formal(self):
+            module = Driver()
+            self.assertFormal(module, mode="bmc", depth=2)
+            self.assertFormal(module, mode="cover", depth=2)
+
+        def test_ilang(self):
+            dut = Driver()
+            vl = rtlil.convert(dut, ports=[])
+            with open("regfile.il", "w") as f:
+                f.write(vl)
+
+
+if __name__ == '__main__':
+    unittest.main()
-- 
2.30.2