src/soc/regfile/formal/proof_regfile_binary.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, Array)
   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 import math
  11
  12 from soc.regfile.regfile import RegFile
  13
  14
  15 class Driver(RegFile):
  16     def __init__(self):
  17         super().__init__(width=8, depth=4)
  18         for i in range(1): # just do one for now
  19             self.read_port()
  20             self.write_port()
  21
  22     def elaborate(self, platform):
  23         m = super().elaborate(platform)
  24         comb = m.d.comb
  25         sync = m.d.sync
  26
  27         width     = self.width
  28         depth     = self.depth
  29         lg2depth  = int(math.ceil(math.log2(depth)))
  30         _rdports  = self._rdports
  31         _wrports  = self._wrports
  32
  33         comb += _wrports[0].data_i.eq(AnySeq(8))
  34
  35         comb += _wrports[0].wen.eq(AnySeq(1))
  36         comb += _wrports[0].waddr.eq(AnySeq(lg2depth))
  37         comb += _rdports[0].ren.eq(AnySeq(1))
  38         comb += _rdports[0].raddr.eq(AnySeq(lg2depth))
  39
  40         rst = ResetSignal()
  41
  42         init = Initial()
  43
  44         # Most likely incorrect 4-way truth table
  45         #
  46         # rp.ren  wp.wen  rp.data_o            reg
  47         # 0       0       zero                 should be previous value
  48         # 0       1       zero                 wp.data_i
  49         # 1       0       reg                  should be previous value
  50         # 1       1       wp.data_i            wp.data_i
  51
  52         # Holds the value written to the register when a write happens
  53         register_data = Array([Signal(self.width, name=f"reg_data{i}")
  54                                for i in range(depth)])
  55         register_written = Array([Signal(name=f"reg_written{i}")
  56                                   for i in range(depth)])
  57
  58         with m.If(init):
  59             comb += Assume(rst == 1)
  60
  61             for i in range(depth):
  62                 comb += Assume(register_written[i] == 0)
  63
  64         with m.Else():
  65             comb += Assume(rst == 0)
  66
  67             with m.If(_rdports[0].ren == 0):
  68                 comb += Assert(_rdports[0].data_o == 0)
  69
  70             # Read enable is active
  71             with m.Else():
  72                 addr = _rdports[0].raddr
  73                 # Check to see if there's a write on this
  74                 # cycle. If so, then the output data should be
  75                 # that of the write port
  76                 with m.If(_wrports[0].wen & (_wrports[0].waddr == addr)):
  77                     comb += Assert(_rdports[0].data_o ==
  78                                    _wrports[0].data_i)
  79                     comb += Cover(1)
  80
  81                 # Otherwise the data output should be the
  82                 # saved register
  83                 with m.Elif(register_written[addr]):
  84                     comb += Assert(_rdports[0].data_o ==
  85                                    register_data[addr])
  86                     comb += Cover(1)
  87
  88             # If there's a write to a given register, store that
  89             # data in a copy of the register, and mark it as
  90             # written
  91             with m.If(_wrports[0].wen):
  92                 addr = _wrports[0].waddr
  93                 sync += register_data[addr].eq(_wrports[0].data_i)
  94                 sync += register_written[addr].eq(1)
  95
  96
  97
  98         return m
  99
 100
 101 class TestCase(FHDLTestCase):
 102     def test_formal(self):
 103         module = Driver()
 104         self.assertFormal(module, mode="bmc", depth=10)
 105         self.assertFormal(module, mode="cover", depth=10)
 106
 107     def test_ilang(self):
 108         dut = Driver()
 109         vl = rtlil.convert(dut, ports=[])
 110         with open("regfile_binary.il", "w") as f:
 111             f.write(vl)
 112
 113
 114 if __name__ == '__main__':
 115     unittest.main()