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 nmutil.gtkw import write_gtkw
  13 from nmigen.cli import rtlil
  14 import unittest
  15 import os
  16
  17 from soc.fu.compunits.compunits import FunctionUnitBaseSingle
  18 from soc.experiment.alu_hier import DummyALU
  19 from soc.experiment.compalu_multi import MultiCompUnit
  20 from soc.fu.cr.cr_input_record import CompCROpSubset
  21
  22
  23 class Driver(Elaboratable):
  24     def __init__(self):
  25         pass
  26
  27     def elaborate(self, platform):
  28         m = Module()
  29         comb = m.d.comb
  30         sync = m.d.sync
  31         inspec = [('INT', 'a', '0:15'),
  32                   ('INT', 'b', '0:15'),
  33                   ('INT', 'c', '0:15')]
  34         outspec = [('INT', 'o', '0:15')]
  35
  36         regspec = (inspec, outspec)
  37         alu = DummyALU(16)
  38         m.submodules.dut = dut = MultiCompUnit(regspec, alu, CompCROpSubset)
  39
  40         issue = dut.issue_i
  41         busy = dut.busy_o
  42
  43         go_rd = dut.rd.go_i
  44         rd_rel = dut.rd.rel_o
  45
  46         go_wr = dut.wr.go_i
  47         wr_rel = dut.wr.rel_o
  48
  49         go_die = dut.go_die_i
  50         shadow_n = dut.shadown_i
  51
  52         rst = ResetSignal()
  53
  54         init = Initial()
  55
  56         has_issued = Signal(reset=0)
  57
  58         with m.If(init):
  59             comb += Assume(has_issued == 0)
  60             comb += Assume(issue == 0)
  61             comb += Assume(go_rd == 0)
  62             comb += Assume(rst == 1)
  63         with m.Else():
  64             comb += Assume(rst == 0)
  65
  66             # Property 1: When issue is first raised, a busy signal is
  67             # sent out. The operand can be latched in at this point
  68             # (rd_rel and go_rd are allowed to be high)
  69
  70             # Busy should rise after issue.
  71             with m.If(Past(issue)):
  72                 comb += Assert(Rose(busy))
  73
  74             # Instructions should not be issued if busy == 1
  75             with m.If(busy):
  76                 comb += Assume(issue == 0)
  77
  78             # Property 2: Issue will only be raised for one
  79             # cycle. Read requests may go out immediately after issue
  80             # goes low
  81
  82
  83             # The read_request should not happen while the unit is not busy
  84             with m.If(~busy):
  85                 comb += Assert(rd_rel == 0)
  86
  87             # Property 3: Read request is sent, which is acknowledged
  88             # through the scoreboard to the priority picker which
  89             # generates one go_read at a time. One of those will
  90             # eventually be this computation unit
  91
  92             # there cannot be a go_rd if rd_rel is clear
  93             with m.If(rd_rel == 0):
  94                 comb += Assume(go_rd == 0)
  95
  96             # Property 4: Once Go_Read is set, the src1/src2/operand
  97             # latch door shuts and the ALU is told to proceed
  98
  99             # When a go_rd is received for each operand, the data
 100             # should be captured
 101             with m.If(~Past(go_die)):
 102                 with m.If(Past(go_rd)[0] & Past(rd_rel)[0]):
 103                     comb += Assert(dut.alu.a == Past(dut.src1_i))
 104                 with m.If(Past(go_rd)[1] & Past(rd_rel)[1]):
 105                     comb += Assert(dut.alu.b == Past(dut.src2_i))
 106
 107             # Property 5: When the ALU pipeline is ready, this
 108             # activates write_request release and the ALU's output is
 109             # captured in a temporary register
 110
 111             # I can't see the actual temporary register, so I have to
 112             # simulate it here. This will be checked when the ALU data
 113             # is actually output
 114             alu_temp = Signal(16)
 115             write_req_valid = Signal(reset=0)
 116             with m.If(~Past(go_die) & Past(busy)):
 117                 with m.If(Rose(dut.alu.n.valid_o)):
 118                     sync += alu_temp.eq(dut.alu.o)
 119                     sync += write_req_valid.eq(1)
 120
 121             # write_req_valid should only be high once the alu finishes
 122             with m.If(~write_req_valid & ~dut.alu.n.valid_o):
 123                 comb += Assert(wr_rel == 0)
 124
 125             # Property 6: Write request release is held up if shadow_n
 126             # is asserted low
 127
 128             # If shadow_n is low (indicating that everything is
 129             # shadowed), wr_rel should not be able to rise
 130             with m.If(shadow_n == 0):
 131                 with m.If(Past(wr_rel) == 0):
 132                     comb += Assert(wr_rel == 0)
 133
 134             # Property 7: Write request release will go through a
 135             # similar process as read request, resulting (eventually
 136             # in go_write being asserted
 137
 138             # Go_wr should not be asserted if wr_rel is not
 139             with m.If(wr_rel == 0):
 140                 comb += Assume(go_wr == 0)
 141
 142
 143             # Property 8: When go_write is asserted, two things
 144             # happen. 1 - the data in the temp register is placed
 145             # combinatorially onto the output. And 2 - the req_l latch
 146             # is cleared, busy is dropped, and the comp unit is ready
 147             # to do another task
 148
 149             # If a write release is accepted (by asserting go_wr),
 150             # then the alu data should be output
 151             with m.If(Past(wr_rel) & Past(go_wr)):
 152                 # the alu data is output
 153                 comb += Assert((dut.data_o == alu_temp) | (dut.data_o == dut.alu.o))
 154                 # wr_rel is dropped
 155                 comb += Assert(wr_rel == 0)
 156                 # busy is dropped.
 157                 with m.If(~Past(go_die)):
 158                     comb += Assert(busy == 0)
 159
 160
 161         # It is REQUIRED that issue be held valid only for one cycle
 162         with m.If(Past(issue)):
 163             comb += Assume(issue == 0)
 164
 165         # It is REQUIRED that GO_Read be held valid only for one
 166         # cycle, and it is REQUIRED that the corresponding read_req be
 167         # dropped exactly one cycle after go_read is asserted high
 168
 169         for i in range(2):
 170             with m.If(Past(go_rd)[i] & Past(rd_rel)[i]):
 171                 comb += Assume(go_rd[i] == 0)
 172                 comb += Assert(rd_rel[i] == 0)
 173
 174         # Likewise for go_write/wr_rel
 175         with m.If(Past(go_wr) & Past(wr_rel)):
 176             comb += Assume(go_wr == 0)
 177             comb += Assert(wr_rel == 0)
 178
 179         # When go_die is asserted the the entire FSM should be fully
 180         # reset.
 181
 182         with m.If(Past(go_die) & Past(busy)):
 183             comb += Assert(rd_rel == 0)
 184             # this doesn't work?
 185             # comb += Assert(wr_rel == 0)
 186             sync += write_req_valid.eq(0)
 187
 188         return m
 189
 190
 191 class FUTestCase(FHDLTestCase):
 192     def test_formal(self):
 193         style = {
 194             'in': {'color': 'orange'},
 195             'out': {'color': 'yellow'},
 196         }
 197         traces = [
 198             'clk',
 199             ('operation port', {'color': 'red'}, [
 200                 'cu_issue_i', 'cu_busy_o',
 201                 {'comment': 'shadow / go_die'},
 202                 'cu_shadown_i','cu_go_die_i']),
 203             ('operand 1 port', 'in', [
 204                 ('cu_rd__rel_o[2:0]', {'bit': 2}),
 205                 ('cu_rd__go_i[2:0]', {'bit': 2}),
 206                 'src1_i[15:0]']),
 207             ('operand 2 port', 'in', [
 208                 ('cu_rd__rel_o[2:0]', {'bit': 1}),
 209                 ('cu_rd__go_i[2:0]', {'bit': 1}),
 210                 'src2_i[15:0]']),
 211             ('operand 3 port', 'in', [
 212                 ('cu_rd__rel_o[2:0]', {'bit': 0}),
 213                 ('cu_rd__go_i[2:0]', {'bit': 0}),
 214                 'src1_i[15:0]']),
 215             ('result port', 'out', [
 216                 'cu_wr__rel_o', 'cu_wr__go_i', 'dest1_o[15:0]']),
 217             ('alu', {'submodule': 'alu'}, [
 218                 ('prev port', 'in', [
 219                     'oper_i_None__insn_type', 'i1[15:0]',
 220                     'valid_i', 'ready_o']),
 221                 ('next port', 'out', [
 222                     'alu_o[15:0]', 'valid_o', 'ready_i'])])]
 223
 224         write_gtkw('test_fu_formal_bmc.gtkw',
 225                    os.path.dirname(__file__) +
 226                    '/proof_fu_formal/engine_0/trace.vcd',
 227                    traces, style,
 228                    clk_period=10e-9,
 229                    time_resolution_unit="ns",
 230                    module='top.dut')
 231
 232         module = Driver()
 233         self.assertFormal(module, mode="bmc", depth=10)
 234         self.assertFormal(module, mode="cover", depth=10)
 235     def test_ilang(self):
 236         inspec = [('INT', 'a', '0:15'),
 237                   ('INT', 'b', '0:15'),
 238                   ('INT', 'c', '0:15')]
 239         outspec = [('INT', 'o', '0:15')]
 240
 241         regspec = (inspec, outspec)
 242         dut = MultiCompUnit(regspec, DummyALU(16), CompCROpSubset)
 243         vl = rtlil.convert(dut, ports=dut.ports())
 244         with open("multicompunit.il", "w") as f:
 245             f.write(vl)
 246
 247
 248 if __name__ == '__main__':
 249     unittest.main()