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.
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
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 # 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
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
)
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
])
123 do_write
= Signal(dut
.n_dst
)
124 m
.d
.comb
+= do_write
.eq(dut
.cu
.wr
.rel_o
& dut
.cu
.wr
.go_i
)
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
)
135 # Ask the formal engine to give an example
136 m
.d
.comb
+= Cover((cnt_issue
== 2)
139 & (cnt_write
[0] == 1)
140 & (cnt_write
[1] == 1)
141 & (cnt_alu_write
== 1))
142 self
.assertFormal(m
, mode
="cover", depth
=10)
145 if __name__
== "__main__":