e6e8b7c7ca0d1952a83025abd3495ab26e3fae5a
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
.alu
.pipe_data
import ALUPipeSpec
16 from soc
.fu
.alu
.alu_input_record
import CompALUOpSubset
17 from soc
.decoder
.power_enums
import MicrOp
19 from nmutil
.extend
import exts
22 # This defines a module to drive the device under test and assert
23 # properties about its outputs
24 class Driver(Elaboratable
):
29 def elaborate(self
, platform
):
33 rec
= CompALUOpSubset()
34 # Setup random inputs for dut.op
36 comb
+= p
.eq(AnyConst(p
.width
))
38 pspec
= ALUPipeSpec(id_wid
=2)
39 m
.submodules
.dut
= dut
= ShiftRotMainStage(pspec
)
41 # convenience variables
45 carry_in
= dut
.i
.xer_ca
[0]
46 carry_in32
= dut
.i
.xer_ca
[1]
47 carry_out
= dut
.o
.xer_ca
51 comb
+= a
.eq(AnyConst(64))
52 comb
+= b
.eq(AnyConst(64))
53 comb
+= carry_in
.eq(AnyConst(1))
54 comb
+= carry_in32
.eq(AnyConst(1))
56 comb
+= dut
.i
.ctx
.op
.eq(rec
)
58 # Assert that op gets copied from the input to output
59 for rec_sig
in rec
.ports():
61 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
62 comb
+= Assert(dut_sig
== rec_sig
)
64 # signed and signed/32 versions of input a
65 a_signed
= Signal(signed(64))
66 a_signed_32
= Signal(signed(32))
67 comb
+= a_signed
.eq(a
)
68 comb
+= a_signed_32
.eq(a
[0:32])
74 # main assertion of arithmetic operations
75 with m
.Switch(rec
.insn_type
):
77 with m
.Case(MicrOp
.OP_SHL
):
78 comb
+= Assume(ra
== 0)
79 with m
.If(rec
.is_32bit
):
80 comb
+= Assert(o
[0:32] == ((a
<< b
[0:6]) & 0xffffffff))
81 comb
+= Assert(o
[32:64] == 0)
83 comb
+= Assert(o
== ((a
<< b
[0:7]) & ((1 << 64)-1)))
85 with m
.Case(MicrOp
.OP_SHR
):
86 comb
+= Assume(ra
== 0)
87 with m
.If(~rec
.is_signed
):
88 with m
.If(rec
.is_32bit
):
89 comb
+= Assert(o
[0:32] == (a
[0:32] >> b
[0:6]))
90 comb
+= Assert(o
[32:64] == 0)
92 comb
+= Assert(o
== (a
>> b
[0:7]))
94 with m
.If(rec
.is_32bit
):
95 comb
+= Assert(o
[0:32] == (a_signed_32
>> b
[0:6]))
96 comb
+= Assert(o
[32:64] == Repl(a
[31], 32))
98 comb
+= Assert(o
== (a_signed
>> b
[0:7]))
100 with m
.Case(MicrOp
.OP_RLC
):
102 with m
.Case(MicrOp
.OP_RLCR
):
104 with m
.Case(MicrOp
.OP_RLCL
):
106 with m
.Case(MicrOp
.OP_EXTSWSLI
):
108 a_s
= Signal(64, reset_less
=True)
109 comb
+= a_s
.eq(exts(a
, 32, 64))
110 # assume b[0:6] is sh
111 comb
+= Assume(b
[7:] == 0)
112 with m
.If(b
[0:7] == 0):
113 comb
+= Assert(o
[0:32] == a_s
[0:32])
116 #comb += Assert(o == ((a_s << b_s) & ((1 << 64)-1)))
122 # check that data ok was only enabled when op actioned
123 comb
+= Assert(dut
.o
.o
.ok
== o_ok
)
128 class ALUTestCase(FHDLTestCase
):
129 def test_formal(self
):
131 self
.assertFormal(module
, mode
="bmc", depth
=2)
132 self
.assertFormal(module
, mode
="cover", depth
=2)
133 def test_ilang(self
):
135 vl
= rtlil
.convert(dut
, ports
=[])
136 with
open("main_stage.il", "w") as f
:
140 if __name__
== '__main__':