whoops missed make_hazard_vec test
[soc.git] / src / soc / fu / alu / formal / proof_main_stage.py
1 # Proof of correctness for ALU pipeline, main stage
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
3 """
4 Links:
5 * https://bugs.libre-soc.org/show_bug.cgi?id=306
6 * https://bugs.libre-soc.org/show_bug.cgi?id=305
7 * https://bugs.libre-soc.org/show_bug.cgi?id=343
8 """
9
10 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
11 signed)
12 from nmigen.asserts import Assert, AnyConst, Assume, Cover
13 from nmutil.formaltest import FHDLTestCase
14 from nmigen.cli import rtlil
15
16 from soc.fu.alu.main_stage import ALUMainStage
17 from soc.fu.alu.pipe_data import ALUPipeSpec
18 from soc.fu.alu.alu_input_record import CompALUOpSubset
19 from openpower.decoder.power_enums import MicrOp
20 import unittest
21
22
23 # This defines a module to drive the device under test and assert
24 # properties about its outputs
25 class Driver(Elaboratable):
26 def __init__(self):
27 # inputs and outputs
28 pass
29
30 def elaborate(self, platform):
31 m = Module()
32 comb = m.d.comb
33
34 rec = CompALUOpSubset()
35 # Setup random inputs for dut.op
36 for p in rec.ports():
37 width = p.width
38 comb += p.eq(AnyConst(width))
39
40 pspec = ALUPipeSpec(id_wid=2)
41 m.submodules.dut = dut = ALUMainStage(pspec)
42
43 # convenience variables
44 a = dut.i.a
45 b = dut.i.b
46 ca_in = dut.i.xer_ca[0] # CA carry in
47 ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
48 so_in = dut.i.xer_so # SO sticky overflow
49
50 ca_o = dut.o.xer_ca.data[0] # CA carry out
51 ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
52 ov_o = dut.o.xer_ov.data[0] # OV overflow
53 ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
54 o = dut.o.o.data
55
56 # setup random inputs
57 comb += [a.eq(AnyConst(64)),
58 b.eq(AnyConst(64)),
59 ca_in.eq(AnyConst(0b11)),
60 so_in.eq(AnyConst(1))]
61
62 # and for the context muxid
63 width = dut.i.ctx.muxid.width
64 comb += dut.i.ctx.muxid.eq(AnyConst(width))
65
66 # assign the PowerDecode2 operation subset
67 comb += dut.i.ctx.op.eq(rec)
68
69 # check that the operation (op) is passed through (and muxid)
70 comb += Assert(dut.o.ctx.op == dut.i.ctx.op)
71 comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid)
72
73 # signed and signed/32 versions of input a
74 a_signed = Signal(signed(64))
75 a_signed_32 = Signal(signed(32))
76 comb += a_signed.eq(a)
77 comb += a_signed_32.eq(a[0:32])
78
79 # do not check MSBs of a/b in 32-bit mode
80 with m.If(rec.is_32bit):
81 comb += Assume(a[32:64] == 0)
82 comb += Assume(b[32:64] == 0)
83
84 # Data.ok checking. these only to be valid when there is a change
85 # in the output that needs to go into a regfile
86 o_ok = Signal()
87 cr0_ok = Signal()
88 ov_ok = Signal()
89 ca_ok = Signal()
90 comb += cr0_ok.eq(0)
91 comb += ov_ok.eq(0)
92 comb += ca_ok.eq(0)
93
94 # main assertion of arithmetic operations
95 with m.Switch(rec.insn_type):
96 with m.Case(MicrOp.OP_ADD):
97
98 # check result of 65-bit add-with-carry
99 comb += Assert(Cat(o, ca_o) == (a + b + ca_in))
100
101 # CA32 - XXX note this fails! replace with ca_in and it works
102 comb += Assert((a[0:32] + b[0:32] + ca_in)[32] == ca32_o)
103
104 # From microwatt execute1.vhdl line 130, calc_ov() function
105 comb += Assert(ov_o == ((ca_o ^ o[-1]) & ~(a[-1] ^ b[-1])))
106 comb += Assert(ov32_o == ((ca32_o ^ o[31]) & ~(a[31] ^ b[31])))
107 comb += ov_ok.eq(1)
108 comb += ca_ok.eq(1)
109 comb += o_ok.eq(1)
110
111 with m.Case(MicrOp.OP_EXTS):
112 for i in [1, 2, 4]:
113 with m.If(rec.data_len == i):
114 # main part, then sign-bit replicated up
115 comb += Assert(o[0:i*8] == a[0:i*8])
116 comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
117 comb += o_ok.eq(1)
118
119 with m.Case(MicrOp.OP_CMP):
120 # CMP is defined as not taking in carry
121 comb += Assume(ca_in == 0)
122 comb += Assert(o == (a+b)[0:64])
123
124 with m.Case(MicrOp.OP_CMPEQB):
125 src1 = a[0:8]
126 eqs = Signal(8)
127 for i in range(8):
128 comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
129 comb += Assert(dut.o.cr0.data[2] == eqs.any())
130 comb += cr0_ok.eq(1)
131
132 # check that data ok was only enabled when op actioned
133 comb += Assert(dut.o.o.ok == o_ok)
134 comb += Assert(dut.o.cr0.ok == cr0_ok)
135 comb += Assert(dut.o.xer_ov.ok == ov_ok)
136 comb += Assert(dut.o.xer_ca.ok == ca_ok)
137
138 return m
139
140
141 class ALUTestCase(FHDLTestCase):
142 def test_formal(self):
143 module = Driver()
144 self.assertFormal(module, mode="bmc", depth=2)
145 self.assertFormal(module, mode="cover", depth=2)
146 def test_ilang(self):
147 dut = Driver()
148 vl = rtlil.convert(dut, ports=[])
149 with open("alu_main_stage.il", "w") as f:
150 f.write(vl)
151
152
153 if __name__ == '__main__':
154 unittest.main()