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
5 from nmigen
.asserts
import Assert
, AnyConst
, Assume
, Cover
6 from nmigen
.test
.utils
import FHDLTestCase
7 from nmigen
.cli
import rtlil
9 from soc
.alu
.main_stage
import ALUMainStage
10 from soc
.alu
.pipe_data
import ALUPipeSpec
11 from soc
.alu
.alu_input_record
import CompALUOpSubset
12 from soc
.decoder
.power_enums
import InternalOp
16 # This defines a module to drive the device under test and assert
17 # properties about its outputs
18 class Driver(Elaboratable
):
23 def elaborate(self
, platform
):
27 rec
= CompALUOpSubset()
29 # Setup random inputs for dut.op
33 comb
+= p
.eq(AnyConst(width
))
35 pspec
= ALUPipeSpec(id_wid
=2, op_wid
=recwidth
)
36 m
.submodules
.dut
= dut
= ALUMainStage(pspec
)
42 comb
+= [dut
.i
.a
.eq(a
),
44 dut
.i
.carry_in
.eq(carry_in
),
48 carry_in
.eq(AnyConst(1)),
49 so_in
.eq(AnyConst(1))]
52 comb
+= dut
.i
.ctx
.op
.eq(rec
)
55 # Assert that op gets copied from the input to output
59 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
60 comb
+= Assert(dut_sig
== rec_sig
)
62 with m
.Switch(rec
.insn_type
):
63 with m
.Case(InternalOp
.OP_ADD
):
64 comb
+= Assert(Cat(dut
.o
.o
, dut
.o
.carry_out
) ==
66 with m
.Case(InternalOp
.OP_AND
):
67 comb
+= Assert(dut
.o
.o
== a
& b
)
68 with m
.Case(InternalOp
.OP_OR
):
69 comb
+= Assert(dut
.o
.o
== a | b
)
70 with m
.Case(InternalOp
.OP_XOR
):
71 comb
+= Assert(dut
.o
.o
== a ^ b
)
76 class GTCombinerTestCase(FHDLTestCase
):
77 def test_formal(self
):
79 self
.assertFormal(module
, mode
="bmc", depth
=4)
80 self
.assertFormal(module
, mode
="cover", depth
=4)
83 vl
= rtlil
.convert(dut
, ports
=[])
84 with
open("main_stage.il", "w") as f
:
88 if __name__
== '__main__':