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

   1 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   2                     signed, ResetSignal)
   3 from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial,
   4                             Rose, Fell, Stable, Past)
   5 from nmigen.test.utils import FHDLTestCase
   6 from nmigen.cli import rtlil
   7 import unittest
   8
   9 from soc.fu.compunits.compunits import FunctionUnitBaseSingle
  10 from soc.experiment.alu_hier import DummyALU
  11 from soc.experiment.compalu_multi import MultiCompUnit
  12 from soc.fu.alu.alu_input_record import CompALUOpSubset
  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         sync = m.d.sync
  22         alu = DummyALU(16)
  23         m.submodules.dut = dut = MultiCompUnit(16, alu,
  24                                                CompALUOpSubset)
  25
  26         go_rd = dut.rd.go
  27         rd_rel = dut.rd.rel
  28         issue = dut.issue_i
  29
  30         go_die = dut.go_die_i
  31
  32         rst = ResetSignal()
  33
  34         init = Initial()
  35
  36         has_issued = Signal(reset=0)
  37
  38
  39
  40         with m.If(init):
  41             comb += Assume(has_issued == 0)
  42             comb += Assume(issue == 0)
  43             comb += Assume(go_rd == 0)
  44             comb += Assume(rst == 1)
  45         with m.Else():
  46             comb += Assume(rst == 0)
  47
  48             # Property One: Rd_rel should never be asserted before issue
  49
  50             # detect when issue has been raised and remember it
  51             with m.If(issue):
  52                 sync += has_issued.eq(1)
  53                 comb += Cover(has_issued)
  54             # If issue has never been raised, then rd_rel should never be raised
  55             with m.If(rd_rel != 0):
  56                 comb += Assert(has_issued)
  57
  58
  59             # Property Two: when rd_rel is asserted, it should stay
  60             # that way until a go_rd
  61             with m.If((Past(go_rd) == 0) & ~Past(go_die)):
  62                 comb += Assert(~Fell(rd_rel))
  63
  64             # Property Three: when a bit in rd_rel is asserted, and
  65             # the corresponding bit in go_rd is asserted, then that
  66             # bit of rd_rel should be deasserted
  67             for i in range(2):
  68                 with m.If(Past(go_rd)[i] & (Past(rd_rel) != 0)):
  69                     comb += Assert(rd_rel[i] == ~Past(go_rd)[i])
  70
  71             # Property Four: Similarly, if rd_rel is asserted,
  72             # asserting go_die should make rd_rel be deasserted
  73
  74             with m.If(Past(rd_rel) != 0):
  75                 with m.If(Past(go_die)):
  76                     comb += Assert(rd_rel == 0)
  77
  78             # Property
  79
  80             comb += Cover(Fell(rd_rel))
  81
  82             # Assume no instruction is issued until rd_rel is
  83             # released. Idk if this is valid
  84
  85             with m.If((rd_rel != 0) | (Past(rd_rel) != 0)):
  86                 comb += Assume(issue == 0)
  87
  88
  89
  90
  91
  92         return m
  93
  94 class FUTestCase(FHDLTestCase):
  95     def test_formal(self):
  96         module = Driver()
  97         self.assertFormal(module, mode="bmc", depth=5)
  98         self.assertFormal(module, mode="cover", depth=5)
  99     def test_ilang(self):
 100         dut = MultiCompUnit(16, DummyALU(16), CompALUOpSubset)
 101         vl = rtlil.convert(dut, ports=dut.ports())
 102         with open("multicompunit.il", "w") as f:
 103             f.write(vl)
 104
 105
 106 if __name__ == '__main__':
 107     unittest.main()