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