Start of formal proof of MultiCompUnit
[soc.git] / 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 # Transaction counters
105 do_issue = Signal()
106 m.d.comb += do_issue.eq(dut.issue_i & ~dut.busy_o)
107 cnt_issue = Signal(4)
108 m.d.sync += cnt_issue.eq(cnt_issue + do_issue)
109 # Ask the formal engine to give an example
110 m.d.comb += Cover(cnt_issue == 2)
111 self.assertFormal(m, mode="cover", depth=4)
112
113
114 if __name__ == "__main__":
115 unittest.main()