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 soc.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 comb += dut.i.ctx.op.eq(rec)
63
64 # Assert that op gets copied from the input to output
65 for rec_sig in rec.ports():
66 name = rec_sig.name
67 dut_sig = getattr(dut.o.ctx.op, name)
68 comb += Assert(dut_sig == rec_sig)
69
70 # signed and signed/32 versions of input a
71 a_signed = Signal(signed(64))
72 a_signed_32 = Signal(signed(32))
73 comb += a_signed.eq(a)
74 comb += a_signed_32.eq(a[0:32])
75
76 # do not check MSBs of a/b in 32-bit mode
77 with m.If(rec.is_32bit):
78 comb += Assume(a[32:64] == 0)
79 comb += Assume(b[32:64] == 0)
80
81 # Data.ok checking. these only to be valid when there is a change
82 # in the output that needs to go into a regfile
83 o_ok = Signal()
84 cr0_ok = Signal()
85 ov_ok = Signal()
86 ca_ok = Signal()
87 comb += cr0_ok.eq(0)
88 comb += ov_ok.eq(0)
89 comb += ca_ok.eq(0)
90
91 # main assertion of arithmetic operations
92 with m.Switch(rec.insn_type):
93 with m.Case(MicrOp.OP_ADD):
94
95 # check result of 65-bit add-with-carry
96 comb += Assert(Cat(o, ca_o) == (a + b + ca_in))
97
98 # CA32 - XXX note this fails! replace with ca_in and it works
99 comb += Assert((a[0:32] + b[0:32] + ca_in)[32] == ca32_o)
100
101 # From microwatt execute1.vhdl line 130, calc_ov() function
102 comb += Assert(ov_o == ((ca_o ^ o[-1]) & ~(a[-1] ^ b[-1])))
103 comb += Assert(ov32_o == ((ca32_o ^ o[31]) & ~(a[31] ^ b[31])))
104 comb += ov_ok.eq(1)
105 comb += ca_ok.eq(1)
106 comb += o_ok.eq(1)
107
108 with m.Case(MicrOp.OP_EXTS):
109 for i in [1, 2, 4]:
110 with m.If(rec.data_len == i):
111 # main part, then sign-bit replicated up
112 comb += Assert(o[0:i*8] == a[0:i*8])
113 comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
114 comb += o_ok.eq(1)
115
116 with m.Case(MicrOp.OP_CMP):
117 # CMP is defined as not taking in carry
118 comb += Assume(ca_in == 0)
119 comb += Assert(o == (a+b)[0:64])
120
121 with m.Case(MicrOp.OP_CMPEQB):
122 src1 = a[0:8]
123 eqs = Signal(8)
124 for i in range(8):
125 comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
126 comb += Assert(dut.o.cr0.data[2] == eqs.any())
127 comb += cr0_ok.eq(1)
128
129 # check that data ok was only enabled when op actioned
130 comb += Assert(dut.o.o.ok == o_ok)
131 comb += Assert(dut.o.cr0.ok == cr0_ok)
132 comb += Assert(dut.o.xer_ov.ok == ov_ok)
133 comb += Assert(dut.o.xer_ca.ok == ca_ok)
134
135 return m
136
137
138 class ALUTestCase(FHDLTestCase):
139 def test_formal(self):
140 module = Driver()
141 self.assertFormal(module, mode="bmc", depth=2)
142 self.assertFormal(module, mode="cover", depth=2)
143 def test_ilang(self):
144 dut = Driver()
145 vl = rtlil.convert(dut, ports=[])
146 with open("alu_main_stage.il", "w") as f:
147 f.write(vl)
148
149
150 if __name__ == '__main__':
151 unittest.main()