src/soc/fu/compunits/formal/proof_fu.py

   1 # This is the proof for the computation unit/Function Unit/ALU
   2 # manager. Description here:
   3 # https://libre-soc.org/3d_gpu/architecture/compunit/
   4
   5 # This attempts to prove most of the bullet points on that page
   6
   7
   8 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   9                     signed, ResetSignal)
  10 from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial,
  11                             Rose, Fell, Stable, Past)
  12 from nmigen.test.utils import FHDLTestCase
  13 from nmigen.cli import rtlil
  14 import unittest
  15
  16 from soc.fu.compunits.compunits import FunctionUnitBaseSingle
  17 from soc.experiment.alu_hier import DummyALU
  18 from soc.experiment.compalu_multi import MultiCompUnit
  19 from soc.fu.alu.alu_input_record import CompALUOpSubset
  20
  21 class Driver(Elaboratable):
  22     def __init__(self):
  23         pass
  24
  25     def elaborate(self, platform):
  26         m = Module()
  27         comb = m.d.comb
  28         sync = m.d.sync
  29         alu = DummyALU(16)
  30         m.submodules.dut = dut = MultiCompUnit(16, alu,
  31                                                CompALUOpSubset)
  32
  33         issue = dut.issue_i
  34         busy = dut.busy_o
  35
  36         go_rd = dut.rd.go
  37         rd_rel = dut.rd.rel
  38
  39         go_wr = dut.wr.go
  40         wr_rel = dut.wr.rel
  41
  42         go_die = dut.go_die_i
  43         shadow = dut.shadown_i
  44
  45         rst = ResetSignal()
  46
  47         init = Initial()
  48
  49         has_issued = Signal(reset=0)
  50
  51
  52
  53         with m.If(init):
  54             comb += Assume(has_issued == 0)
  55             comb += Assume(issue == 0)
  56             comb += Assume(go_rd == 0)
  57             comb += Assume(rst == 1)
  58         with m.Else():
  59             comb += Assume(rst == 0)
  60
  61             # detect when issue has been raised and remember it
  62             with m.If(issue):
  63                 sync += has_issued.eq(1)
  64                 comb += Cover(has_issued)
  65
  66             # Property 1: after an issue, busy should be raised
  67             with m.If(Past(issue)):
  68                 comb += Assert(busy)
  69
  70             # Property 2: After a wr_rel and go_wr, busy should be lowered
  71             with m.If(Past(wr_rel) & Past(go_wr)):
  72                 # Shadow interferes with this and I'm not sure what is
  73                 # correct
  74                 with m.If(~Past(shadow)):
  75                     comb += Assert(busy == 0)
  76             with m.Elif(Past(busy) == 1):
  77                 comb += Assert(busy == 1)
  78
  79             # Property 3: Rd_rel should never be asserted before issue
  80
  81             # If issue has never been raised, then rd_rel should never
  82             # be raised
  83             with m.If(rd_rel != 0):
  84                 comb += Assert(has_issued)
  85
  86             # Property 4: when rd_rel is asserted, it should stay
  87             # that way until a go_rd
  88             with m.If((Past(go_rd) == 0) & ~Past(go_die)):
  89                 comb += Assert(~Fell(rd_rel))
  90
  91             # Property 5: when a bit in rd_rel is asserted, and
  92             # the corresponding bit in go_rd is asserted, then that
  93             # bit of rd_rel should be deasserted
  94             for i in range(2):
  95                 with m.If(Past(go_rd)[i] & (Past(rd_rel) != 0)):
  96                     comb += Assert(rd_rel[i] == ~Past(go_rd)[i])
  97
  98             # Property 6: Similarly, if rd_rel is asserted,
  99             # asserting go_die should make rd_rel be deasserted
 100
 101             with m.If(Past(rd_rel) != 0):
 102                 with m.If(Past(go_die)):
 103                     comb += Assert(rd_rel == 0)
 104
 105             comb += Cover(Fell(rd_rel))
 106
 107             # Property 7: Similar to property 3, wr_rel should
 108             # never be asserted unless there was a preceeding issue
 109
 110             with m.If(wr_rel != 0):
 111                 comb += Assert(has_issued)
 112
 113             # Property 8: Similar to property 4, wr_rel should stay
 114             # asserted until a go_rd, go_die, or shadow
 115
 116             with m.If((Past(go_wr) == 0) & ~Past(go_die, 2) &
 117                       ~Past(shadow)):
 118                 comb += Assert(~Fell(wr_rel))
 119             # Assume go_wr is not asserted unless wr_rel is
 120             with m.If(wr_rel == 0):
 121                 comb += Assume(go_wr == 0)
 122
 123
 124             # Property 9: Similar to property 5, when wr_rel is
 125             # asserted and go_wr is asserted, then wr_rel should be
 126             # deasserted
 127             with m.If(Past(wr_rel) & Past(go_wr)):
 128                 comb += Assert(wr_rel == 0)
 129
 130
 131             # Property 10: Similar to property 6, wr_rel should be
 132             # deasserted when go_die is asserted
 133             with m.If(Past(wr_rel) & Past(go_die)):
 134                 comb += Assert(wr_rel == 0)
 135
 136             # Property 11: wr_rel should not fall while shadow is
 137             # asserted
 138             with m.If(wr_rel & shadow):
 139                 comb += Assert(~Fell(wr_rel))
 140
 141             # Assume no instruction is issued until rd_rel is
 142             # released. Idk if this is valid
 143
 144             with m.If(busy):
 145                 comb += Assume(issue == 0)
 146
 147         return m
 148
 149 class FUTestCase(FHDLTestCase):
 150     def test_formal(self):
 151         module = Driver()
 152         self.assertFormal(module, mode="bmc", depth=5)
 153         self.assertFormal(module, mode="cover", depth=5)
 154     def test_ilang(self):
 155         dut = MultiCompUnit(16, DummyALU(16), CompALUOpSubset)
 156         vl = rtlil.convert(dut, ports=dut.ports())
 157         with open("multicompunit.il", "w") as f:
 158             f.write(vl)
 159
 160
 161 if __name__ == '__main__':
 162     unittest.main()