4528de0a4cb8cb3649674adb392eeee9c0cfb4ce
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
))
57 pspec
= ShiftRotPipeSpec(id_wid
=2)
58 m
.submodules
.dut
= dut
= ShiftRotMainStage(pspec
)
60 # convenience variables
61 rs
= dut
.i
.rs
# register to shift
62 b
= dut
.i
.rb
# register containing amount to shift by
63 ra
= dut
.i
.a
# source register if masking is to be done
64 carry_in
= dut
.i
.xer_ca
[0]
65 carry_in32
= dut
.i
.xer_ca
[1]
66 carry_out
= dut
.o
.xer_ca
68 print("fields", rec
.fields
)
72 m_fields
= dut
.fields
.FormM
73 md_fields
= dut
.fields
.FormMD
76 comb
+= rs
.eq(AnyConst(64))
77 comb
+= ra
.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 rs
90 a_signed
= Signal(signed(64))
91 a_signed_32
= Signal(signed(32))
92 comb
+= a_signed
.eq(rs
)
93 comb
+= a_signed_32
.eq(rs
[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
)
104 comb
+= mb
.eq(md_fields
.mb
)
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
)
121 comb
+= me
.eq(md_fields
.me
)
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] == ((rs
<< b
[0:6]) & 0xffffffff))
141 comb
+= Assert(o
[32:64] == 0)
143 comb
+= Assert(o
== ((rs
<< 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] == (rs
[0:32] >> b
[0:6]))
151 comb
+= Assert(o
[32:64] == 0)
153 comb
+= Assert(o
== (rs
>> 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(rs
[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] == ((rs
<< 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(rs
, 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)
177 comb
+= Assume(rec
.is_32bit
)
179 # Duplicate some signals so that they're much easier to find
181 # Pro-tip: when debugging, factor out expressions into
183 # signals, and search using a unique grep-tag (RLC in my case).
185 # debugging, resubstitute values to comply with surrounding
188 mrl
= Signal(64, reset_less
=True, name
='MASK_FOR_RLC')
190 comb
+= mrl
.eq(ml | mr
)
192 comb
+= mrl
.eq(ml
& mr
)
194 ainp
= Signal(64, reset_less
=True, name
='A_INP_FOR_RLC')
195 comb
+= ainp
.eq(field(rs
, 32, 63))
197 sh
= Signal(6, reset_less
=True, name
='SH_FOR_RLC')
198 comb
+= sh
.eq(b
[0:6])
200 exp_shl
= Signal(64, reset_less
=True,
201 name
='A_SHIFTED_LEFT_BY_SH_FOR_RLC')
202 comb
+= exp_shl
.eq((ainp
<< sh
) & 0xFFFFFFFF)
204 exp_shr
= Signal(64, reset_less
=True,
205 name
='A_SHIFTED_RIGHT_FOR_RLC')
206 comb
+= exp_shr
.eq((ainp
>> (32 - sh
)) & 0xFFFFFFFF)
208 exp_rot
= Signal(64, reset_less
=True,
209 name
='A_ROTATED_LEFT_FOR_RLC')
210 comb
+= exp_rot
.eq(exp_shl | exp_shr
)
212 exp_ol
= Signal(32, reset_less
=True,
213 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)
252 def test_ilang(self
):
254 vl
= rtlil
.convert(dut
, ports
=[])
255 with
open("main_stage.il", "w") as f
:
259 if __name__
== '__main__':