5d8bae28fd3773f655679a9596902dc6644e2511
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 openpower
.decoder
.power_enums
import MicrOp
19 from openpower
.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
62 rs
= dut
.i
.rs
# register to shift
63 b
= dut
.i
.rb
# register containing amount to shift by
64 ra
= dut
.i
.a
# source register if masking is to be done
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
+= rs
.eq(AnyConst(64))
78 comb
+= ra
.eq(AnyConst(64))
79 comb
+= b
.eq(AnyConst(64))
80 comb
+= carry_in
.eq(AnyConst(1))
81 comb
+= carry_in32
.eq(AnyConst(1))
84 comb
+= dut
.i
.ctx
.op
.eq(rec
)
86 # check that the operation (op) is passed through (and muxid)
87 comb
+= Assert(dut
.o
.ctx
.op
== dut
.i
.ctx
.op
)
88 comb
+= Assert(dut
.o
.ctx
.muxid
== dut
.i
.ctx
.muxid
)
90 # signed and signed/32 versions of input rs
91 a_signed
= Signal(signed(64))
92 a_signed_32
= Signal(signed(32))
93 comb
+= a_signed
.eq(rs
)
94 comb
+= a_signed_32
.eq(rs
[0:32])
97 mb
= Signal(7, reset_less
=True)
98 ml
= Signal(64, reset_less
=True)
101 with m
.If((itype
== MicrOp
.OP_RLC
) |
(itype
== MicrOp
.OP_RLCL
)):
102 with m
.If(rec
.is_32bit
):
103 comb
+= mb
.eq(m_fields
.MB
)
105 comb
+= mb
.eq(md_fields
.mb
)
107 with m
.If(rec
.is_32bit
):
108 comb
+= mb
.eq(b
[0:6])
111 comb
+= ml
.eq(left_mask(m
, mb
))
114 me
= Signal(7, reset_less
=True)
115 mr
= Signal(64, reset_less
=True)
118 with m
.If((itype
== MicrOp
.OP_RLC
) |
(itype
== MicrOp
.OP_RLCR
)):
119 with m
.If(rec
.is_32bit
):
120 comb
+= me
.eq(m_fields
.ME
)
122 comb
+= me
.eq(md_fields
.me
)
124 with m
.If(rec
.is_32bit
):
125 comb
+= me
.eq(b
[0:6])
128 comb
+= mr
.eq(right_mask(m
, me
))
134 # main assertion of arithmetic operations
135 with m
.Switch(itype
):
137 # left-shift: 64/32-bit
138 with m
.Case(MicrOp
.OP_SHL
):
139 comb
+= Assume(ra
== 0)
140 with m
.If(rec
.is_32bit
):
141 comb
+= Assert(o
[0:32] == ((rs
<< b
[0:6]) & 0xffffffff))
142 comb
+= Assert(o
[32:64] == 0)
144 comb
+= Assert(o
== ((rs
<< b
[0:7]) & ((1 << 64)-1)))
146 # right-shift: 64/32-bit / signed
147 with m
.Case(MicrOp
.OP_SHR
):
148 comb
+= Assume(ra
== 0)
149 with m
.If(~rec
.is_signed
):
150 with m
.If(rec
.is_32bit
):
151 comb
+= Assert(o
[0:32] == (rs
[0:32] >> b
[0:6]))
152 comb
+= Assert(o
[32:64] == 0)
154 comb
+= Assert(o
== (rs
>> b
[0:7]))
156 with m
.If(rec
.is_32bit
):
157 comb
+= Assert(o
[0:32] == (a_signed_32
>> b
[0:6]))
158 comb
+= Assert(o
[32:64] == Repl(rs
[31], 32))
160 comb
+= Assert(o
== (a_signed
>> b
[0:7]))
162 # extswsli: 32/64-bit moded
163 with m
.Case(MicrOp
.OP_EXTSWSLI
):
164 comb
+= Assume(ra
== 0)
165 with m
.If(rec
.is_32bit
):
166 comb
+= Assert(o
[0:32] == ((rs
<< b
[0:6]) & 0xffffffff))
167 comb
+= Assert(o
[32:64] == 0)
169 # sign-extend to 64 bit
170 a_s
= Signal(64, reset_less
=True)
171 comb
+= a_s
.eq(exts(rs
, 32, 64))
172 comb
+= Assert(o
== ((a_s
<< b
[0:7]) & ((1 << 64)-1)))
174 # rlwinm, rlwnm, rlwimi
175 # *CAN* these even be 64-bit capable? I don't think they are.
176 with m
.Case(MicrOp
.OP_RLC
):
177 comb
+= Assume(ra
== 0)
178 comb
+= Assume(rec
.is_32bit
)
180 # Duplicate some signals so that they're much easier to find
182 # Pro-tip: when debugging, factor out expressions into
184 # signals, and search using a unique grep-tag (RLC in my case).
186 # debugging, resubstitute values to comply with surrounding
189 mrl
= Signal(64, reset_less
=True, name
='MASK_FOR_RLC')
191 comb
+= mrl
.eq(ml | mr
)
193 comb
+= mrl
.eq(ml
& mr
)
195 ainp
= Signal(64, reset_less
=True, name
='A_INP_FOR_RLC')
196 comb
+= ainp
.eq(field(rs
, 32, 63))
198 sh
= Signal(6, reset_less
=True, name
='SH_FOR_RLC')
199 comb
+= sh
.eq(b
[0:6])
201 exp_shl
= Signal(64, reset_less
=True,
202 name
='A_SHIFTED_LEFT_BY_SH_FOR_RLC')
203 comb
+= exp_shl
.eq((ainp
<< sh
) & 0xFFFFFFFF)
205 exp_shr
= Signal(64, reset_less
=True,
206 name
='A_SHIFTED_RIGHT_FOR_RLC')
207 comb
+= exp_shr
.eq((ainp
>> (32 - sh
)) & 0xFFFFFFFF)
209 exp_rot
= Signal(64, reset_less
=True,
210 name
='A_ROTATED_LEFT_FOR_RLC')
211 comb
+= exp_rot
.eq(exp_shl | exp_shr
)
213 exp_ol
= Signal(32, reset_less
=True, name
='EXPECTED_OL_FOR_RLC')
214 comb
+= exp_ol
.eq(field((exp_rot
& mrl
) |
(ainp
& ~mrl
),
217 act_ol
= Signal(32, reset_less
=True, name
='ACTUAL_OL_FOR_RLC')
218 comb
+= act_ol
.eq(field(o
, 32, 63))
220 # If I uncomment the following lines, I can confirm that all
221 # 32-bit rotations work. If I uncomment only one of the
222 # following lines, I can confirm that all 32-bit rotations
223 # work. When I remove/recomment BOTH lines, however, the
224 # assertion fails. Why??
226 # comb += Assume(mr == 0xFFFFFFFF)
227 # comb += Assume(ml == 0xFFFFFFFF)
228 #with m.If(rec.is_32bit):
229 # comb += Assert(act_ol == exp_ol)
230 # comb += Assert(field(o, 0, 31) == 0)
233 with m
.Case(MicrOp
.OP_RLCR
):
235 with m
.Case(MicrOp
.OP_RLCL
):
240 # check that data ok was only enabled when op actioned
241 comb
+= Assert(dut
.o
.o
.ok
== o_ok
)
246 class ALUTestCase(FHDLTestCase
):
247 def test_formal(self
):
249 self
.assertFormal(module
, mode
="bmc", depth
=2)
250 self
.assertFormal(module
, mode
="cover", depth
=2)
251 def test_ilang(self
):
253 vl
= rtlil
.convert(dut
, ports
=[])
254 with
open("main_stage.il", "w") as f
:
258 if __name__
== '__main__':