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
39 comb
+= p
.eq(AnyConst(p
.width
))
41 pspec
= ShiftRotPipeSpec(id_wid
=2)
42 m
.submodules
.dut
= dut
= ShiftRotMainStage(pspec
)
44 # convenience variables
48 carry_in
= dut
.i
.xer_ca
[0]
49 carry_in32
= dut
.i
.xer_ca
[1]
50 carry_out
= dut
.o
.xer_ca
52 print ("fields", rec
.fields
)
56 m_fields
= dut
.fields
.FormM
57 md_fields
= dut
.fields
.FormMD
60 comb
+= a
.eq(AnyConst(64))
61 comb
+= b
.eq(AnyConst(64))
62 comb
+= carry_in
.eq(AnyConst(1))
63 comb
+= carry_in32
.eq(AnyConst(1))
66 comb
+= dut
.i
.ctx
.op
.eq(rec
)
68 # check that the operation (op) is passed through (and muxid)
69 comb
+= Assert(dut
.o
.ctx
.op
== dut
.i
.ctx
.op
)
70 comb
+= Assert(dut
.o
.ctx
.muxid
== dut
.i
.ctx
.muxid
)
72 # signed and signed/32 versions of input a
73 a_signed
= Signal(signed(64))
74 a_signed_32
= Signal(signed(32))
75 comb
+= a_signed
.eq(a
)
76 comb
+= a_signed_32
.eq(a
[0:32])
79 mb
= Signal(7, reset_less
=True)
80 ml
= Signal(64, reset_less
=True)
83 with m
.If((itype
== MicrOp
.OP_RLC
) |
(itype
== MicrOp
.OP_RLCL
)):
84 with m
.If(rec
.is_32bit
):
85 comb
+= mb
.eq(m_fields
.MB
[0:-1])
87 comb
+= mb
.eq(md_fields
.mb
[0:-1])
89 with m
.If(rec
.is_32bit
):
93 comb
+= ml
.eq(left_mask(m
, mb
))
96 me
= Signal(7, reset_less
=True)
97 mr
= Signal(64, reset_less
=True)
100 with m
.If((itype
== MicrOp
.OP_RLC
) |
(itype
== MicrOp
.OP_RLCR
)):
101 with m
.If(rec
.is_32bit
):
102 comb
+= me
.eq(m_fields
.ME
[0:-1])
104 comb
+= me
.eq(md_fields
.me
[0:-1])
106 with m
.If(rec
.is_32bit
):
107 comb
+= me
.eq(b
[0:6])
110 comb
+= mr
.eq(right_mask(m
, me
))
116 # main assertion of arithmetic operations
117 with m
.Switch(itype
):
119 # left-shift: 64/32-bit
120 with m
.Case(MicrOp
.OP_SHL
):
121 comb
+= Assume(ra
== 0)
122 with m
.If(rec
.is_32bit
):
123 comb
+= Assert(o
[0:32] == ((a
<< b
[0:6]) & 0xffffffff))
124 comb
+= Assert(o
[32:64] == 0)
126 comb
+= Assert(o
== ((a
<< b
[0:7]) & ((1 << 64)-1)))
128 # right-shift: 64/32-bit / signed
129 with m
.Case(MicrOp
.OP_SHR
):
130 comb
+= Assume(ra
== 0)
131 with m
.If(~rec
.is_signed
):
132 with m
.If(rec
.is_32bit
):
133 comb
+= Assert(o
[0:32] == (a
[0:32] >> b
[0:6]))
134 comb
+= Assert(o
[32:64] == 0)
136 comb
+= Assert(o
== (a
>> b
[0:7]))
138 with m
.If(rec
.is_32bit
):
139 comb
+= Assert(o
[0:32] == (a_signed_32
>> b
[0:6]))
140 comb
+= Assert(o
[32:64] == Repl(a
[31], 32))
142 comb
+= Assert(o
== (a_signed
>> b
[0:7]))
144 # extswsli: 32/64-bit moded
145 with m
.Case(MicrOp
.OP_EXTSWSLI
):
146 comb
+= Assume(ra
== 0)
147 with m
.If(rec
.is_32bit
):
148 comb
+= Assert(o
[0:32] == ((a
<< b
[0:6]) & 0xffffffff))
149 comb
+= Assert(o
[32:64] == 0)
151 # sign-extend to 64 bit
152 a_s
= Signal(64, reset_less
=True)
153 comb
+= a_s
.eq(exts(a
, 32, 64))
154 comb
+= Assert(o
== ((a_s
<< b
[0:7]) & ((1 << 64)-1)))
156 # rlwinm, rlwnm, rlwimi
157 # *CAN* these even be 64-bit capable? I don't think they are.
158 with m
.Case(MicrOp
.OP_RLC
):
159 comb
+= Assume(ra
== 0)
161 # Duplicate some signals so that they're much easier to find in gtkwave.
162 # Pro-tip: when debugging, factor out expressions into explicitly named
163 # signals, and search using a unique grep-tag (RLC in my case). After
164 # debugging, resubstitute values to taste.
166 mrl
= Signal(32, reset_less
=True, name
='MASK_FOR_RLC')
167 comb
+= mrl
.eq(ml
& mr
)
169 ainp
= Signal(32, reset_less
=True, name
='A_INP_FOR_RLC')
170 comb
+= ainp
.eq(field(a
, 32, 63))
172 sh
= Signal(6, reset_less
=True, name
='SH_FOR_RLC')
173 comb
+= sh
.eq(b
[0:6])
175 exp_shl
= Signal(32, reset_less
=True, name
='A_SHIFTED_LEFT_BY_SH_FOR_RLC')
176 comb
+= exp_shl
.eq((ainp
<< sh
) & 0xFFFFFFFF)
178 exp_shr
= Signal(32, reset_less
=True, name
='A_SHIFTED_RIGHT_FOR_RLC')
179 comb
+= exp_shr
.eq((ainp
>> (32 - sh
)) & 0xFFFFFFFF)
181 exp_ol
= Signal(32, reset_less
=True, name
='EXPECTED_OL_FOR_RLC')
182 comb
+= exp_ol
.eq(((exp_shl | exp_shr
) & mrl
) |
(ainp
& ~mrl
))
184 # If I uncomment the following lines, I can confirm that all
185 # 32-bit rotations work. If I uncomment only one of the
186 # following lines, I can confirm that all 32-bit rotations
187 # work. When I remove/recomment BOTH lines, however, the
188 # assertion fails. Why??
190 # comb += Assume(mr == 0xFFFFFFFF)
191 # comb += Assume(ml == 0xFFFFFFFF)
192 with m
.If(rec
.is_32bit
):
193 comb
+= Assert(field(o
, 32, 63) == exp_ol
)
194 comb
+= Assert(field(o
, 0, 31) == 0)
197 with m
.Case(MicrOp
.OP_RLCR
):
199 with m
.Case(MicrOp
.OP_RLCL
):
204 # check that data ok was only enabled when op actioned
205 comb
+= Assert(dut
.o
.o
.ok
== o_ok
)
210 class ALUTestCase(FHDLTestCase
):
211 def test_formal(self
):
213 self
.assertFormal(module
, mode
="bmc", depth
=2)
214 self
.assertFormal(module
, mode
="cover", depth
=2)
215 def test_ilang(self
):
217 vl
= rtlil
.convert(dut
, ports
=[])
218 with
open("main_stage.il", "w") as f
:
222 if __name__
== '__main__':