1 # Proof of correctness for partitioned scalar shifter
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
4 from nmigen
import Module
, Signal
, Elaboratable
, Mux
, Cat
5 from nmigen
.asserts
import Assert
, AnyConst
, Assume
6 from nmigen
.test
.utils
import FHDLTestCase
7 from nmigen
.cli
import rtlil
9 from ieee754
.part_mul_add
.partpoints
import PartitionPoints
10 from ieee754
.part_shift
.part_shift_scalar
import PartitionedScalarShift
14 # This defines a module to drive the device under test and assert
15 # properties about its outputs
16 class ShifterDriver(Elaboratable
):
21 def get_intervals(self
, signal
, points
):
24 keys
= list(points
.keys()) + [signal
.width
]
27 interval
.append(signal
[start
:end
])
31 def elaborate(self
, platform
):
38 # setup the inputs and outputs of the DUT as anyconst
41 shifter
= Signal(shifterwidth
)
42 points
= PartitionPoints()
43 gates
= Signal(mwidth
-1)
44 step
= int(width
/mwidth
)
45 for i
in range(mwidth
-1):
46 points
[(i
+1)*step
] = gates
[i
]
49 comb
+= [data
.eq(AnyConst(width
)),
50 shifter
.eq(AnyConst(shifterwidth
)),
51 gates
.eq(AnyConst(mwidth
-1))]
53 m
.submodules
.dut
= dut
= PartitionedScalarShift(width
, points
)
55 data_intervals
= self
.get_intervals(data
, points
)
56 out_intervals
= self
.get_intervals(out
, points
)
58 comb
+= [dut
.data
.eq(data
),
59 dut
.shifter
.eq(shifter
),
62 expected
= Signal(width
)
64 with m
.Switch(points
.as_sig()):
67 # out[0:24] == (data[0:24] << (shifter & 0x1f)) & 0xffffff)
70 comb
+= Assert(out
[0:8] ==
71 (data
[0:8] << (shifter
& 0x7)) & 0xFF)
72 # comb += Assert(out[8:16] ==
73 # (data[8:16] << (shifter)) & 0xffff)
76 # comb += Assert(out[16:24] ==
77 # (data[16:24] << (shifter & 0x7)) & 0xff)
78 comb
+= Assert(out
[0:16] ==
79 (data
[0:16] << (shifter
& 0xf)) & 0xffff)
82 comb
+= Assert(out
[0:8] ==
83 (data
[0:8] << (shifter
& 0x7)) & 0xFF)
84 comb
+= Assert(out
[8:16] ==
85 (data
[8:16] << (shifter
& 0x7)) & 0xff)
86 comb
+= Assert(out
[16:24] ==
87 (data
[16:24] << (shifter
& 0x7)) & 0xff)
90 class PartitionedScalarShiftTestCase(FHDLTestCase
):
92 module
= ShifterDriver()
93 self
.assertFormal(module
, mode
="bmc", depth
=4)
97 gates
= Signal(mwidth
-1)
98 points
= PartitionPoints()
99 step
= int(width
/mwidth
)
100 for i
in range(mwidth
-1):
101 points
[(i
+1)*step
] = gates
[i
]
103 dut
= PartitionedScalarShift(width
, points
)
104 vl
= rtlil
.convert(dut
, ports
=[gates
, dut
.data
,
107 with
open("scalar_shift.il", "w") as f
:
110 if __name__
== "__main__":