1 # Proof of correctness for trap pipeline, main stage
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/
15 from nmigen
import Cat
, Const
, Elaboratable
, Module
, Signal
, signed
16 from nmigen
.asserts
import Assert
, AnyConst
17 from nmigen
.cli
import rtlil
19 from nmutil
.extend
import exts
20 from nmutil
.formaltest
import FHDLTestCase
22 from soc
.consts
import MSR
, PI
, TT
24 from soc
.decoder
.power_enums
import MicrOp
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
31 def field(r
, start
, end
=None):
32 """Answers with a subfield of the signal r ("register"), where
33 the start and end bits use IBM conventions. start < end.
37 return r
[63-end
:64-start
]
40 class Driver(Elaboratable
):
44 def elaborate(self
, platform
):
48 rec
= CompTrapOpSubset()
49 pspec
= TrapPipeSpec(id_wid
=2)
51 m
.submodules
.dut
= dut
= TrapMainStage(pspec
)
53 # frequently used aliases
55 msr_o
, msr_i
= dut
.o
.msr
, op
.msr
56 srr0_o
, srr0_i
= dut
.o
.srr0
, dut
.i
.srr0
57 srr1_o
, srr1_i
= dut
.o
.srr1
, dut
.i
.srr1
63 with m
.Switch(op
.insn_type
):
66 # TDI/TWI/TD/TW. v3.0B p90-91
68 with m
.Case(MicrOp
.OP_TRAP
):
69 # TODO: put back use of fields, do not access insn bits direct
70 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
72 comb
+= to
.eq(op
.insn
[31-10:31-5])
76 comb
+= a_i
.eq(dut
.i
.a
)
77 comb
+= b_i
.eq(dut
.i
.b
)
79 a_s
= Signal(signed(64), reset_less
=True)
80 b_s
= Signal(signed(64), reset_less
=True)
81 a
= Signal(64, reset_less
=True)
82 b
= Signal(64, reset_less
=True)
84 with m
.If(op
.is_32bit
):
85 comb
+= a_s
.eq(exts(a_i
, 32, 64))
86 comb
+= b_s
.eq(exts(b_i
, 32, 64))
87 comb
+= a
.eq(a_i
[0:32])
88 comb
+= b
.eq(b_i
[0:32])
95 lt_s
= Signal(reset_less
=True)
96 gt_s
= Signal(reset_less
=True)
97 lt_u
= Signal(reset_less
=True)
98 gt_u
= Signal(reset_less
=True)
99 equal
= Signal(reset_less
=True)
101 comb
+= lt_s
.eq(a_s
< b_s
)
102 comb
+= gt_s
.eq(a_s
> b_s
)
103 comb
+= lt_u
.eq(a
< b
)
104 comb
+= gt_u
.eq(a
> b
)
105 comb
+= equal
.eq(a
== b
)
107 trapbits
= Signal(5, reset_less
=True)
108 comb
+= trapbits
.eq(Cat(gt_u
, lt_u
, equal
, gt_s
, lt_s
))
111 traptype
= op
.traptype
112 comb
+= take_trap
.eq(traptype
.any() |
(trapbits
& to
).any())
114 with m
.If(take_trap
):
115 expected_msr
= Signal(len(msr_o
.data
))
116 comb
+= expected_msr
.eq(op
.msr
)
118 comb
+= expected_msr
[MSR
.IR
].eq(0)
119 comb
+= expected_msr
[MSR
.DR
].eq(0)
120 comb
+= expected_msr
[MSR
.FE0
].eq(0)
121 comb
+= expected_msr
[MSR
.FE1
].eq(0)
122 comb
+= expected_msr
[MSR
.EE
].eq(0)
123 comb
+= expected_msr
[MSR
.RI
].eq(0)
124 comb
+= expected_msr
[MSR
.SF
].eq(1)
125 comb
+= expected_msr
[MSR
.TM
].eq(0)
126 comb
+= expected_msr
[MSR
.VEC
].eq(0)
127 comb
+= expected_msr
[MSR
.VSX
].eq(0)
128 comb
+= expected_msr
[MSR
.PR
].eq(0)
129 comb
+= expected_msr
[MSR
.FP
].eq(0)
130 comb
+= expected_msr
[MSR
.PMM
].eq(0)
131 comb
+= expected_msr
[MSR
.TEs
:MSR
.TEe
+1].eq(0)
132 comb
+= expected_msr
[MSR
.UND
].eq(0)
133 comb
+= expected_msr
[MSR
.LE
].eq(1)
135 with m
.If(op
.msr
[MSR
.TSs
:MSR
.TSe
+1] == 0b10):
136 comb
+= expected_msr
[MSR
.TSs
:MSR
.TSe
+1].eq(0b01)
138 comb
+= expected_msr
[MSR
.TSs
:MSR
.TSe
+1].eq(
139 op
.msr
[MSR
.TSs
:MSR
.TSe
+1]
142 expected_srr1
= Signal(len(srr1_o
.data
))
143 comb
+= expected_srr1
.eq(op
.msr
)
145 comb
+= expected_srr1
[63-36:63-32].eq(0)
146 comb
+= expected_srr1
[PI
.TRAP
].eq(traptype
== 0)
147 comb
+= expected_srr1
[PI
.PRIV
].eq(traptype
[1])
148 comb
+= expected_srr1
[PI
.FP
].eq(traptype
[0])
149 comb
+= expected_srr1
[PI
.ADR
].eq(traptype
[3])
150 comb
+= expected_srr1
[PI
.ILLEG
].eq(traptype
[4])
151 comb
+= expected_srr1
[PI
.TM_BAD_THING
].eq(0)
155 Assert(msr_o
.data
== expected_msr
),
157 Assert(srr0_o
.data
== op
.cia
),
159 Assert(srr1_o
.data
== expected_srr1
),
161 Assert(nia_o
.data
== op
.trapaddr
<< 4),
167 with m
.Case(MicrOp
.OP_SC
):
168 expected_msr
= Signal(len(msr_o
.data
))
169 comb
+= expected_msr
.eq(op
.msr
)
170 # Unless otherwise documented, these exceptions to the MSR bits
171 # are documented in Power ISA V3.0B, page 1063 or 1064.
172 comb
+= expected_msr
[MSR
.IR
].eq(0)
173 comb
+= expected_msr
[MSR
.DR
].eq(0)
174 comb
+= expected_msr
[MSR
.FE0
].eq(0)
175 comb
+= expected_msr
[MSR
.FE1
].eq(0)
176 comb
+= expected_msr
[MSR
.EE
].eq(0)
177 comb
+= expected_msr
[MSR
.RI
].eq(0)
178 comb
+= expected_msr
[MSR
.SF
].eq(1)
179 comb
+= expected_msr
[MSR
.TM
].eq(0)
180 comb
+= expected_msr
[MSR
.VEC
].eq(0)
181 comb
+= expected_msr
[MSR
.VSX
].eq(0)
182 comb
+= expected_msr
[MSR
.PR
].eq(0)
183 comb
+= expected_msr
[MSR
.FP
].eq(0)
184 comb
+= expected_msr
[MSR
.PMM
].eq(0)
185 # TODO: check ordering (which is smaller, which is larger)
186 # MSR.TSs or MSR.TSe+1?
187 comb
+= expected_msr
[MSR
.TEs
:MSR
.TEe
+1].eq(0)
188 comb
+= expected_msr
[MSR
.UND
].eq(0)
189 comb
+= expected_msr
[MSR
.LE
].eq(1)
191 # TODO: check ordering (which is smaller, which is larger)
192 # MSR.TSs or MSR.TSe+1?
193 # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c107
194 with m
.If(op
.msr
[MSR
.TSs
:MSR
.TSe
+1] == 0b10):
195 comb
+= expected_msr
[MSR
.TSs
:MSR
.TSe
+1].eq(0b01)
197 comb
+= expected_msr
[MSR
.TSs
:MSR
.TSe
+1].eq(
198 op
.msr
[MSR
.TSs
:MSR
.TSe
+1]
201 # Power ISA V3.0B, Book 2, Section 3.3.1
202 # TODO: put back use of fields, do not access insn bits direct
203 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
204 with m
.If(field(op
.insn
, 20, 26) == 1):
205 comb
+= expected_msr
[MSR
.HV
].eq(1)
207 comb
+= expected_msr
[MSR
.HV
].eq(0)
210 Assert(dut
.o
.srr0
.ok
),
214 Assert(dut
.o
.srr0
.data
== (op
.cia
+ 4)[0:64]),
215 Assert(field(srr1_o
, 33, 36) == 0),
216 Assert(field(srr1_o
, 42, 47) == 0),
217 Assert(field(srr1_o
, 0, 32) == field(msr_i
, 0, 32)),
218 Assert(field(srr1_o
, 37, 41) == field(msr_i
, 37, 41)),
219 Assert(field(srr1_o
, 48, 63) == field(msr_i
, 48, 63)),
221 Assert(msr_o
.data
== expected_msr
),
223 # TODO: put back use of fields, do not access insn bits direct
224 # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
225 # XXX what is this for? it is not possible to identify
226 # it because the "direct access to insn bits" provides
227 # absolutely no clue as to its purpose.
228 # also: this is likely to be wrong because of PowerISA
229 # field ordering (see V3.0B p4 section 1.3.4)
230 with m
.If(field(op
.insn
, 20, 26) == 1):
231 comb
+= Assert(msr_o
[MSR
.HV
] == 1)
233 comb
+= Assert(msr_o
[MSR
.HV
] == 0)
238 with m
.Case(MicrOp
.OP_RFID
):
244 # Note: going through the spec pseudo-code, line-by-line,
245 # in order, with these assertions. idea is: compare
246 # *directly* against the pseudo-code. therefore, leave
247 # numbering in (from pseudo-code) and add *comments* about
248 # which field it is (3 == HV etc.)
250 # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
251 with m
.If(msr_i
[3]): # HV
252 comb
+= Assert(msr_o
[51] == srr1_i
[51]) # ME from SRR1
254 comb
+= Assert(msr_o
[51] == msr_i
[51]) # ME from MSR (in)
257 # spec: MSR[3] <- (MSR[3] & SRR1[3])
258 Assert(msr_o
[3] == (srr1_i
[3] & msr_i
[3])), # HV
261 # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
262 # MSR[29:31] <- SRR1[29:31]
263 with m
.If((field(msr_i
, 29, 31) != 0b010) |
264 (field(srr1_i
, 29, 31) != 0b000)):
265 comb
+= Assert(field(msr_o
.data
, 29, 31) ==
266 field(srr1_i
, 29, 31))
268 comb
+= Assert(field(msr_o
.data
, 29, 31) ==
269 field(msr_i
, 29, 31))
271 # check EE (48) IR (58), DR (59): PR (49) will over-ride
273 Assert(msr_o
[48] == (srr1_i
[48] | srr1_i
[48])), # EE
274 Assert(msr_o
[58] == (srr1_i
[58] | srr1_i
[58])), # IR
275 Assert(msr_o
[59] == (srr1_i
[59] | srr1_i
[59])), # DR
278 # remaining bits: straight copy. don't know what these are:
279 # just trust the v3.0B spec is correct.
281 Assert(field(msr_o
, 0, 2) == field(srr1_i
, 0, 2)),
282 Assert(field(msr_o
, 4, 28) == field(srr1_i
, 4, 28)),
283 Assert(field(msr_o
, 32) == field(srr1_i
, 32)),
284 Assert(field(msr_o
, 37, 41) == field(srr1_i
, 37, 41)),
285 Assert(field(msr_o
, 49, 50) == field(srr1_i
, 49, 50)),
286 Assert(field(msr_o
, 52, 57) == field(srr1_i
, 52, 57)),
287 Assert(field(msr_o
, 60, 63) == field(srr1_i
, 60, 63)),
290 # check NIA against SRR0. 2 LSBs are set to zero (word-align)
291 comb
+= Assert(nia_o
.data
== Cat(Const(0, 2), dut
.i
.srr0
[2:]))
293 comb
+= dut
.i
.ctx
.matches(dut
.o
.ctx
)
298 class TrapMainStageTestCase(FHDLTestCase
):
299 def test_formal(self
):
300 self
.assertFormal(Driver(), mode
="bmc", depth
=10)
301 self
.assertFormal(Driver(), mode
="cover", depth
=10)
303 def test_ilang(self
):
304 vl
= rtlil
.convert(Driver(), ports
=[])
305 with
open("trap_main_stage.il", "w") as f
:
309 if __name__
== '__main__':