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(Elaboratable):
  15     def __init__(self):
  16         pass
  17
  18     def elaborate(self, platform):
  19         m = Module()
  20         comb = m.d.comb
  21         m.submodules.dut = dut = Register(32)
  22
  23         width     = dut.width
  24         writethru = dut.writethru
  25         _rdports  = dut._rdports
  26         _wrports  = dut._wrports
  27         reg       = dut.reg
  28
  29         for i in range(8):
  30             dut.read_port(f"{i}")
  31             dut.write_port(f"{i}")
  32
  33         comb += reg.eq(AnyConst(32))
  34
  35         for i in range(0,len(_rdports)):
  36             with m.If(_rdports[i].ren & writethru):
  37                 with m.If(_wrports[i].wen):
  38                     comb += Assert(rdports[i].data_o == _wrports[i].data_i)
  39                 with m.Else():
  40                     comb += Assert(rdports[i].data_o == reg)
  41             with m.Else():
  42                 comb += Assert(_rdports[i].data_o == reg)
  43
  44         return m
  45
  46
  47 class TestCase(FHDLTestCase):
  48     def test_formal(self):
  49         module = Driver()
  50         self.assertFormal(module, mode="bmc", depth=2)
  51         self.assertFormal(module, mode="cover", depth=2)
  52
  53     def test_ilang(self):
  54         dut = Driver()
  55         vl = rtlil.convert(dut, ports=[])
  56         with open("regfile.il", "w") as f:
  57             f.write(vl)
  58
  59
  60 if __name__ == '__main__':
  61     unittest.main()