52409c4ea6617c59df754481381f6c23a28d0137
[soc.git] / src / soc / fu / branch / formal / proof_input_stage.py
1 # Proof of correctness for partitioned equal signal combiner
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
3
4 from nmigen import Module, Signal, Elaboratable, Mux
5 from nmigen.asserts import Assert, AnyConst, Assume, Cover
6 from nmutil.formaltest import FHDLTestCase
7 from nmigen.cli import rtlil
8
9 from soc.fu.alu.input_stage import ALUInputStage
10 from soc.fu.alu.pipe_data import ALUPipeSpec
11 from soc.fu.branch.br_input_record import CompBROpSubset
12 from soc.decoder.power_enums import MicrOp
13 import unittest
14
15
16 # This defines a module to drive the device under test and assert
17 # properties about its outputs
18 class Driver(Elaboratable):
19 def __init__(self):
20 # inputs and outputs
21 pass
22
23 def elaborate(self, platform):
24 m = Module()
25 comb = m.d.comb
26
27 rec = CompBROpSubset()
28 recwidth = 0
29 # Setup random inputs for dut.op
30 for p in rec.ports():
31 width = p.width
32 recwidth += width
33 comb += p.eq(AnyConst(width))
34
35 pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
36 m.submodules.dut = dut = ALUInputStage(pspec)
37
38 a = Signal(64)
39 b = Signal(64)
40 comb += [dut.i.a.eq(a),
41 dut.i.b.eq(b),
42 a.eq(AnyConst(64)),
43 b.eq(AnyConst(64))]
44
45 comb += dut.i.ctx.op.eq(rec)
46
47 # Assert that op gets copied from the input to output
48 for p in rec.ports():
49 name = p.name
50 rec_sig = p
51 dut_sig = getattr(dut.o.ctx.op, name)
52 comb += Assert(dut_sig == rec_sig)
53
54 with m.If(rec.invert_a):
55 comb += Assert(dut.o.a == ~a)
56 with m.Else():
57 comb += Assert(dut.o.a == a)
58
59 with m.If(rec.imm_data.imm_ok &
60 ~(rec.insn_type == MicrOp.OP_RLC)):
61 comb += Assert(dut.o.b == rec.imm_data.imm)
62 with m.Else():
63 comb += Assert(dut.o.b == b)
64
65 return m
66
67 class GTCombinerTestCase(FHDLTestCase):
68 def test_formal(self):
69 module = Driver()
70 self.assertFormal(module, mode="bmc", depth=4)
71 self.assertFormal(module, mode="cover", depth=4)
72 def test_ilang(self):
73 dut = Driver()
74 vl = rtlil.convert(dut, ports=[])
75 with open("input_stage.il", "w") as f:
76 f.write(vl)
77
78
79 if __name__ == '__main__':
80 unittest.main()