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 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   8                     signed, ResetSignal)
   9 from nmigen.asserts import (Assert, AnyConst, Assume, Cover, Initial,
  10                             Rose, Fell, Stable, Past)
  11 from nmigen.test.utils import FHDLTestCase
  12 from nmigen.cli import rtlil
  13 import unittest
  14
  15 from soc.fu.compunits.compunits import FunctionUnitBaseSingle
  16 from soc.experiment.alu_hier import DummyALU
  17 from soc.experiment.compalu_multi import MultiCompUnit
  18 from soc.fu.alu.alu_input_record import CompALUOpSubset
  19
  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, CompALUOpSubset)
  31
  32         issue = dut.issue_i
  33         busy = dut.busy_o
  34
  35         go_rd = dut.rd.go
  36         rd_rel = dut.rd.rel
  37
  38         go_wr = dut.wr.go
  39         wr_rel = dut.wr.rel
  40
  41         go_die = dut.go_die_i
  42         shadow_n = dut.shadown_i
  43
  44         rst = ResetSignal()
  45
  46         init = Initial()
  47
  48         has_issued = Signal(reset=0)
  49
  50         with m.If(init):
  51             comb += Assume(has_issued == 0)
  52             comb += Assume(issue == 0)
  53             comb += Assume(go_rd == 0)
  54             comb += Assume(rst == 1)
  55         with m.Else():
  56             comb += Assume(rst == 0)
  57
  58             # Property 1: When issue is first raised, a busy signal is
  59             # sent out. The operand can be latched in at this point
  60             # (rd_rel and go_rd are allowed to be high)
  61
  62             # Busy should rise after issue.
  63             with m.If(Past(issue)):
  64                 comb += Assert(Rose(busy))
  65
  66             # Instructions should not be issued if busy == 1
  67             with m.If(busy):
  68                 comb += Assume(issue == 0)
  69
  70             # Property 2: Issue will only be raised for one
  71             # cycle. Read requests may go out immediately after issue
  72             # goes low
  73
  74
  75             # The read_request should not happen while the unit is not busy
  76             with m.If(~busy):
  77                 comb += Assert(rd_rel == 0)
  78
  79             # Property 3: Read request is sent, which is acknowledged
  80             # through the scoreboard to the priority picker which
  81             # generates one go_read at a time. One of those will
  82             # eventually be this computation unit
  83
  84             # there cannot be a go_rd if rd_rel is clear
  85             with m.If(rd_rel == 0):
  86                 comb += Assume(go_rd == 0)
  87
  88             # Property 4: Once Go_Read is set, the src1/src2/operand
  89             # latch door shuts and the ALU is told to proceed
  90
  91             # When a go_rd is received for each operand, the data
  92             # should be captured
  93             with m.If(~Past(go_die)):
  94                 with m.If(Past(go_rd)[0] & Past(rd_rel)[0]):
  95                     comb += Assert(dut.alu.a == Past(dut.src1_i))
  96                 with m.If(Past(go_rd)[1] & Past(rd_rel)[1]):
  97                     comb += Assert(dut.alu.b == Past(dut.src2_i))
  98
  99             # Property 5: When the ALU pipeline is ready, this
 100             # activates write_request release and the ALU's output is
 101             # captured in a temporary register
 102
 103             # I can't see the actual temporary register, so I have to
 104             # simulate it here. This will be checked when the ALU data
 105             # is actually output
 106             alu_temp = Signal(16)
 107             write_req_valid = Signal(reset=0)
 108             with m.If(~Past(go_die) & Past(busy)):
 109                 with m.If(Rose(dut.alu.n.valid_o)):
 110                     sync += alu_temp.eq(dut.alu.o)
 111                     sync += write_req_valid.eq(1)
 112
 113             # write_req_valid should only be high once the alu finishes
 114             with m.If(~write_req_valid & ~dut.alu.n.valid_o):
 115                 comb += Assert(wr_rel == 0)
 116
 117             # Property 6: Write request release is held up if shadow_n
 118             # is asserted low
 119
 120             # If shadow_n is low (indicating that everything is
 121             # shadowed), wr_rel should not be able to rise
 122             with m.If(shadow_n == 0):
 123                 with m.If(Past(wr_rel) == 0):
 124                     comb += Assert(wr_rel == 0)
 125
 126             # Property 7: Write request release will go through a
 127             # similar process as read request, resulting (eventually
 128             # in go_write being asserted
 129
 130             # Go_wr should not be asserted if wr_rel is not
 131             with m.If(wr_rel == 0):
 132                 comb += Assume(go_wr == 0)
 133
 134
 135             # Property 8: When go_write is asserted, two things
 136             # happen. 1 - the data in the temp register is placed
 137             # combinatorially onto the output. And 2 - the req_l latch
 138             # is cleared, busy is dropped, and the comp unit is ready
 139             # to do another task
 140
 141             # If a write release is accepted (by asserting go_wr),
 142             # then the alu data should be output
 143             with m.If(Past(wr_rel) & Past(go_wr)):
 144                 # the alu data is output
 145                 comb += Assert((dut.data_o == alu_temp) | (dut.data_o == dut.alu.o))
 146                 # wr_rel is dropped
 147                 comb += Assert(wr_rel == 0)
 148                 # busy is dropped.
 149                 with m.If(~Past(go_die)):
 150                     comb += Assert(busy == 0)
 151
 152
 153         # It is REQUIRED that issue be held valid only for one cycle
 154         with m.If(Past(issue)):
 155             comb += Assume(issue == 0)
 156
 157         # It is REQUIRED that GO_Read be held valid only for one
 158         # cycle, and it is REQUIRED that the corresponding read_req be
 159         # dropped exactly one cycle after go_read is asserted high
 160
 161         for i in range(2):
 162             with m.If(Past(go_rd)[i] & Past(rd_rel)[i]):
 163                 comb += Assume(go_rd[i] == 0)
 164                 comb += Assert(rd_rel[i] == 0)
 165
 166         # Likewise for go_write/wr_rel
 167         with m.If(Past(go_wr) & Past(wr_rel)):
 168             comb += Assume(go_wr == 0)
 169             comb += Assert(wr_rel == 0)
 170
 171         # When go_die is asserted the the entire FSM should be fully
 172         # reset.
 173
 174         with m.If(Past(go_die) & Past(busy)):
 175             comb += Assert(rd_rel == 0)
 176             # this doesn't work?
 177             # comb += Assert(wr_rel == 0)
 178             sync += write_req_valid.eq(0)
 179
 180         return m
 181
 182
 183 class FUTestCase(FHDLTestCase):
 184     def test_formal(self):
 185         module = Driver()
 186         self.assertFormal(module, mode="bmc", depth=10)
 187         self.assertFormal(module, mode="cover", depth=10)
 188     def test_ilang(self):
 189         dut = MultiCompUnit(16, DummyALU(16), CompALUOpSubset)
 190         vl = rtlil.convert(dut, ports=dut.ports())
 191         with open("multicompunit.il", "w") as f:
 192             f.write(vl)
 193
 194
 195 if __name__ == '__main__':
 196     unittest.main()