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.
7 Formal proof of soc.experiment.compalu_multi.MultiCompUnit
9 In short, MultiCompUnit:
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)
20 Note that, if the conditions are right, many of the above can occur together,
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
29 This can be checked using holding registers and transaction counters.
31 See https://bugs.libre-soc.org/show_bug.cgi?id=879 and
32 https://bugs.libre-soc.org/show_bug.cgi?id=197
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
42 from soc
.experiment
.compalu_multi
import MultiCompUnit
43 from soc
.fu
.alu
.alu_input_record
import CompALUOpSubset
46 # Formal model of a simple ALU, whose inputs and outputs are randomly
47 # generated by the formal engine
51 self
.op
= CompALUOpSubset(name
="op")
61 return [self
.a
.eq(i
.a
), self
.b
.eq(i
.b
)]
70 return [self
.o1
.eq(i
.o1
), self
.o2
.eq(i
.o2
)]
73 class ALU(ControlBase
):
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
79 def setup(self
, m
, i
):
82 def ispec(self
, name
=None):
85 def ospec(self
, name
=None):
88 def elaborate(self
, platform
):
89 m
= super().elaborate(platform
)
93 class CompALUMultiTestCase(FHDLTestCase
):
94 def test_formal(self
):
95 inspec
= [('INT', 'a', '0:15'),
97 outspec
= [('INT', 'o1', '0:15'),
98 ('INT', 'o2', '0:15')]
99 regspec
= (inspec
, outspec
)
101 # Instantiate "random" 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
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
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
)
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
])
126 do_write
= Signal(dut
.n_dst
)
127 m
.d
.comb
+= do_write
.eq(dut
.cu
.wr
.rel_o
& dut
.cu
.wr
.go_i
)
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
)
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
)
146 extra
= dut
.oper_i
.zero_a
148 extra
= dut
.oper_i
.imm_data
.ok
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
) & ~do_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
)
166 # For every instruction issued, at any point in time,
167 # each operand was either:
169 # 2) Not read yet, but the read is pending (rel_o high)
171 for i
in range(dut
.n_src
):
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
)
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
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(
189 (dut
.cu
.rd
.rel_o
.any() | all_masked | alu
.p
.i_valid
))
190 m
.d
.comb
+= Assert(sum_alu_write
== cnt_issue
)
192 # Ask the formal engine to give an example
193 m
.d
.comb
+= Cover((cnt_issue
== 2)
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)
206 with self
.subTest("bmc"):
207 self
.assertFormal(m
, mode
="bmc", depth
=10)
210 if __name__
== "__main__":