7c0d7593d1eb1ac564b08ce328f5659708453321
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 shift_right
= Signal()
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 shift_right
.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
.shift_right
.eq(shift_right
),
65 expected
= Signal(width
)
67 with m
.If(shift_right
== 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)
94 with m
.Switch(points
.as_sig()):
97 out
[0:24] == (data
[0:24] >> (shifter
& 0x1f)) &
101 comb
+= Assert(out
[0:8] ==
102 (data
[0:8] >> (shifter
& 0x7)) & 0xFF)
103 comb
+= Assert(out
[8:24] ==
104 (data
[8:24] >> (shifter
& 0xf)) & 0xffff)
107 comb
+= Assert(out
[16:24] ==
108 (data
[16:24] >> (shifter
& 0x7)) & 0xff)
109 comb
+= Assert(out
[0:16] ==
110 (data
[0:16] >> (shifter
& 0xf)) & 0xffff)
113 comb
+= Assert(out
[0:8] ==
114 (data
[0:8] >> (shifter
& 0x7)) & 0xFF)
115 comb
+= Assert(out
[8:16] ==
116 (data
[8:16] >> (shifter
& 0x7)) & 0xff)
117 comb
+= Assert(out
[16:24] ==
118 (data
[16:24] >> (shifter
& 0x7)) & 0xff)
121 class PartitionedScalarShiftTestCase(FHDLTestCase
):
122 def test_shift(self
):
123 module
= ShifterDriver()
124 self
.assertFormal(module
, mode
="bmc", depth
=4)
125 def test_ilang(self
):
128 gates
= Signal(mwidth
-1)
129 points
= PartitionPoints()
130 step
= int(width
/mwidth
)
131 for i
in range(mwidth
-1):
132 points
[(i
+1)*step
] = gates
[i
]
134 dut
= PartitionedScalarShift(width
, points
)
135 vl
= rtlil
.convert(dut
, ports
=[gates
, dut
.data
,
138 with
open("scalar_shift.il", "w") as f
:
141 if __name__
== "__main__":