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, AnySeq, Assume, Cover, Initial,
   6                             Rose, Fell, Stable, Past)
   7 from nmutil.formaltest 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, writethru=True):
  16         super().__init__(8, writethru)
  17         for i in range(1): # just do one for now
  18             self.read_port(f"{i}")
  19             self.write_port(f"{i}")
  20
  21     def elaborate(self, platform):
  22         m = super().elaborate(platform)
  23         comb = m.d.comb
  24         sync = m.d.sync
  25
  26         width     = self.width
  27         writethru = self.writethru
  28         _rdports  = self._rdports
  29         _wrports  = self._wrports
  30
  31
  32         comb += _wrports[0].data_i.eq(AnySeq(8))
  33         comb += _wrports[0].wen.eq(AnySeq(1))
  34         comb += _rdports[0].ren.eq(AnySeq(1))
  35
  36         rst = ResetSignal()
  37
  38         init = Initial()
  39
  40         # Most likely incorrect 4-way truth table
  41         #
  42         # rp.ren  wp.wen  rp.data_o            reg
  43         # 0       0       zero                 should be previous value
  44         # 0       1       zero                 wp.data_i
  45         # 1       0       reg                  should be previous value
  46         # 1       1       wp.data_i            wp.data_i
  47
  48         # Holds the value written to the register when a write happens
  49         register_data = Signal(self.width)
  50         register_written = Signal()
  51
  52         # Make sure we're actually hitting a read and write
  53         comb += Cover(_rdports[0].ren & register_written)
  54
  55         with m.If(init):
  56             comb += Assume(rst == 1)
  57             for port in _rdports:
  58                 comb += Assume(port.ren == 0)
  59             for port in _wrports:
  60                 comb += Assume(port.wen == 0)
  61
  62             comb += Assume(register_written == 0)
  63
  64         with m.Else():
  65             comb += Assume(rst == 0)
  66
  67             # If there is no read, then data_o should be 0
  68             with m.If(_rdports[0].ren == 0):
  69                 comb += Assert(_rdports[0].data_o == 0)
  70
  71             # If there is a read request
  72             with m.Else():
  73                 if writethru:
  74                     # Since writethrough is enabled, we need to check
  75                     # if we're writing while reading. If so, then the
  76                     # data from the read port should be the same as
  77                     # that of the write port
  78                     with m.If(_wrports[0].wen):
  79                         comb += Assert(_rdports[0].data_o ==
  80                                        _wrports[0].data_i)
  81
  82                     # Otherwise, check to make sure the register has
  83                     # been written to at some point, and make sure the
  84                     # data output matches the data that was written
  85                     # before
  86                     with m.Else():
  87                         with m.If(register_written):
  88                             comb += Assert(_rdports[0].data_o == register_data)
  89
  90                 else:
  91                     # Same as the Else branch above, make sure the
  92                     # read port data matches the previously written
  93                     # data
  94                     with m.If(register_written):
  95                         comb += Assert(_rdports[0].data_o == register_data)
  96
  97             # If there is a write, store the data to be written to our
  98             # copy of the register and mark it as written
  99             with m.If(_wrports[0].wen):
 100                 sync += register_data.eq(_wrports[0].data_i)
 101                 sync += register_written.eq(1)
 102
 103         return m
 104
 105
 106 class TestCase(FHDLTestCase):
 107     def test_formal(self):
 108         for writethrough in [False, True]:
 109             module = Driver(writethrough)
 110             self.assertFormal(module, mode="bmc", depth=10)
 111             self.assertFormal(module, mode="cover", depth=10)
 112
 113     def test_ilang(self):
 114         dut = Driver()
 115         vl = rtlil.convert(dut, ports=[])
 116         with open("regfile.il", "w") as f:
 117             f.write(vl)
 118
 119
 120 if __name__ == '__main__':
 121     unittest.main()