moving teststate_check_regs written by klehman into openpower-isa
[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 * https://libre-soc.org/openpower/isa/fixedtrap/
8 * https://libre-soc.org/openpower/isa/sprset/
9 * https://libre-soc.org/openpower/isa/system/
10 """
11
12
13 import unittest
14
15 from nmigen import Cat, Const, Elaboratable, Module, Signal, signed
16 from nmigen.asserts import Assert, AnyConst
17 from nmigen.cli import rtlil
18
19 from nmutil.extend import exts
20 from nmutil.formaltest import FHDLTestCase
21
22 from openpower.consts import MSR, MSRb, PI, TT, field
23
24 from openpower.decoder.power_enums import MicrOp
25
26 from soc.fu.trap.main_stage import TrapMainStage
27 from soc.fu.trap.pipe_data import TrapPipeSpec
28 from soc.fu.trap.trap_input_record import CompTrapOpSubset
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, msr_i = dut.o.msr, op.msr
47 srr0_o, srr0_i = dut.o.srr0, dut.i.srr0
48 srr1_o, srr1_i = dut.o.srr1, dut.i.srr1
49 nia_o = dut.o.nia
50 rs = dut.i.a
51
52 comb += op.eq(rec)
53
54 # expected values
55 exp_msr = Signal(len(msr_o.data))
56 exp_srr1 = Signal(len(srr1_o.data))
57
58 d_fields = dut.fields.FormD
59 sc_fields = dut.fields.FormSC
60 x_fields = dut.fields.FormX
61
62 L = x_fields.L[0:-1]
63
64 # This alias exists because some of our assertions exceed PEP8
65 # width constraints. Avoid using this alias in the general
66 # case; ONLY use it when you're simultaneously trying to preserve
67 # line-oriented readability (to make the code easy to compare with
68 # the v3.0B spec) while simultaneously preserving PEP8 compliance.
69 F = field
70
71 # start of properties
72 with m.Switch(op.insn_type):
73
74 ###############
75 # TDI/TWI/TD/TW. v3.0B p90-91
76 ###############
77 with m.Case(MicrOp.OP_TRAP):
78 to = Signal(len(d_fields.TO))
79 comb += to.eq(d_fields.TO[0:-1])
80
81 a_i = Signal(64)
82 b_i = Signal(64)
83 comb += a_i.eq(dut.i.a)
84 comb += b_i.eq(dut.i.b)
85
86 a_s = Signal(signed(64), reset_less=True)
87 b_s = Signal(signed(64), reset_less=True)
88 a = Signal(64, reset_less=True)
89 b = Signal(64, reset_less=True)
90
91 with m.If(op.is_32bit):
92 comb += a_s.eq(exts(a_i, 32, 64))
93 comb += b_s.eq(exts(b_i, 32, 64))
94 comb += a.eq(a_i[0:32])
95 comb += b.eq(b_i[0:32])
96 with m.Else():
97 comb += a_s.eq(a_i)
98 comb += b_s.eq(b_i)
99 comb += a.eq(a_i)
100 comb += b.eq(b_i)
101
102 lt_s = Signal(reset_less=True)
103 gt_s = Signal(reset_less=True)
104 lt_u = Signal(reset_less=True)
105 gt_u = Signal(reset_less=True)
106 equal = Signal(reset_less=True)
107
108 comb += lt_s.eq(a_s < b_s)
109 comb += gt_s.eq(a_s > b_s)
110 comb += lt_u.eq(a < b)
111 comb += gt_u.eq(a > b)
112 comb += equal.eq(a == b)
113
114 trapbits = Signal(5, reset_less=True)
115 comb += trapbits.eq(Cat(gt_u, lt_u, equal, gt_s, lt_s))
116
117 take_trap = Signal()
118 traptype = op.traptype
119 comb += take_trap.eq(traptype.any() | (trapbits & to).any())
120
121 with m.If(take_trap):
122 comb += exp_msr.eq(op.msr)
123
124 # these are all set depending on the trap address (type)
125 # see V3.0B p1063 however as noted in main_stage.py
126 # the types of interrupts supported all need the same
127 # values (for now)
128 comb += field(exp_msr, MSRb.IR).eq(0)
129 comb += field(exp_msr, MSRb.DR).eq(0)
130 comb += field(exp_msr, MSRb.FE0).eq(0)
131 comb += field(exp_msr, MSRb.FE1).eq(0)
132 comb += field(exp_msr, MSRb.EE).eq(0)
133 comb += field(exp_msr, MSRb.RI).eq(0)
134 comb += field(exp_msr, MSRb.SF).eq(1)
135 comb += field(exp_msr, MSRb.TM).eq(0)
136 comb += field(exp_msr, MSRb.VEC).eq(0)
137 comb += field(exp_msr, MSRb.VSX).eq(0)
138 comb += field(exp_msr, MSRb.PR).eq(0)
139 comb += field(exp_msr, MSRb.FP).eq(0)
140 comb += field(exp_msr, MSRb.PMM).eq(0)
141
142 comb += field(exp_msr, MSRb.TEs, MSRb.TEe).eq(0)
143
144 comb += field(exp_msr, MSRb.UND).eq(0)
145 comb += field(exp_msr, MSRb.LE).eq(1)
146
147 comb += exp_srr1.eq(op.msr)
148
149 # Per V3.0B, page 1075
150 comb += field(exp_srr1, 33, 36).eq(0)
151 comb += field(exp_srr1, 42).eq(0) # TM_BAD_THING
152 comb += field(exp_srr1, 43).eq(traptype[0]) # FP
153 comb += field(exp_srr1, 44).eq(traptype[4]) # ILLEG
154 comb += field(exp_srr1, 45).eq(traptype[1]) # PRIV
155 comb += field(exp_srr1, 46).eq(traptype == 0) # TRAP
156 comb += field(exp_srr1, 47).eq(traptype[3]) # ADDR
157
158 comb += [
159 Assert(msr_o.ok),
160 Assert(msr_o.data == exp_msr),
161 Assert(srr0_o.ok),
162 Assert(srr0_o.data == op.cia),
163 Assert(srr1_o.ok),
164 Assert(srr1_o.data == exp_srr1),
165 Assert(nia_o.ok),
166 Assert(nia_o.data == op.trapaddr << 4),
167 ]
168
169 ###################
170 # MTMSR
171 # Specs found on V3.0B, page 977.
172 ###################
173
174 with m.Case(MicrOp.OP_MTMSR):
175 comb += exp_msr.eq(msr_i) # will copy and override
176
177 with m.If(L == 0):
178 comb += [
179 field(exp_msr, 48).eq(field(rs, 48) | field(rs, 49)),
180 field(exp_msr, 58).eq(field(rs, 58) | field(rs, 49)),
181 field(exp_msr, 59).eq(field(rs, 59) | field(rs, 49)),
182 field(exp_msr, 32, 47).eq(field(rs, 32, 47)),
183 field(exp_msr, 49, 50).eq(field(rs, 49, 50)),
184 field(exp_msr, 52, 57).eq(field(rs, 52, 57)),
185 field(exp_msr, 60, 62).eq(field(rs, 60, 62)),
186 ]
187 with m.Else():
188 # L=1 only checks 48 and 62
189 comb += [
190 field(exp_msr, 48).eq(field(rs, 48)),
191 field(exp_msr, 62).eq(field(rs, 62)),
192 ]
193
194 comb += [
195 Assert(msr_o.data == exp_msr),
196 Assert(msr_o.ok),
197 ]
198
199 ###################
200 # MTMSRD
201 # Specs found on V3.0B, page 978.
202 ###################
203
204 with m.Case(MicrOp.OP_MTMSRD):
205 msr_od = msr_o.data # another "shortener"
206
207 with m.If(L == 0):
208 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
209 # MSR[29:31] <- SRR1[29:31]
210 with m.If((field(msr_i, 29, 31) != 0b010) |
211 (field(rs, 29, 31) != 0b000)):
212 comb += Assert(F(msr_od, 29, 31) == F(rs, 29, 31))
213 with m.Else():
214 comb += Assert(F(msr_od, 29, 31) == F(msr_i, 29, 31))
215
216 # MSR[48] <- (RS)[48] | (RS)[49]
217 # MSR[58] <- (RS)[58] | (RS)[49]
218 # MSR[59] <- (RS)[59] | (RS)[49]
219 PR = field(rs, 49) # alias/copy of SRR1 PR field
220 comb += [
221 Assert(field(msr_od, 48) == field(rs, 48) | PR),
222 Assert(field(msr_od, 58) == field(rs, 58) | PR),
223 Assert(field(msr_od, 59) == field(rs, 59) | PR),
224 ]
225
226 comb += [
227 # Ambiguity in specification on page 978 of V3.0B:
228 # MSR[4:28] <- RS[4 6:28].
229 #
230 # I've decided to follow the prose in the programmer
231 # note just underneath the typographical ambiguity.
232 # MSR[4:28] <- RS[4:28].
233
234 # range = 0:2 4:28 32:40 42:47 49:50 52:57 60:62
235 # MSR[range] <- (RS)[range]
236 Assert(field(msr_od, 0, 2) == field(rs, 0, 2)),
237 Assert(field(msr_od, 4, 28) == field(rs, 4, 28)),
238 Assert(field(msr_od, 32, 47) == field(rs, 32, 47)),
239 Assert(field(msr_od, 49, 50) == field(rs, 49, 50)),
240 Assert(field(msr_od, 52, 57) == field(rs, 52, 57)),
241 Assert(field(msr_od, 60, 62) == field(rs, 60, 62)),
242 ]
243 with m.Else():
244 # L=1 only checks 48 and 62 (MSR.EE, MSR.RI)
245 comb += [
246 Assert(field(msr_od, 48) == field(rs, 48)),
247 Assert(field(msr_od, 62) == field(rs, 62)),
248 ]
249
250 comb += Assert(msr_o.ok)
251
252 ###################
253 # MFMSR
254 ###################
255
256 with m.Case(MicrOp.OP_MFMSR):
257 comb += [
258 Assert(dut.o.o.ok),
259 Assert(dut.o.o.data == msr_i),
260 ]
261
262 ###################
263 # RFID. v3.0B p955
264 ###################
265 with m.Case(MicrOp.OP_RFID):
266 msr_od = msr_o.data # another "shortener"
267 comb += [
268 Assert(msr_o.ok),
269 Assert(nia_o.ok),
270 ]
271
272 # Note: going through the spec pseudo-code, line-by-line,
273 # in order, with these assertions. idea is: compare
274 # *directly* against the pseudo-code. therefore, leave
275 # numbering in (from pseudo-code) and add *comments* about
276 # which field it is (3 == HV etc.)
277
278 # spec: MSR[51] <- MSR[3] & SRR1[51]
279 comb += Assert(field(msr_o, 3) == field(srr1_i, 3))
280
281 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
282 # MSR[29:31] <- SRR1[29:31]
283 with m.If((field(msr_i , 29, 31) != 0b010) |
284 (field(srr1_i, 29, 31) != 0b000)):
285 comb += Assert(F(msr_od, 29, 31) == F(srr1_i, 29, 31))
286 with m.Else():
287 comb += Assert(F(msr_od, 29, 31) == F(msr_i, 29, 31))
288
289 # check EE (48) IR (58), DR (59): PR (49) will over-ride
290 # MSR[48] <- (RS)[48] | (RS)[49]
291 # MSR[58] <- (RS)[58] | (RS)[49]
292 # MSR[59] <- (RS)[59] | (RS)[49]
293 PR = field(srr1_i, 49) # alias/copy of SRR1 PR field
294 comb += [
295 Assert(field(msr_od, 48) == field(srr1_i, 48) | PR),
296 Assert(field(msr_od, 58) == field(srr1_i, 58) | PR),
297 Assert(field(msr_od, 59) == field(srr1_i, 59) | PR),
298 ]
299
300 # remaining bits: straight copy. don't know what these are:
301 # just trust the v3.0B spec is correct.
302 # range = 0:2 4:28 32:40 42:47 49:50 52:57 60:62
303 # MSR[range] <- (RS)[range]
304 comb += [
305 Assert(field(msr_od, 0, 2) == field(srr1_i, 0, 2)),
306 Assert(field(msr_od, 4, 28) == field(srr1_i, 4, 28)),
307 Assert(field(msr_od, 32) == field(srr1_i, 32)),
308 Assert(field(msr_od, 37, 41) == field(srr1_i, 37, 41)),
309 Assert(field(msr_od, 49, 50) == field(srr1_i, 49, 50)),
310 Assert(field(msr_od, 52, 57) == field(srr1_i, 52, 57)),
311 Assert(field(msr_od, 60, 63) == field(srr1_i, 60, 63)),
312 ]
313
314 # check NIA against SRR0. 2 LSBs are set to zero (word-align)
315 comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
316
317 #################
318 # SC. v3.0B p952
319 #################
320 with m.Case(MicrOp.OP_SC):
321 comb += exp_msr.eq(op.msr)
322 # Unless otherwise documented, these exceptions to the MSR bits
323 # are documented in Power ISA V3.0B, page 1063 or 1064.
324 # We are not supporting hypervisor or transactional semantics,
325 # so we skip enforcing those fields' properties.
326 comb += field(exp_msr, MSRb.IR).eq(0)
327 comb += field(exp_msr, MSRb.DR).eq(0)
328 comb += field(exp_msr, MSRb.FE0).eq(0)
329 comb += field(exp_msr, MSRb.FE1).eq(0)
330 comb += field(exp_msr, MSRb.EE).eq(0)
331 comb += field(exp_msr, MSRb.RI).eq(0)
332 comb += field(exp_msr, MSRb.SF).eq(1)
333 comb += field(exp_msr, MSRb.TM).eq(0)
334 comb += field(exp_msr, MSRb.VEC).eq(0)
335 comb += field(exp_msr, MSRb.VSX).eq(0)
336 comb += field(exp_msr, MSRb.PR).eq(0)
337 comb += field(exp_msr, MSRb.FP).eq(0)
338 comb += field(exp_msr, MSRb.PMM).eq(0)
339 comb += field(exp_msr, MSRb.TEs, MSRb.TEe).eq(0)
340 comb += field(exp_msr, MSRb.UND).eq(0)
341 comb += field(exp_msr, MSRb.LE).eq(1)
342
343 comb += [
344 Assert(dut.o.srr0.ok),
345 Assert(srr1_o.ok),
346 Assert(msr_o.ok),
347
348 Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
349 Assert(field(srr1_o, 33, 36) == 0),
350 Assert(field(srr1_o, 42, 47) == 0),
351 Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
352 Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
353 Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
354
355 Assert(msr_o.data == exp_msr),
356 ]
357
358 comb += dut.i.ctx.matches(dut.o.ctx)
359
360 return m
361
362
363 class TrapMainStageTestCase(FHDLTestCase):
364 def test_formal(self):
365 self.assertFormal(Driver(), mode="bmc", depth=10)
366 self.assertFormal(Driver(), mode="cover", depth=10)
367
368 def test_ilang(self):
369 vl = rtlil.convert(Driver(), ports=[])
370 with open("trap_main_stage.il", "w") as f:
371 f.write(vl)
372
373
374 if __name__ == '__main__':
375 unittest.main()
376