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         for i in range(dut.n_src):
 143             cnt = Signal(4, name="cnt_masked_read_%d" % i)
 144             if i == 0:
 145                 extra = dut.oper_i.zero_a
 146             elif i == 1:
 147                 extra = dut.oper_i.imm_data.ok
 148             else:
 149                 extra = Const(0, 1)
 150             m.d.sync += cnt.eq(cnt + (do_issue & (dut.rdmaskn[i] | extra)))
 151             cnt_masked_read.append(cnt)
 152         # If the ALU is idle, do not assert valid
 153         with m.If(cnt_alu_read == cnt_alu_write):
 154             m.d.comb += Assume(~alu.n.o_valid)
 155
 156         # Invariant check
 157         # For every instruction issued, at any point in time,
 158         # each operand was either:
 159         # 1) Already read
 160         # 2) Not read yet, but the read is pending (rel_o high)
 161         # 3) Masked
 162         for i in range(dut.n_src):
 163             sum_read = Signal(4)
 164             m.d.comb += sum_read.eq(
 165                 cnt_read[i] + cnt_masked_read[i] + dut.cu.rd.rel_o[i])
 166             m.d.comb += Assert(sum_read == cnt_issue)
 167
 168         # Ask the formal engine to give an example
 169         m.d.comb += Cover((cnt_issue == 2)
 170                           & (cnt_read[0] == 1)
 171                           & (cnt_read[1] == 0)
 172                           & (cnt_write[0] == 1)
 173                           & (cnt_write[1] == 1)
 174                           & (cnt_alu_write == 1)
 175                           & (cnt_alu_read == 1)
 176                           & (cnt_masked_read[0] == 1)
 177                           & (cnt_masked_read[1] == 1))
 178         with self.subTest("cover"):
 179             self.assertFormal(m, mode="cover", depth=10)
 180
 181         # Check assertions
 182         with self.subTest("bmc"):
 183             self.assertFormal(m, mode="bmc", depth=10)
 184
 185
 186 if __name__ == "__main__":
 187     unittest.main()