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 and NGI POINTER under EU Grants 871528 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
  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         # Avoid toggling go_i when rel_o is low (rel / go protocol)
 107         rd_go = Signal(dut.n_src)
 108         m.d.comb += dut.cu.rd.go_i.eq(rd_go & dut.cu.rd.rel_o)
 109         wr_go = Signal(dut.n_dst)
 110         m.d.comb += dut.cu.wr.go_i.eq(wr_go & dut.cu.wr.rel_o)
 111         # Transaction counters
 112         do_issue = Signal()
 113         m.d.comb += do_issue.eq(dut.issue_i & ~dut.busy_o)
 114         cnt_issue = Signal(4)
 115         m.d.sync += cnt_issue.eq(cnt_issue + do_issue)
 116         do_read = Signal(dut.n_src)
 117         m.d.comb += do_read.eq(dut.cu.rd.rel_o & dut.cu.rd.go_i)
 118         cnt_read = []
 119         for i in range(dut.n_src):
 120             cnt = Signal(4, name="cnt_read_%d" % i)
 121             m.d.sync += cnt.eq(cnt + do_read[i])
 122             cnt_read.append(cnt)
 123         do_write = Signal(dut.n_dst)
 124         m.d.comb += do_write.eq(dut.cu.wr.rel_o & dut.cu.wr.go_i)
 125         cnt_write = []
 126         for i in range(dut.n_dst):
 127             cnt = Signal(4, name="cnt_write_%d" % i)
 128             m.d.sync += cnt.eq(cnt + do_write[i])
 129             cnt_write.append(cnt)
 130         do_alu_write = Signal()
 131         m.d.comb += do_alu_write.eq(alu.p.i_valid & alu.p.o_ready)
 132         cnt_alu_write = Signal(4)
 133         m.d.sync += cnt_alu_write.eq(cnt_alu_write + do_alu_write)
 134         do_alu_read = Signal()
 135         m.d.comb += do_alu_read.eq(alu.n.o_valid & alu.n.i_ready)
 136         cnt_alu_read = Signal(4)
 137         m.d.sync += cnt_alu_read.eq(cnt_alu_read + do_alu_read)
 138
 139         # Ask the formal engine to give an example
 140         m.d.comb += Cover((cnt_issue == 2)
 141                           & (cnt_read[0] == 1)
 142                           & (cnt_read[1] == 1)
 143                           & (cnt_write[0] == 1)
 144                           & (cnt_write[1] == 1)
 145                           & (cnt_alu_write == 1)
 146                           & (cnt_alu_read == 1))
 147         self.assertFormal(m, mode="cover", depth=10)
 148
 149
 150 if __name__ == "__main__":
 151     unittest.main()