1 # Proof of correctness for partitioned equal signal combiner
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
4 from nmigen
import (Module
, Signal
, Elaboratable
, Mux
, Cat
, Repl
,
6 from nmigen
.asserts
import Assert
, AnyConst
, Assume
, Cover
7 from nmigen
.test
.utils
import FHDLTestCase
8 from nmigen
.cli
import rtlil
10 from soc
.fu
.alu
.main_stage
import ALUMainStage
11 from soc
.fu
.alu
.pipe_data
import ALUPipeSpec
12 from soc
.fu
.alu
.alu_input_record
import CompALUOpSubset
13 from soc
.decoder
.power_enums
import InternalOp
17 # This defines a module to drive the device under test and assert
18 # properties about its outputs
19 class Driver(Elaboratable
):
24 def elaborate(self
, platform
):
28 rec
= CompALUOpSubset()
30 # Setup random inputs for dut.op
34 comb
+= p
.eq(AnyConst(width
))
36 pspec
= ALUPipeSpec(id_wid
=2, op_wid
=recwidth
)
37 m
.submodules
.dut
= dut
= ALUMainStage(pspec
)
39 # convenience variables
42 carry_in
= dut
.i
.xer_ca
[0]
43 carry_in32
= dut
.i
.xer_ca
[1]
45 carry_out
= dut
.o
.xer_ca
.data
[0]
46 carry_out32
= dut
.o
.xer_ca
.data
[1]
47 ov_out
= dut
.o
.xer_ov
.data
[0]
48 ov_out32
= dut
.o
.xer_ov
.data
[1]
52 comb
+= [a
.eq(AnyConst(64)),
54 carry_in
.eq(AnyConst(0b11)),
55 so_in
.eq(AnyConst(1))]
57 comb
+= dut
.i
.ctx
.op
.eq(rec
)
59 # Assert that op gets copied from the input to output
60 for rec_sig
in rec
.ports():
62 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
63 comb
+= Assert(dut_sig
== rec_sig
)
65 # signed and signed/32 versions of input a
66 a_signed
= Signal(signed(64))
67 a_signed_32
= Signal(signed(32))
68 comb
+= a_signed
.eq(a
)
69 comb
+= a_signed_32
.eq(a
[0:32])
71 comb
+= Assume(a
[32:64] == 0)
72 comb
+= Assume(b
[32:64] == 0)
73 # main assertion of arithmetic operations
74 with m
.Switch(rec
.insn_type
):
75 with m
.Case(InternalOp
.OP_ADD
):
77 comb
+= Assert(Cat(o
, carry_out
) == (a
+ b
+ carry_in
))
79 # CA32 - XXX note this fails! replace with carry_in and it works
80 comb
+= Assert((a
[0:32] + b
[0:32] + carry_in
)[32]
83 # From microwatt execute1.vhdl line 130
84 comb
+= Assert(ov_out
== ((carry_out ^ o
[-1]) &
86 comb
+= Assert(ov_out32
== ((carry_out32 ^ o
[31]) &
88 with m
.Case(InternalOp
.OP_EXTS
):
90 with m
.If(rec
.data_len
== i
):
91 comb
+= Assert(o
[0:i
*8] == a
[0:i
*8])
92 comb
+= Assert(o
[i
*8:64] == Repl(a
[i
*8-1], 64-(i
*8)))
93 with m
.Case(InternalOp
.OP_CMP
):
94 # CMP is defined as not taking in carry
95 comb
+= Assume(carry_in
== 0)
96 comb
+= Assert(o
== (a
+b
)[0:64])
98 with m
.Case(InternalOp
.OP_CMPEQB
):
102 comb
+= eqs
[i
].eq(src1
== b
[i
*8:(i
+1)*8])
103 comb
+= Assert(dut
.o
.cr0
[2] == eqs
.any())
108 class ALUTestCase(FHDLTestCase
):
109 def test_formal(self
):
111 self
.assertFormal(module
, mode
="bmc", depth
=2)
112 self
.assertFormal(module
, mode
="cover", depth
=2)
113 def test_ilang(self
):
115 vl
= rtlil
.convert(dut
, ports
=[])
116 with
open("alu_main_stage.il", "w") as f
:
120 if __name__
== '__main__':