--- /dev/null
+# SPDX-License-Identifier: LGPLv3+
+# Copyright (C) 2022 Cesar Strauss <cestrauss@gmail.com>
+# Sponsored by NLnet and NGI POINTER under EU Grants 871528 and 957073
+# Part of the Libre-SOC Project.
+
+"""
+Formal proof of soc.experiment.compalu_multi.MultiCompUnit
+
+In short, MultiCompUnit:
+
+1) stores an opcode from Issue, when not "busy", and "issue" is pulsed
+2) signals "busy" high
+3) fetches its operand(s), if any (which are not masked or zero) from the
+Scoreboard (REL/GO protocol)
+4) starts the ALU (ready/valid protocol), as soon as all inputs are available
+5) captures result from ALU (again ready/valid)
+5) sends the result(s) back to the Scoreboard (again REL/GO)
+6) drops "busy"
+
+Note that, if the conditions are right, many of the above can occur together,
+on a single cycle.
+
+The formal proof involves ensuring that:
+1) the ALU gets the right opcode from Issue
+2) the ALU gets the right operands from the Scoreboard
+3) the Scoreboard receives the right result from the ALU
+4) no transactions are dropped or repeated
+
+This can be checked using holding registers and transaction counters.
+
+See https://bugs.libre-soc.org/show_bug.cgi?id=879 and
+https://bugs.libre-soc.org/show_bug.cgi?id=197
+"""
+
+import unittest
+
+from nmigen import Signal, Module
+from nmigen.hdl.ast import Cover
+from nmutil.formaltest import FHDLTestCase
+from nmutil.singlepipe import ControlBase
+
+from soc.experiment.compalu_multi import MultiCompUnit
+from soc.fu.alu.alu_input_record import CompALUOpSubset
+
+
+# Formal model of a simple ALU, whose inputs and outputs are randomly
+# generated by the formal engine
+
+class ALUCtx:
+ def __init__(self):
+ self.op = CompALUOpSubset(name="op")
+
+
+class ALUInput:
+ def __init__(self):
+ self.a = Signal(16)
+ self.b = Signal(16)
+ self.ctx = ALUCtx()
+
+ def eq(self, i):
+ return [self.a.eq(i.a), self.b.eq(i.b)]
+
+
+class ALUOutput:
+ def __init__(self):
+ self.o1 = Signal(16)
+ self.o2 = Signal(16)
+
+ def eq(self, i):
+ return [self.o1.eq(i.o1), self.o2.eq(i.o2)]
+
+
+class ALU(ControlBase):
+ def __init__(self):
+ super().__init__(stage=self)
+ self.p.i_data, self.n.o_data = self.new_specs(None)
+ self.i, self.o = self.p.i_data, self.n.o_data
+
+ def setup(self, m, i):
+ pass
+
+ def ispec(self, name=None):
+ return ALUInput()
+
+ def ospec(self, name=None):
+ return ALUOutput()
+
+ def elaborate(self, platform):
+ m = super().elaborate(platform)
+ return m
+
+
+class CompALUMultiTestCase(FHDLTestCase):
+ def test_formal(self):
+ inspec = [('INT', 'a', '0:15'),
+ ('INT', 'b', '0:15')]
+ outspec = [('INT', 'o1', '0:15'),
+ ('INT', 'o2', '0:15')]
+ regspec = (inspec, outspec)
+ m = Module()
+ # Instantiate "random" ALU
+ alu = ALU()
+ m.submodules.dut = dut = MultiCompUnit(regspec, alu, CompALUOpSubset)
+ # Transaction counters
+ do_issue = Signal()
+ m.d.comb += do_issue.eq(dut.issue_i & ~dut.busy_o)
+ cnt_issue = Signal(4)
+ m.d.sync += cnt_issue.eq(cnt_issue + do_issue)
+ # Ask the formal engine to give an example
+ m.d.comb += Cover(cnt_issue == 2)
+ self.assertFormal(m, mode="cover", depth=4)
+
+
+if __name__ == "__main__":
+ unittest.main()