src/soc/experiment/formal/proof_compalu_multi.py

   1 # SPDX-License-Identifier: LGPLv3+
   2 # Copyright (C) 2022 Cesar Strauss <cestrauss@gmail.com>
   3 # Sponsored by NLnet under EU Grant and 957073
   4 # Part of the Libre-SOC Project.
   5
   6 """
   7 Formal proof of soc.experiment.compalu_multi.MultiCompUnit
   8
   9 In short, MultiCompUnit:
  10
  11 1) stores an opcode from Issue, when not "busy", and "issue" is pulsed
  12 2) signals "busy" high
  13 3) fetches its operand(s), if any (which are not masked or zero) from the
  14 Scoreboard (REL/GO protocol)
  15 4) starts the ALU (ready/valid protocol), as soon as all inputs are available
  16 5) captures result from ALU (again ready/valid)
  17 5) sends the result(s) back to the Scoreboard (again REL/GO)
  18 6) drops "busy"
  19
  20 Note that, if the conditions are right, many of the above can occur together,
  21 on a single cycle.
  22
  23 The formal proof involves ensuring that:
  24 1) the ALU gets the right opcode from Issue
  25 2) the ALU gets the right operands from the Scoreboard
  26 3) the Scoreboard receives the right result from the ALU
  27 4) no transactions are dropped or repeated
  28
  29 This can be checked using holding registers and transaction counters.
  30
  31 See https://bugs.libre-soc.org/show_bug.cgi?id=879 and
  32 https://bugs.libre-soc.org/show_bug.cgi?id=197
  33 """
  34
  35 import unittest
  36
  37 from nmigen import Signal, Module
  38 from nmigen.hdl.ast import Cover, Const, Assume, Assert
  39 from nmutil.formaltest import FHDLTestCase
  40 from nmutil.singlepipe import ControlBase
  41
  42 from soc.experiment.compalu_multi import MultiCompUnit
  43 from soc.fu.alu.alu_input_record import CompALUOpSubset
  44
  45
  46 # Formal model of a simple ALU, whose inputs and outputs are randomly
  47 # generated by the formal engine
  48
  49 class ALUCtx:
  50     def __init__(self):
  51         self.op = CompALUOpSubset(name="op")
  52
  53
  54 class ALUInput:
  55     def __init__(self):
  56         self.a = Signal(16)
  57         self.b = Signal(16)
  58         self.ctx = ALUCtx()
  59
  60     def eq(self, i):
  61         return [self.a.eq(i.a), self.b.eq(i.b)]
  62
  63
  64 class ALUOutput:
  65     def __init__(self):
  66         self.o1 = Signal(16)
  67         self.o2 = Signal(16)
  68
  69     def eq(self, i):
  70         return [self.o1.eq(i.o1), self.o2.eq(i.o2)]
  71
  72
  73 class ALU(ControlBase):
  74     def __init__(self):
  75         super().__init__(stage=self)
  76         self.p.i_data, self.n.o_data = self.new_specs(None)
  77         self.i, self.o = self.p.i_data, self.n.o_data
  78
  79     def setup(self, m, i):
  80         pass
  81
  82     def ispec(self, name=None):
  83         return ALUInput()
  84
  85     def ospec(self, name=None):
  86         return ALUOutput()
  87
  88     def elaborate(self, platform):
  89         m = super().elaborate(platform)
  90         return m
  91
  92
  93 class CompALUMultiTestCase(FHDLTestCase):
  94     def test_formal(self):
  95         inspec = [('INT', 'a', '0:15'),
  96                   ('INT', 'b', '0:15')]
  97         outspec = [('INT', 'o1', '0:15'),
  98                    ('INT', 'o2', '0:15')]
  99         regspec = (inspec, outspec)
 100         m = Module()
 101         # Instantiate "random" ALU
 102         alu = ALU()
 103         m.submodules.dut = dut = MultiCompUnit(regspec, alu, CompALUOpSubset)
 104         # TODO Test shadow / die
 105         m.d.comb += [dut.shadown_i.eq(1), dut.go_die_i.eq(0)]
 106         # Don't issue while busy
 107         issue = Signal()
 108         m.d.comb += dut.issue_i.eq(issue & ~dut.busy_o)
 109         # Avoid toggling go_i when rel_o is low (rel / go protocol)
 110         rd_go = Signal(dut.n_src)
 111         m.d.comb += dut.cu.rd.go_i.eq(rd_go & dut.cu.rd.rel_o)
 112         wr_go = Signal(dut.n_dst)
 113         m.d.comb += dut.cu.wr.go_i.eq(wr_go & dut.cu.wr.rel_o)
 114         # Transaction counters
 115         do_issue = Signal()
 116         m.d.comb += do_issue.eq(dut.issue_i & ~dut.busy_o)
 117         cnt_issue = Signal(4)
 118         m.d.sync += cnt_issue.eq(cnt_issue + do_issue)
 119         do_read = Signal(dut.n_src)
 120         m.d.comb += do_read.eq(dut.cu.rd.rel_o & dut.cu.rd.go_i)
 121         cnt_read = []
 122         for i in range(dut.n_src):
 123             cnt = Signal(4, name="cnt_read_%d" % i)
 124             m.d.sync += cnt.eq(cnt + do_read[i])
 125             cnt_read.append(cnt)
 126         do_write = Signal(dut.n_dst)
 127         m.d.comb += do_write.eq(dut.cu.wr.rel_o & dut.cu.wr.go_i)
 128         cnt_write = []
 129         for i in range(dut.n_dst):
 130             cnt = Signal(4, name="cnt_write_%d" % i)
 131             m.d.sync += cnt.eq(cnt + do_write[i])
 132             cnt_write.append(cnt)
 133         do_alu_write = Signal()
 134         m.d.comb += do_alu_write.eq(alu.p.i_valid & alu.p.o_ready)
 135         cnt_alu_write = Signal(4)
 136         m.d.sync += cnt_alu_write.eq(cnt_alu_write + do_alu_write)
 137         do_alu_read = Signal()
 138         m.d.comb += do_alu_read.eq(alu.n.o_valid & alu.n.i_ready)
 139         cnt_alu_read = Signal(4)
 140         m.d.sync += cnt_alu_read.eq(cnt_alu_read + do_alu_read)
 141         cnt_masked_read = []
 142         do_masked_read = Signal(dut.n_src)
 143         for i in range(dut.n_src):
 144             cnt = Signal(4, name="cnt_masked_read_%d" % i)
 145             if i == 0:
 146                 extra = dut.oper_i.zero_a
 147             elif i == 1:
 148                 extra = dut.oper_i.imm_data.ok
 149             else:
 150                 extra = Const(0, 1)
 151             m.d.comb += do_masked_read[i].eq(do_issue &
 152                                              (dut.rdmaskn[i] | extra))
 153             m.d.sync += cnt.eq(cnt + do_masked_read[i])
 154             cnt_masked_read.append(cnt)
 155         # If the ALU is idle, do not assert valid
 156         with m.If(cnt_alu_read == cnt_alu_write):
 157             m.d.comb += Assume(~alu.n.o_valid)
 158         # Keep ALU valid high, until read
 159         last_alu_valid = Signal()
 160         m.d.sync += last_alu_valid.eq(alu.n.o_valid & ~alu.n.i_ready)
 161         with m.If(last_alu_valid):
 162             m.d.comb += Assume(alu.n.o_valid)
 163
 164         # Invariant checks
 165
 166         # For every instruction issued, at any point in time,
 167         # each operand was either:
 168         # 1) Already read
 169         # 2) Not read yet, but the read is pending (rel_o high)
 170         # 3) Masked
 171         for i in range(dut.n_src):
 172             sum_read = Signal(4)
 173             m.d.comb += sum_read.eq(
 174                 cnt_read[i] + cnt_masked_read[i] + dut.cu.rd.rel_o[i])
 175             m.d.comb += Assert(sum_read == cnt_issue)
 176
 177         # For every instruction, either:
 178         # 1) The ALU is executing the instruction
 179         # 2) Otherwise, execution is pending (alu.p.i_valid is high)
 180         # 3) Otherwise, it is waiting for operands
 181         #    (some dut.cu.rd.rel_o are still high)
 182         # 4) ... unless all operands are masked, in which case there is a one
 183         #    cycle delay
 184         all_masked = Signal()
 185         m.d.sync += all_masked.eq(do_masked_read.all())
 186         sum_alu_write = Signal(4)
 187         m.d.comb += sum_alu_write.eq(
 188             cnt_alu_write +
 189             (dut.cu.rd.rel_o.any() | all_masked | alu.p.i_valid))
 190         m.d.comb += Assert(sum_alu_write == cnt_issue)
 191
 192         # Ask the formal engine to give an example
 193         m.d.comb += Cover((cnt_issue == 2)
 194                           & (cnt_read[0] == 1)
 195                           & (cnt_read[1] == 0)
 196                           & (cnt_write[0] == 1)
 197                           & (cnt_write[1] == 1)
 198                           & (cnt_alu_write == 1)
 199                           & (cnt_alu_read == 1)
 200                           & (cnt_masked_read[0] == 1)
 201                           & (cnt_masked_read[1] == 1))
 202         with self.subTest("cover"):
 203             self.assertFormal(m, mode="cover", depth=10)
 204
 205         # Check assertions
 206         with self.subTest("bmc"):
 207             self.assertFormal(m, mode="bmc", depth=10)
 208
 209
 210 if __name__ == "__main__":
 211     unittest.main()