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
20 from nmutil
.extend
import exts
23 # This defines a module to drive the device under test and assert
24 # properties about its outputs
25 class Driver(Elaboratable
):
30 def elaborate(self
, platform
):
34 rec
= CompSROpSubset()
35 # Setup random inputs for dut.op
37 comb
+= p
.eq(AnyConst(p
.width
))
39 pspec
= ShiftRotPipeSpec(id_wid
=2)
40 m
.submodules
.dut
= dut
= ShiftRotMainStage(pspec
)
42 # convenience variables
46 carry_in
= dut
.i
.xer_ca
[0]
47 carry_in32
= dut
.i
.xer_ca
[1]
48 carry_out
= dut
.o
.xer_ca
50 print ("fields", rec
.fields
)
54 m_fields
= dut
.fields
.FormM
55 md_fields
= dut
.fields
.FormMD
58 comb
+= a
.eq(AnyConst(64))
59 comb
+= b
.eq(AnyConst(64))
60 comb
+= carry_in
.eq(AnyConst(1))
61 comb
+= carry_in32
.eq(AnyConst(1))
64 comb
+= dut
.i
.ctx
.op
.eq(rec
)
66 # check that the operation (op) is passed through (and muxid)
67 comb
+= Assert(dut
.o
.ctx
.op
== dut
.i
.ctx
.op
)
68 comb
+= Assert(dut
.o
.ctx
.muxid
== dut
.i
.ctx
.muxid
)
70 # signed and signed/32 versions of input a
71 a_signed
= Signal(signed(64))
72 a_signed_32
= Signal(signed(32))
73 comb
+= a_signed
.eq(a
)
74 comb
+= a_signed_32
.eq(a
[0:32])
77 mb
= Signal(7, reset_less
=True)
78 ml
= Signal(64, reset_less
=True)
81 with m
.If((itype
== MicrOp
.OP_RLC
) |
(itype
== MicrOp
.OP_RLCL
)):
82 with m
.If(rec
.is_32bit
):
83 comb
+= mb
.eq(m_fields
.MB
[0:-1])
85 comb
+= mb
.eq(md_fields
.mb
[0:-1])
87 with m
.If(rec
.is_32bit
):
91 comb
+= ml
.eq(left_mask(m
, mb
))
94 me
= Signal(7, reset_less
=True)
95 mr
= Signal(64, reset_less
=True)
98 with m
.If((itype
== MicrOp
.OP_RLC
) |
(itype
== MicrOp
.OP_RLCR
)):
99 with m
.If(rec
.is_32bit
):
100 comb
+= me
.eq(m_fields
.ME
[0:-1])
102 comb
+= me
.eq(md_fields
.me
[0:-1])
104 with m
.If(rec
.is_32bit
):
105 comb
+= me
.eq(b
[0:6])
108 comb
+= mr
.eq(right_mask(m
, me
))
114 # main assertion of arithmetic operations
115 with m
.Switch(itype
):
117 # left-shift: 64/32-bit
118 with m
.Case(MicrOp
.OP_SHL
):
119 comb
+= Assume(ra
== 0)
120 with m
.If(rec
.is_32bit
):
121 comb
+= Assert(o
[0:32] == ((a
<< b
[0:6]) & 0xffffffff))
122 comb
+= Assert(o
[32:64] == 0)
124 comb
+= Assert(o
== ((a
<< b
[0:7]) & ((1 << 64)-1)))
126 # right-shift: 64/32-bit / signed
127 with m
.Case(MicrOp
.OP_SHR
):
128 comb
+= Assume(ra
== 0)
129 with m
.If(~rec
.is_signed
):
130 with m
.If(rec
.is_32bit
):
131 comb
+= Assert(o
[0:32] == (a
[0:32] >> b
[0:6]))
132 comb
+= Assert(o
[32:64] == 0)
134 comb
+= Assert(o
== (a
>> b
[0:7]))
136 with m
.If(rec
.is_32bit
):
137 comb
+= Assert(o
[0:32] == (a_signed_32
>> b
[0:6]))
138 comb
+= Assert(o
[32:64] == Repl(a
[31], 32))
140 comb
+= Assert(o
== (a_signed
>> b
[0:7]))
142 # extswsli: 32/64-bit moded
143 with m
.Case(MicrOp
.OP_EXTSWSLI
):
144 comb
+= Assume(ra
== 0)
145 with m
.If(rec
.is_32bit
):
146 comb
+= Assert(o
[0:32] == ((a
<< b
[0:6]) & 0xffffffff))
147 comb
+= Assert(o
[32:64] == 0)
149 # sign-extend to 64 bit
150 a_s
= Signal(64, reset_less
=True)
151 comb
+= a_s
.eq(exts(a
, 32, 64))
152 comb
+= Assert(o
== ((a_s
<< b
[0:7]) & ((1 << 64)-1)))
155 with m
.Case(MicrOp
.OP_RLC
):
157 with m
.Case(MicrOp
.OP_RLCR
):
159 with m
.Case(MicrOp
.OP_RLCL
):
164 # check that data ok was only enabled when op actioned
165 comb
+= Assert(dut
.o
.o
.ok
== o_ok
)
170 class ALUTestCase(FHDLTestCase
):
171 def test_formal(self
):
173 self
.assertFormal(module
, mode
="bmc", depth
=2)
174 self
.assertFormal(module
, mode
="cover", depth
=2)
175 def test_ilang(self
):
177 vl
= rtlil
.convert(dut
, ports
=[])
178 with
open("main_stage.il", "w") as f
:
182 if __name__
== '__main__':