src/soc/regfile/formal/proof_regfile.py

   1 # This is the proof for Regfile class from regfile/regfile.py
   2
   3 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   4                     signed, ResetSignal)
   5 from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial,
   6                             Rose, Fell, Stable, Past)
   7 from nmigen.test.utils import FHDLTestCase
   8 from nmigen.cli import rtlil
   9 import unittest
  10
  11 from soc.regfile.regfile import Register
  12
  13
  14 class Driver(Register):
  15     def __init__(self):
  16         super().__init__(8)
  17
  18     def elaborate(self, platform):
  19         m = super().elaborate(platform)
  20         comb = m.d.comb
  21
  22         width     = self.width
  23         writethru = self.writethru
  24         _rdports  = self._rdports
  25         _wrports  = self._wrports
  26         reg       = self.reg
  27
  28         for i in range(8):
  29             self.read_port(f"{i}")
  30             self.write_port(f"{i}")
  31
  32         comb += reg.eq(AnyConst(8))
  33
  34         for i in range(0,len(_rdports)):
  35             with m.If(_rdports[i].ren & writethru):
  36                 with m.If(_wrports[i].wen):
  37                     comb += Assert(_rdports[i].data_o == _wrports[i].data_i)
  38                 with m.Else():
  39                     comb += Assert(_rdports[i].data_o == reg)
  40             with m.Else():
  41                 comb += Assert(_rdports[i].data_o == reg)
  42
  43         return m
  44
  45
  46 class TestCase(FHDLTestCase):
  47     def test_formal(self):
  48         module = Driver()
  49         self.assertFormal(module, mode="bmc", depth=2)
  50         self.assertFormal(module, mode="cover", depth=2)
  51
  52     def test_ilang(self):
  53         dut = Driver()
  54         vl = rtlil.convert(dut, ports=[])
  55         with open("regfile.il", "w") as f:
  56             f.write(vl)
  57
  58
  59 if __name__ == '__main__':
  60     unittest.main()