1 # This is the proof for the computation unit/Function Unit/ALU
2 # manager. Description here:
3 # https://libre-soc.org/3d_gpu/architecture/compunit/
5 # This attempts to prove most of the bullet points on that page
7 from nmigen
import (Module
, Signal
, Elaboratable
, Mux
, Cat
, Repl
,
9 from nmigen
.asserts
import (Assert
, AnyConst
, Assume
, Cover
, Initial
,
10 Rose
, Fell
, Stable
, Past
)
11 from nmutil
.formaltest
import FHDLTestCase
12 from nmutil
.gtkw
import write_gtkw
13 from nmigen
.cli
import rtlil
17 from soc
.fu
.compunits
.compunits
import FunctionUnitBaseSingle
18 from soc
.experiment
.alu_hier
import DummyALU
19 from soc
.experiment
.compalu_multi
import MultiCompUnit
20 from soc
.fu
.cr
.cr_input_record
import CompCROpSubset
23 class Driver(Elaboratable
):
27 def elaborate(self
, platform
):
31 inspec
= [('INT', 'a', '0:15'),
34 outspec
= [('INT', 'o', '0:15')]
36 regspec
= (inspec
, outspec
)
38 m
.submodules
.dut
= dut
= MultiCompUnit(regspec
, alu
, CompCROpSubset
)
50 shadow_n
= dut
.shadown_i
56 has_issued
= Signal(reset
=0)
59 comb
+= Assume(has_issued
== 0)
60 comb
+= Assume(issue
== 0)
61 comb
+= Assume(go_rd
== 0)
62 comb
+= Assume(rst
== 1)
64 comb
+= Assume(rst
== 0)
66 # Property 1: When issue is first raised, a busy signal is
67 # sent out. The operand can be latched in at this point
68 # (rd_rel and go_rd are allowed to be high)
70 # Busy should rise after issue.
71 with m
.If(Past(issue
)):
72 comb
+= Assert(Rose(busy
))
74 # Instructions should not be issued if busy == 1
76 comb
+= Assume(issue
== 0)
78 # Property 2: Issue will only be raised for one
79 # cycle. Read requests may go out immediately after issue
83 # The read_request should not happen while the unit is not busy
85 comb
+= Assert(rd_rel
== 0)
87 # Property 3: Read request is sent, which is acknowledged
88 # through the scoreboard to the priority picker which
89 # generates one go_read at a time. One of those will
90 # eventually be this computation unit
92 # there cannot be a go_rd if rd_rel is clear
93 with m
.If(rd_rel
== 0):
94 comb
+= Assume(go_rd
== 0)
96 # Property 4: Once Go_Read is set, the src1/src2/operand
97 # latch door shuts and the ALU is told to proceed
99 # When a go_rd is received for each operand, the data
101 with m
.If(~
Past(go_die
)):
102 with m
.If(Past(go_rd
)[0] & Past(rd_rel
)[0]):
103 comb
+= Assert(dut
.alu
.a
== Past(dut
.src1_i
))
104 with m
.If(Past(go_rd
)[1] & Past(rd_rel
)[1]):
105 comb
+= Assert(dut
.alu
.b
== Past(dut
.src2_i
))
107 # Property 5: When the ALU pipeline is ready, this
108 # activates write_request release and the ALU's output is
109 # captured in a temporary register
111 # I can't see the actual temporary register, so I have to
112 # simulate it here. This will be checked when the ALU data
114 alu_temp
= Signal(16)
115 write_req_valid
= Signal(reset
=0)
116 with m
.If(~
Past(go_die
) & Past(busy
)):
117 with m
.If(Rose(dut
.alu
.n
.valid_o
)):
118 sync
+= alu_temp
.eq(dut
.alu
.o
)
119 sync
+= write_req_valid
.eq(1)
121 # write_req_valid should only be high once the alu finishes
122 with m
.If(~write_req_valid
& ~dut
.alu
.n
.valid_o
):
123 comb
+= Assert(wr_rel
== 0)
125 # Property 6: Write request release is held up if shadow_n
128 # If shadow_n is low (indicating that everything is
129 # shadowed), wr_rel should not be able to rise
130 with m
.If(shadow_n
== 0):
131 with m
.If(Past(wr_rel
) == 0):
132 comb
+= Assert(wr_rel
== 0)
134 # Property 7: Write request release will go through a
135 # similar process as read request, resulting (eventually
136 # in go_write being asserted
138 # Go_wr should not be asserted if wr_rel is not
139 with m
.If(wr_rel
== 0):
140 comb
+= Assume(go_wr
== 0)
143 # Property 8: When go_write is asserted, two things
144 # happen. 1 - the data in the temp register is placed
145 # combinatorially onto the output. And 2 - the req_l latch
146 # is cleared, busy is dropped, and the comp unit is ready
149 # If a write release is accepted (by asserting go_wr),
150 # then the alu data should be output
151 with m
.If(Past(wr_rel
) & Past(go_wr
)):
152 # the alu data is output
153 comb
+= Assert((dut
.data_o
== alu_temp
) |
(dut
.data_o
== dut
.alu
.o
))
155 comb
+= Assert(wr_rel
== 0)
157 with m
.If(~
Past(go_die
)):
158 comb
+= Assert(busy
== 0)
161 # It is REQUIRED that issue be held valid only for one cycle
162 with m
.If(Past(issue
)):
163 comb
+= Assume(issue
== 0)
165 # It is REQUIRED that GO_Read be held valid only for one
166 # cycle, and it is REQUIRED that the corresponding read_req be
167 # dropped exactly one cycle after go_read is asserted high
170 with m
.If(Past(go_rd
)[i
] & Past(rd_rel
)[i
]):
171 comb
+= Assume(go_rd
[i
] == 0)
172 comb
+= Assert(rd_rel
[i
] == 0)
174 # Likewise for go_write/wr_rel
175 with m
.If(Past(go_wr
) & Past(wr_rel
)):
176 comb
+= Assume(go_wr
== 0)
177 comb
+= Assert(wr_rel
== 0)
179 # When go_die is asserted the the entire FSM should be fully
182 with m
.If(Past(go_die
) & Past(busy
)):
183 comb
+= Assert(rd_rel
== 0)
185 # comb += Assert(wr_rel == 0)
186 sync
+= write_req_valid
.eq(0)
191 class FUTestCase(FHDLTestCase
):
192 def test_formal(self
):
194 'in': {'color': 'orange'},
195 'out': {'color': 'yellow'},
199 ('operation port', {'color': 'red'}, [
200 'cu_issue_i', 'cu_busy_o',
201 {'comment': 'shadow / go_die'},
202 'cu_shadown_i','cu_go_die_i']),
203 ('operand 1 port', 'in', [
204 ('cu_rd__rel_o[2:0]', {'bit': 2}),
205 ('cu_rd__go_i[2:0]', {'bit': 2}),
207 ('operand 2 port', 'in', [
208 ('cu_rd__rel_o[2:0]', {'bit': 1}),
209 ('cu_rd__go_i[2:0]', {'bit': 1}),
211 ('operand 3 port', 'in', [
212 ('cu_rd__rel_o[2:0]', {'bit': 0}),
213 ('cu_rd__go_i[2:0]', {'bit': 0}),
215 ('result port', 'out', [
216 'cu_wr__rel_o', 'cu_wr__go_i', 'dest1_o[15:0]']),
217 ('alu', {'submodule': 'alu'}, [
218 ('prev port', 'in', [
219 'oper_i_None__insn_type', 'i1[15:0]',
220 'valid_i', 'ready_o']),
221 ('next port', 'out', [
222 'alu_o[15:0]', 'valid_o', 'ready_i'])])]
224 write_gtkw('test_fu_formal_bmc.gtkw',
225 os
.path
.dirname(__file__
) +
226 '/proof_fu_formal/engine_0/trace.vcd',
229 time_resolution_unit
="ns",
233 self
.assertFormal(module
, mode
="bmc", depth
=10)
234 self
.assertFormal(module
, mode
="cover", depth
=10)
235 def test_ilang(self
):
236 inspec
= [('INT', 'a', '0:15'),
237 ('INT', 'b', '0:15'),
238 ('INT', 'c', '0:15')]
239 outspec
= [('INT', 'o', '0:15')]
241 regspec
= (inspec
, outspec
)
242 dut
= MultiCompUnit(regspec
, DummyALU(16), CompCROpSubset
)
243 vl
= rtlil
.convert(dut
, ports
=dut
.ports())
244 with
open("multicompunit.il", "w") as f
:
248 if __name__
== '__main__':