move unused directory out of src, to indicate "ignore completely"
[soc.git] / src / soc / fu / trap / formal / proof_main_stage.py
1 # Proof of correctness for trap pipeline, main stage
2
3
4 """
5 Links:
6 * https://bugs.libre-soc.org/show_bug.cgi?id=421
7 """
8
9
10 import unittest
11
12 from nmigen import Cat, Const, Elaboratable, Module, Signal
13 from nmigen.asserts import Assert, AnyConst
14 from nmigen.cli import rtlil
15
16 from nmutil.formaltest import FHDLTestCase
17
18 from soc.consts import MSR
19
20 from soc.decoder.power_enums import MicrOp
21
22 from soc.fu.trap.main_stage import TrapMainStage
23 from soc.fu.trap.pipe_data import TrapPipeSpec
24 from soc.fu.trap.trap_input_record import CompTrapOpSubset
25
26
27 def field(r, start, end):
28 return r[63-end:63-start]
29
30
31 class Driver(Elaboratable):
32 """
33 """
34
35 def elaborate(self, platform):
36 m = Module()
37 comb = m.d.comb
38
39 rec = CompTrapOpSubset()
40 pspec = TrapPipeSpec(id_wid=2)
41
42 m.submodules.dut = dut = TrapMainStage(pspec)
43
44 # frequently used aliases
45 op = dut.i.ctx.op
46 msr_o = dut.o.msr
47 srr1_i = dut.i.srr1
48
49 comb += op.eq(rec)
50
51 # start of properties
52 with m.Switch(op.insn_type):
53 with m.Case(MicrOp.OP_SC):
54 comb += [
55 Assert(dut.o.srr0.ok),
56 Assert(dut.o.srr1.ok),
57
58 Assert(dut.o.srr0.data == (dut.i.cia + 4)[0:64]),
59 Assert(field(dut.o.srr1, 33, 36) == 0),
60 Assert(field(dut.o.srr1, 42, 47) == 0),
61 Assert(field(dut.o.srr1, 0, 32) == field(dut.i.msr, 0, 32)),
62 Assert(field(dut.o.srr1, 37, 41) == field(dut.i.msr, 37, 41)),
63 Assert(field(dut.o.srr1, 48, 63) == field(dut.i.msr, 48, 63)),
64 ]
65 with m.Case(MicrOp.OP_RFID):
66 comb += [
67 Assert(msr_o.ok),
68 Assert(dut.o.nia.ok),
69
70 Assert(msr_o[MSR.HV] == (srr1_i[MSR.HV] & dut.i.msr[MSR.HV])),
71 Assert(msr_o[MSR.EE] == (srr1_i[MSR.EE] | srr1_i[MSR.PR])),
72 Assert(msr_o[MSR.IR] == (srr1_i[MSR.IR] | srr1_i[MSR.PR])),
73 Assert(msr_o[MSR.DR] == (srr1_i[MSR.DR] | srr1_i[MSR.PR])),
74 Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
75 Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
76 Assert(msr_o[63-32] == srr1_i[63-32]),
77 Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
78 Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
79 Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
80 Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
81 Assert(dut.o.nia.data == Cat(Const(0, 2), dut.i.srr0[2:])),
82 ]
83 with m.If(dut.i.msr[MSR.HV]):
84 comb += Assert(msr_o[MSR.ME] == srr1_i[MSR.ME])
85 with m.Else():
86 comb += Assert(msr_o[MSR.ME] == dut.i.msr[MSR.ME])
87 with m.If((field(dut.i.msr, 29, 31) != 0b010) |
88 (field(dut.i.msr, 29, 31) != 0b000)):
89 comb += Assert(field(msr_o.data, 29, 31) == field(srr1_i, 29, 31))
90
91 comb += dut.i.ctx.matches(dut.o.ctx)
92
93 return m
94
95
96 class TrapMainStageTestCase(FHDLTestCase):
97 def test_formal(self):
98 self.assertFormal(Driver(), mode="bmc", depth=10)
99 self.assertFormal(Driver(), mode="cover", depth=10)
100
101 def test_ilang(self):
102 vl = rtlil.convert(Driver(), ports=[])
103 with open("trap_main_stage.il", "w") as f:
104 f.write(vl)
105
106
107 if __name__ == '__main__':
108 unittest.main()
109