50264d5c33d2f73078f13e45cd46e6381a62fe79
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
.shift_rot
.main_stage
import ShiftRotMainStage
11 from soc
.alu
.pipe_data
import ALUPipeSpec
12 from soc
.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
= ShiftRotMainStage(pspec
)
39 # convenience variables
43 carry_in
= dut
.i
.carry_in
45 carry_out
= dut
.o
.carry_out
49 comb
+= [a
.eq(AnyConst(64)),
51 carry_in
.eq(AnyConst(1)),
52 so_in
.eq(AnyConst(1))]
54 comb
+= dut
.i
.ctx
.op
.eq(rec
)
56 # Assert that op gets copied from the input to output
57 for rec_sig
in rec
.ports():
59 dut_sig
= getattr(dut
.o
.ctx
.op
, name
)
60 comb
+= Assert(dut_sig
== rec_sig
)
62 # signed and signed/32 versions of input a
63 a_signed
= Signal(signed(64))
64 a_signed_32
= Signal(signed(32))
65 comb
+= a_signed
.eq(a
)
66 comb
+= a_signed_32
.eq(a
[0:32])
68 # main assertion of arithmetic operations
69 with m
.Switch(rec
.insn_type
):
70 with m
.Case(InternalOp
.OP_SHL
):
71 comb
+= Assume(ra
== 0)
72 with m
.If(rec
.is_32bit
):
73 comb
+= Assert(o
[0:32] == ((a
<< b
[0:6]) & 0xffffffff))
74 comb
+= Assert(o
[32:64] == 0)
76 comb
+= Assert(o
== ((a
<< b
[0:7]) & ((1 << 64)-1)))
77 with m
.Case(InternalOp
.OP_SHR
):
78 comb
+= Assume(ra
== 0)
79 with m
.If(~rec
.is_signed
):
80 with m
.If(rec
.is_32bit
):
81 comb
+= Assert(o
[0:32] == (a
[0:32] >> b
[0:6]))
82 comb
+= Assert(o
[32:64] == 0)
84 comb
+= Assert(o
== (a
>> b
[0:7]))
86 with m
.If(rec
.is_32bit
):
87 comb
+= Assert(o
[0:32] == (a_signed_32
>> b
[0:6]))
88 comb
+= Assert(o
[32:64] == Repl(a
[31], 32))
90 comb
+= Assert(o
== (a_signed
>> b
[0:7]))
95 class ALUTestCase(FHDLTestCase
):
96 def test_formal(self
):
98 self
.assertFormal(module
, mode
="bmc", depth
=2)
99 self
.assertFormal(module
, mode
="cover", depth
=2)
100 def test_ilang(self
):
102 vl
= rtlil
.convert(dut
, ports
=[])
103 with
open("main_stage.il", "w") as f
:
107 if __name__
== '__main__':