b3fc7f281c4375a5637e855c28428278ea520fcc
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
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
.input_stage
import ALUInputStage
10 from soc
.alu
.pipe_data
import ALUPipeSpec
11 from soc
.alu
.alu_input_record
import CompALUOpSubset
15 # This defines a module to drive the device under test and assert
16 # properties about its outputs
17 class Driver(Elaboratable
):
22 def elaborate(self
, platform
):
26 rec
= CompALUOpSubset()
28 # Setup random inputs for dut.op
32 comb
+= p
.eq(AnyConst(width
))
34 pspec
= ALUPipeSpec(id_wid
=2, op_wid
=recwidth
)
35 m
.submodules
.dut
= dut
= ALUInputStage(pspec
)
39 comb
+= [dut
.i
.a
.eq(a
),
45 comb
+= dut
.i
.ctx
.op
.eq(rec
)
48 # Assert that op gets copied from the input to output
52 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
53 comb
+= Assert(dut_sig
== rec_sig
)
55 with m
.If(rec
.invert_a
):
56 comb
+= Assert(dut
.o
.a
== ~a
)
58 comb
+= Assert(dut
.o
.a
== a
)
60 with m
.If(rec
.imm_data
.imm_ok
):
61 comb
+= Assert(dut
.o
.b
== rec
.imm_data
.imm
)
63 comb
+= Assert(dut
.o
.b
== b
)
70 class GTCombinerTestCase(FHDLTestCase
):
71 def test_formal(self
):
73 self
.assertFormal(module
, mode
="bmc", depth
=4)
74 self
.assertFormal(module
, mode
="cover", depth
=4)
77 vl
= rtlil
.convert(dut
, ports
=[])
78 with
open("input_stage.il", "w") as f
:
82 if __name__
== '__main__':