1 # Proof of correctness for partitioned equal signal combiner
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
5 * https://bugs.libre-soc.org/show_bug.cgi?id=340
8 from nmigen
import (Module
, Signal
, Elaboratable
, Mux
, Cat
, Repl
,
10 from nmigen
.asserts
import Assert
, AnyConst
, Assume
, Cover
11 from nmutil
.formaltest
import FHDLTestCase
12 from nmigen
.cli
import rtlil
14 from soc
.fu
.shift_rot
.main_stage
import ShiftRotMainStage
15 from soc
.fu
.shift_rot
.rotator
import right_mask
, left_mask
16 from soc
.fu
.shift_rot
.pipe_data
import ShiftRotPipeSpec
17 from soc
.fu
.shift_rot
.sr_input_record
import CompSROpSubset
18 from soc
.decoder
.power_enums
import MicrOp
19 from soc
.consts
import field
22 from nmutil
.extend
import exts
25 # This defines a module to drive the device under test and assert
26 # properties about its outputs
27 class Driver(Elaboratable
):
32 def elaborate(self
, platform
):
36 rec
= CompSROpSubset()
37 # Setup random inputs for dut.op. do them explicitly so that
38 # we can see which ones cause failures in the debug report
39 #for p in rec.ports():
40 # comb += p.eq(AnyConst(p.width))
41 comb
+= rec
.insn_type
.eq(AnyConst(rec
.insn_type
.width
))
42 comb
+= rec
.fn_unit
.eq(AnyConst(rec
.fn_unit
.width
))
43 comb
+= rec
.imm_data
.imm
.eq(AnyConst(rec
.imm_data
.imm
.width
))
44 comb
+= rec
.imm_data
.imm_ok
.eq(AnyConst(rec
.imm_data
.imm_ok
.width
))
45 comb
+= rec
.rc
.rc
.eq(AnyConst(rec
.rc
.rc
.width
))
46 comb
+= rec
.rc
.rc_ok
.eq(AnyConst(rec
.rc
.rc_ok
.width
))
47 comb
+= rec
.oe
.oe
.eq(AnyConst(rec
.oe
.oe
.width
))
48 comb
+= rec
.oe
.oe_ok
.eq(AnyConst(rec
.oe
.oe_ok
.width
))
49 comb
+= rec
.write_cr0
.eq(AnyConst(rec
.write_cr0
.width
))
50 comb
+= rec
.input_carry
.eq(AnyConst(rec
.input_carry
.width
))
51 comb
+= rec
.output_carry
.eq(AnyConst(rec
.output_carry
.width
))
52 comb
+= rec
.input_cr
.eq(AnyConst(rec
.input_cr
.width
))
53 comb
+= rec
.is_32bit
.eq(AnyConst(rec
.is_32bit
.width
))
54 comb
+= rec
.is_signed
.eq(AnyConst(rec
.is_signed
.width
))
55 comb
+= rec
.insn
.eq(AnyConst(rec
.insn
.width
))
58 pspec
= ShiftRotPipeSpec(id_wid
=2)
59 m
.submodules
.dut
= dut
= ShiftRotMainStage(pspec
)
61 # convenience variables
65 carry_in
= dut
.i
.xer_ca
[0]
66 carry_in32
= dut
.i
.xer_ca
[1]
67 carry_out
= dut
.o
.xer_ca
69 print ("fields", rec
.fields
)
73 m_fields
= dut
.fields
.FormM
74 md_fields
= dut
.fields
.FormMD
77 comb
+= a
.eq(AnyConst(64))
78 comb
+= b
.eq(AnyConst(64))
79 comb
+= carry_in
.eq(AnyConst(1))
80 comb
+= carry_in32
.eq(AnyConst(1))
83 comb
+= dut
.i
.ctx
.op
.eq(rec
)
85 # check that the operation (op) is passed through (and muxid)
86 comb
+= Assert(dut
.o
.ctx
.op
== dut
.i
.ctx
.op
)
87 comb
+= Assert(dut
.o
.ctx
.muxid
== dut
.i
.ctx
.muxid
)
89 # signed and signed/32 versions of input a
90 a_signed
= Signal(signed(64))
91 a_signed_32
= Signal(signed(32))
92 comb
+= a_signed
.eq(a
)
93 comb
+= a_signed_32
.eq(a
[0:32])
96 mb
= Signal(7, reset_less
=True)
97 ml
= Signal(64, reset_less
=True)
100 with m
.If((itype
== MicrOp
.OP_RLC
) |
(itype
== MicrOp
.OP_RLCL
)):
101 with m
.If(rec
.is_32bit
):
102 comb
+= mb
.eq(m_fields
.MB
[0:-1])
104 comb
+= mb
.eq(md_fields
.mb
[0:-1])
106 with m
.If(rec
.is_32bit
):
107 comb
+= mb
.eq(b
[0:6])
110 comb
+= ml
.eq(left_mask(m
, mb
))
113 me
= Signal(7, reset_less
=True)
114 mr
= Signal(64, reset_less
=True)
117 with m
.If((itype
== MicrOp
.OP_RLC
) |
(itype
== MicrOp
.OP_RLCR
)):
118 with m
.If(rec
.is_32bit
):
119 comb
+= me
.eq(m_fields
.ME
[0:-1])
121 comb
+= me
.eq(md_fields
.me
[0:-1])
123 with m
.If(rec
.is_32bit
):
124 comb
+= me
.eq(b
[0:6])
127 comb
+= mr
.eq(right_mask(m
, me
))
133 # main assertion of arithmetic operations
134 with m
.Switch(itype
):
136 # left-shift: 64/32-bit
137 with m
.Case(MicrOp
.OP_SHL
):
138 comb
+= Assume(ra
== 0)
139 with m
.If(rec
.is_32bit
):
140 comb
+= Assert(o
[0:32] == ((a
<< b
[0:6]) & 0xffffffff))
141 comb
+= Assert(o
[32:64] == 0)
143 comb
+= Assert(o
== ((a
<< b
[0:7]) & ((1 << 64)-1)))
145 # right-shift: 64/32-bit / signed
146 with m
.Case(MicrOp
.OP_SHR
):
147 comb
+= Assume(ra
== 0)
148 with m
.If(~rec
.is_signed
):
149 with m
.If(rec
.is_32bit
):
150 comb
+= Assert(o
[0:32] == (a
[0:32] >> b
[0:6]))
151 comb
+= Assert(o
[32:64] == 0)
153 comb
+= Assert(o
== (a
>> b
[0:7]))
155 with m
.If(rec
.is_32bit
):
156 comb
+= Assert(o
[0:32] == (a_signed_32
>> b
[0:6]))
157 comb
+= Assert(o
[32:64] == Repl(a
[31], 32))
159 comb
+= Assert(o
== (a_signed
>> b
[0:7]))
161 # extswsli: 32/64-bit moded
162 with m
.Case(MicrOp
.OP_EXTSWSLI
):
163 comb
+= Assume(ra
== 0)
164 with m
.If(rec
.is_32bit
):
165 comb
+= Assert(o
[0:32] == ((a
<< b
[0:6]) & 0xffffffff))
166 comb
+= Assert(o
[32:64] == 0)
168 # sign-extend to 64 bit
169 a_s
= Signal(64, reset_less
=True)
170 comb
+= a_s
.eq(exts(a
, 32, 64))
171 comb
+= Assert(o
== ((a_s
<< b
[0:7]) & ((1 << 64)-1)))
173 # rlwinm, rlwnm, rlwimi
174 # *CAN* these even be 64-bit capable? I don't think they are.
175 with m
.Case(MicrOp
.OP_RLC
):
176 comb
+= Assume(ra
== 0)
178 # Duplicate some signals so that they're much easier to find in gtkwave.
179 # Pro-tip: when debugging, factor out expressions into explicitly named
180 # signals, and search using a unique grep-tag (RLC in my case). After
181 # debugging, resubstitute values to comply with surrounding code norms.
183 mrl
= Signal(64, reset_less
=True, name
='MASK_FOR_RLC')
184 comb
+= mrl
.eq(ml | mr
)
186 ainp
= Signal(64, reset_less
=True, name
='A_INP_FOR_RLC')
187 comb
+= ainp
.eq(field(a
, 32, 63))
189 sh
= Signal(6, reset_less
=True, name
='SH_FOR_RLC')
190 comb
+= sh
.eq(b
[0:6])
192 exp_shl
= Signal(64, reset_less
=True, name
='A_SHIFTED_LEFT_BY_SH_FOR_RLC')
193 comb
+= exp_shl
.eq((ainp
<< sh
) & 0xFFFFFFFF)
195 exp_shr
= Signal(64, reset_less
=True, name
='A_SHIFTED_RIGHT_FOR_RLC')
196 comb
+= exp_shr
.eq((ainp
>> (32 - sh
)) & 0xFFFFFFFF)
198 exp_rot
= Signal(64, reset_less
=True, name
='A_ROTATED_LEFT_FOR_RLC')
199 comb
+= exp_rot
.eq(exp_shl | exp_shr
)
201 exp_ol
= Signal(32, reset_less
=True, name
='EXPECTED_OL_FOR_RLC')
202 comb
+= exp_ol
.eq(field((exp_rot
& mrl
) |
(ainp
& ~mrl
), 32, 63))
204 act_ol
= Signal(32, reset_less
=True, name
='ACTUAL_OL_FOR_RLC')
205 comb
+= act_ol
.eq(field(o
, 32, 63))
207 # If I uncomment the following lines, I can confirm that all
208 # 32-bit rotations work. If I uncomment only one of the
209 # following lines, I can confirm that all 32-bit rotations
210 # work. When I remove/recomment BOTH lines, however, the
211 # assertion fails. Why??
213 # comb += Assume(mr == 0xFFFFFFFF)
214 # comb += Assume(ml == 0xFFFFFFFF)
215 with m
.If(rec
.is_32bit
):
216 comb
+= Assert(act_ol
== exp_ol
)
217 comb
+= Assert(field(o
, 0, 31) == 0)
220 with m
.Case(MicrOp
.OP_RLCR
):
222 with m
.Case(MicrOp
.OP_RLCL
):
227 # check that data ok was only enabled when op actioned
228 comb
+= Assert(dut
.o
.o
.ok
== o_ok
)
233 class ALUTestCase(FHDLTestCase
):
234 def test_formal(self
):
236 self
.assertFormal(module
, mode
="bmc", depth
=2)
237 self
.assertFormal(module
, mode
="cover", depth
=2)
238 def test_ilang(self
):
240 vl
= rtlil
.convert(dut
, ports
=[])
241 with
open("main_stage.il", "w") as f
:
245 if __name__
== '__main__':