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)
45 step
= int(width
/mwidth
)
46 for i
in range(mwidth
-1):
47 points
[(i
+1)*step
] = gates
[i
]
50 comb
+= [data
.eq(AnyConst(width
)),
51 bitrev
.eq(AnyConst(1)),
52 shifter
.eq(AnyConst(shifterwidth
)),
53 gates
.eq(AnyConst(mwidth
-1))]
55 m
.submodules
.dut
= dut
= PartitionedScalarShift(width
, points
)
57 data_intervals
= self
.get_intervals(data
, points
)
58 out_intervals
= self
.get_intervals(out
, points
)
60 comb
+= [dut
.data
.eq(data
),
61 dut
.shifter
.eq(shifter
),
62 dut
.bitrev
.eq(bitrev
),
65 expected
= Signal(width
)
67 with m
.If(bitrev
== 0):
68 with m
.Switch(points
.as_sig()):
71 out
[0:24] == (data
[0:24] << (shifter
& 0x1f)) &
75 comb
+= Assert(out
[0:8] ==
76 (data
[0:8] << (shifter
& 0x7)) & 0xFF)
77 comb
+= Assert(out
[8:24] ==
78 (data
[8:24] << (shifter
& 0xf)) & 0xffff)
81 comb
+= Assert(out
[16:24] ==
82 (data
[16:24] << (shifter
& 0x7)) & 0xff)
83 comb
+= Assert(out
[0:16] ==
84 (data
[0:16] << (shifter
& 0xf)) & 0xffff)
87 comb
+= Assert(out
[0:8] ==
88 (data
[0:8] << (shifter
& 0x7)) & 0xFF)
89 comb
+= Assert(out
[8:16] ==
90 (data
[8:16] << (shifter
& 0x7)) & 0xff)
91 comb
+= Assert(out
[16:24] ==
92 (data
[16:24] << (shifter
& 0x7)) & 0xff)
95 class PartitionedScalarShiftTestCase(FHDLTestCase
):
97 module
= ShifterDriver()
98 self
.assertFormal(module
, mode
="bmc", depth
=4)
102 gates
= Signal(mwidth
-1)
103 points
= PartitionPoints()
104 step
= int(width
/mwidth
)
105 for i
in range(mwidth
-1):
106 points
[(i
+1)*step
] = gates
[i
]
108 dut
= PartitionedScalarShift(width
, points
)
109 vl
= rtlil
.convert(dut
, ports
=[gates
, dut
.data
,
112 with
open("scalar_shift.il", "w") as f
:
115 if __name__
== "__main__":