from nmutil.extend import exts
from nmutil.formaltest import FHDLTestCase
-from soc.consts import MSR, MSRb, PI, TT, field
+from openpower.consts import MSR, MSRb, PI, TT, field
-from soc.decoder.power_enums import MicrOp
+from openpower.decoder.power_enums import MicrOp
from soc.fu.trap.main_stage import TrapMainStage
from soc.fu.trap.pipe_data import TrapPipeSpec
comb = m.d.comb
rec = CompTrapOpSubset()
- pspec = TrapPipeSpec(id_wid=2)
+ pspec = TrapPipeSpec(id_wid=2, parent_pspec=None)
m.submodules.dut = dut = TrapMainStage(pspec)
srr0_o, srr0_i = dut.o.srr0, dut.i.srr0
srr1_o, srr1_i = dut.o.srr1, dut.i.srr1
nia_o = dut.o.nia
+ rs = dut.i.a
comb += op.eq(rec)
+ # expected values
+ exp_msr = Signal(len(msr_o.data))
+ exp_srr1 = Signal(len(srr1_o.data))
+
d_fields = dut.fields.FormD
sc_fields = dut.fields.FormSC
+ x_fields = dut.fields.FormX
+
+ L = x_fields.L[0:-1]
+
+ # This alias exists because some of our assertions exceed PEP8
+ # width constraints. Avoid using this alias in the general
+ # case; ONLY use it when you're simultaneously trying to preserve
+ # line-oriented readability (to make the code easy to compare with
+ # the v3.0B spec) while simultaneously preserving PEP8 compliance.
+ F = field
# start of properties
with m.Switch(op.insn_type):
comb += take_trap.eq(traptype.any() | (trapbits & to).any())
with m.If(take_trap):
- expected_msr = Signal(len(msr_o.data))
- comb += expected_msr.eq(op.msr)
-
- comb += field(expected_msr, MSRb.IR).eq(0)
- comb += field(expected_msr, MSRb.DR).eq(0)
- comb += field(expected_msr, MSRb.FE0).eq(0)
- comb += field(expected_msr, MSRb.FE1).eq(0)
- comb += field(expected_msr, MSRb.EE).eq(0)
- comb += field(expected_msr, MSRb.RI).eq(0)
- comb += field(expected_msr, MSRb.SF).eq(1)
- comb += field(expected_msr, MSRb.TM).eq(0)
- comb += field(expected_msr, MSRb.VEC).eq(0)
- comb += field(expected_msr, MSRb.VSX).eq(0)
- comb += field(expected_msr, MSRb.PR).eq(0)
- comb += field(expected_msr, MSRb.FP).eq(0)
- comb += field(expected_msr, MSRb.PMM).eq(0)
-
- # still wrong.
- # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c120
- comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
-
- comb += field(expected_msr, MSRb.UND).eq(0)
- comb += field(expected_msr, MSRb.LE).eq(1)
-
- expected_srr1 = Signal(len(srr1_o.data))
- comb += expected_srr1.eq(op.msr)
-
- # note here: 36 is ***LESS*** than 32 ***BUT***
- # ***63-36*** is less than 63-32
- # could do with using field_slice here however
- # *get the number order right*.
-
- # however before doing that: why are these bits
- # initialised to zero then every single one of them
- # is over-ridden? 5 bits, 32-36 (36-32, haha)
- # are set to zero, then 5 bits are set to expressions.
-
- # redundant comb += expected_srr1[63-36:63-32].eq(0)
-
- comb += expected_srr1[PI.TRAP].eq(traptype == 0)
- comb += expected_srr1[PI.PRIV].eq(traptype[1])
- comb += expected_srr1[PI.FP].eq(traptype[0])
- comb += expected_srr1[PI.ADR].eq(traptype[3])
- comb += expected_srr1[PI.ILLEG].eq(traptype[4])
- comb += expected_srr1[PI.TM_BAD_THING].eq(0)
+ comb += exp_msr.eq(op.msr)
+
+ # these are all set depending on the trap address (type)
+ # see V3.0B p1063 however as noted in main_stage.py
+ # the types of interrupts supported all need the same
+ # values (for now)
+ comb += field(exp_msr, MSRb.IR).eq(0)
+ comb += field(exp_msr, MSRb.DR).eq(0)
+ comb += field(exp_msr, MSRb.FE0).eq(0)
+ comb += field(exp_msr, MSRb.FE1).eq(0)
+ comb += field(exp_msr, MSRb.EE).eq(0)
+ comb += field(exp_msr, MSRb.RI).eq(0)
+ comb += field(exp_msr, MSRb.SF).eq(1)
+ comb += field(exp_msr, MSRb.TM).eq(0)
+ comb += field(exp_msr, MSRb.VEC).eq(0)
+ comb += field(exp_msr, MSRb.VSX).eq(0)
+ comb += field(exp_msr, MSRb.PR).eq(0)
+ comb += field(exp_msr, MSRb.FP).eq(0)
+ comb += field(exp_msr, MSRb.PMM).eq(0)
+
+ comb += field(exp_msr, MSRb.TEs, MSRb.TEe).eq(0)
+
+ comb += field(exp_msr, MSRb.UND).eq(0)
+ comb += field(exp_msr, MSRb.LE).eq(1)
+
+ comb += exp_srr1.eq(op.msr)
+
+ # Per V3.0B, page 1075
+ comb += field(exp_srr1, 33, 36).eq(0)
+ comb += field(exp_srr1, 42).eq(0) # TM_BAD_THING
+ comb += field(exp_srr1, 43).eq(traptype[0]) # FP
+ comb += field(exp_srr1, 44).eq(traptype[4]) # ILLEG
+ comb += field(exp_srr1, 45).eq(traptype[1]) # PRIV
+ comb += field(exp_srr1, 46).eq(traptype == 0) # TRAP
+ comb += field(exp_srr1, 47).eq(traptype[3]) # ADDR
comb += [
Assert(msr_o.ok),
- Assert(msr_o.data == expected_msr),
+ Assert(msr_o.data == exp_msr),
Assert(srr0_o.ok),
Assert(srr0_o.data == op.cia),
Assert(srr1_o.ok),
- Assert(srr1_o.data == expected_srr1),
+ Assert(srr1_o.data == exp_srr1),
Assert(nia_o.ok),
Assert(nia_o.data == op.trapaddr << 4),
]
- #################
- # SC. v3.0B p952
- #################
- with m.Case(MicrOp.OP_SC):
- expected_msr = Signal(len(msr_o.data))
- comb += expected_msr.eq(op.msr)
- # Unless otherwise documented, these exceptions to the MSR bits
- # are documented in Power ISA V3.0B, page 1063 or 1064.
- # We are not supporting hypervisor or transactional semantics,
- # so we skip enforcing those fields' properties.
- comb += field(expected_msr, MSRb.IR).eq(0)
- comb += field(expected_msr, MSRb.DR).eq(0)
- comb += field(expected_msr, MSRb.FE0).eq(0)
- comb += field(expected_msr, MSRb.FE1).eq(0)
- comb += field(expected_msr, MSRb.EE).eq(0)
- comb += field(expected_msr, MSRb.RI).eq(0)
- comb += field(expected_msr, MSRb.SF).eq(1)
- comb += field(expected_msr, MSRb.TM).eq(0)
- comb += field(expected_msr, MSRb.VEC).eq(0)
- comb += field(expected_msr, MSRb.VSX).eq(0)
- comb += field(expected_msr, MSRb.PR).eq(0)
- comb += field(expected_msr, MSRb.FP).eq(0)
- comb += field(expected_msr, MSRb.PMM).eq(0)
- # XXX no. slice quantity still inverted producing an empty list
- # https://bugs.libre-soc.org/show_bug.cgi?id=325#c120
- # also add a comment explaining this very non-obvious
- # behaviour
- comb += field(expected_msr, MSRb.TEs, MSRb.TEe).eq(0)
- comb += field(expected_msr, MSRb.UND).eq(0)
- comb += field(expected_msr, MSRb.LE).eq(1)
+ ###################
+ # MTMSR
+ # Specs found on V3.0B, page 977.
+ ###################
+
+ with m.Case(MicrOp.OP_MTMSR):
+ comb += exp_msr.eq(msr_i) # will copy and override
+
+ with m.If(L == 0):
+ comb += [
+ field(exp_msr, 48).eq(field(rs, 48) | field(rs, 49)),
+ field(exp_msr, 58).eq(field(rs, 58) | field(rs, 49)),
+ field(exp_msr, 59).eq(field(rs, 59) | field(rs, 49)),
+ field(exp_msr, 32, 47).eq(field(rs, 32, 47)),
+ field(exp_msr, 49, 50).eq(field(rs, 49, 50)),
+ field(exp_msr, 52, 57).eq(field(rs, 52, 57)),
+ field(exp_msr, 60, 62).eq(field(rs, 60, 62)),
+ ]
+ with m.Else():
+ # L=1 only checks 48 and 62
+ comb += [
+ field(exp_msr, 48).eq(field(rs, 48)),
+ field(exp_msr, 62).eq(field(rs, 62)),
+ ]
comb += [
- Assert(dut.o.srr0.ok),
- Assert(srr1_o.ok),
+ Assert(msr_o.data == exp_msr),
Assert(msr_o.ok),
+ ]
- Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
- Assert(field(srr1_o, 33, 36) == 0),
- Assert(field(srr1_o, 42, 47) == 0),
- Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
- Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
- Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
+ ###################
+ # MTMSRD
+ # Specs found on V3.0B, page 978.
+ ###################
+
+ with m.Case(MicrOp.OP_MTMSRD):
+ msr_od = msr_o.data # another "shortener"
+
+ with m.If(L == 0):
+ # if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
+ # MSR[29:31] <- SRR1[29:31]
+ with m.If((field(msr_i, 29, 31) != 0b010) |
+ (field(rs, 29, 31) != 0b000)):
+ comb += Assert(F(msr_od, 29, 31) == F(rs, 29, 31))
+ with m.Else():
+ comb += Assert(F(msr_od, 29, 31) == F(msr_i, 29, 31))
+
+ # MSR[48] <- (RS)[48] | (RS)[49]
+ # MSR[58] <- (RS)[58] | (RS)[49]
+ # MSR[59] <- (RS)[59] | (RS)[49]
+ PR = field(rs, 49) # alias/copy of SRR1 PR field
+ comb += [
+ Assert(field(msr_od, 48) == field(rs, 48) | PR),
+ Assert(field(msr_od, 58) == field(rs, 58) | PR),
+ Assert(field(msr_od, 59) == field(rs, 59) | PR),
+ ]
+
+ comb += [
+ # Ambiguity in specification on page 978 of V3.0B:
+ # MSR[4:28] <- RS[4 6:28].
+ #
+ # I've decided to follow the prose in the programmer
+ # note just underneath the typographical ambiguity.
+ # MSR[4:28] <- RS[4:28].
+
+ # range = 0:2 4:28 32:40 42:47 49:50 52:57 60:62
+ # MSR[range] <- (RS)[range]
+ Assert(field(msr_od, 0, 2) == field(rs, 0, 2)),
+ Assert(field(msr_od, 4, 28) == field(rs, 4, 28)),
+ Assert(field(msr_od, 32, 47) == field(rs, 32, 47)),
+ Assert(field(msr_od, 49, 50) == field(rs, 49, 50)),
+ Assert(field(msr_od, 52, 57) == field(rs, 52, 57)),
+ Assert(field(msr_od, 60, 62) == field(rs, 60, 62)),
+ ]
+ with m.Else():
+ # L=1 only checks 48 and 62 (MSR.EE, MSR.RI)
+ comb += [
+ Assert(field(msr_od, 48) == field(rs, 48)),
+ Assert(field(msr_od, 62) == field(rs, 62)),
+ ]
+
+ comb += Assert(msr_o.ok)
- Assert(msr_o.data == expected_msr),
+ ###################
+ # MFMSR
+ ###################
+
+ with m.Case(MicrOp.OP_MFMSR):
+ comb += [
+ Assert(dut.o.o.ok),
+ Assert(dut.o.o.data == msr_i),
]
###################
# RFID. v3.0B p955
###################
with m.Case(MicrOp.OP_RFID):
+ msr_od = msr_o.data # another "shortener"
comb += [
Assert(msr_o.ok),
Assert(nia_o.ok),
]
- # XXX code comment has been removed, which explains
- # why the code is written the way it is written
- # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c127
+ # Note: going through the spec pseudo-code, line-by-line,
+ # in order, with these assertions. idea is: compare
+ # *directly* against the pseudo-code. therefore, leave
+ # numbering in (from pseudo-code) and add *comments* about
+ # which field it is (3 == HV etc.)
- # XXX restore HV check
- # https://bugs.libre-soc.org/show_bug.cgi?id=325#c125
+ # spec: MSR[51] <- MSR[3] & SRR1[51]
+ comb += Assert(field(msr_o, 3) == field(srr1_i, 3))
# if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
# MSR[29:31] <- SRR1[29:31]
- with m.If((field(msr_i , 29, 31) != 0b010) |
+ with m.If((field(msr_i, 29, 31) != 0b010) |
(field(srr1_i, 29, 31) != 0b000)):
- comb += Assert(field(msr_o.data, 29, 31) ==
- field(srr1_i, 29, 31))
+ comb += Assert(F(msr_od, 29, 31) == F(srr1_i, 29, 31))
with m.Else():
- comb += Assert(field(msr_o.data, 29, 31) ==
- field(msr_i, 29, 31))
+ comb += Assert(F(msr_od, 29, 31) == F(msr_i, 29, 31))
# check EE (48) IR (58), DR (59): PR (49) will over-ride
-
- # XXX does not look as clear. revert
- # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c122
- for bit in [48, 58, 59]:
- comb += Assert(
- field(msr_o, bit) ==
- (field(srr1_i, bit) | field(srr1_i, 49))
- )
+ # MSR[48] <- (RS)[48] | (RS)[49]
+ # MSR[58] <- (RS)[58] | (RS)[49]
+ # MSR[59] <- (RS)[59] | (RS)[49]
+ PR = field(srr1_i, 49) # alias/copy of SRR1 PR field
+ comb += [
+ Assert(field(msr_od, 48) == field(srr1_i, 48) | PR),
+ Assert(field(msr_od, 58) == field(srr1_i, 58) | PR),
+ Assert(field(msr_od, 59) == field(srr1_i, 59) | PR),
+ ]
# remaining bits: straight copy. don't know what these are:
# just trust the v3.0B spec is correct.
+ # range = 0:2 4:28 32:40 42:47 49:50 52:57 60:62
+ # MSR[range] <- (RS)[range]
comb += [
- Assert(field(msr_o, 0, 2) == field(srr1_i, 0, 2)),
- Assert(field(msr_o, 4, 28) == field(srr1_i, 4, 28)),
- Assert(field(msr_o, 32) == field(srr1_i, 32)),
- Assert(field(msr_o, 37, 41) == field(srr1_i, 37, 41)),
- Assert(field(msr_o, 49, 50) == field(srr1_i, 49, 50)),
- Assert(field(msr_o, 52, 57) == field(srr1_i, 52, 57)),
- Assert(field(msr_o, 60, 63) == field(srr1_i, 60, 63)),
+ Assert(field(msr_od, 0, 2) == field(srr1_i, 0, 2)),
+ Assert(field(msr_od, 4, 28) == field(srr1_i, 4, 28)),
+ Assert(field(msr_od, 32) == field(srr1_i, 32)),
+ Assert(field(msr_od, 37, 41) == field(srr1_i, 37, 41)),
+ Assert(field(msr_od, 49, 50) == field(srr1_i, 49, 50)),
+ Assert(field(msr_od, 52, 57) == field(srr1_i, 52, 57)),
+ Assert(field(msr_od, 60, 63) == field(srr1_i, 60, 63)),
]
# check NIA against SRR0. 2 LSBs are set to zero (word-align)
comb += Assert(nia_o.data == Cat(Const(0, 2), dut.i.srr0[2:]))
+ #################
+ # SC. v3.0B p952
+ #################
+ with m.Case(MicrOp.OP_SC):
+ comb += exp_msr.eq(op.msr)
+ # Unless otherwise documented, these exceptions to the MSR bits
+ # are documented in Power ISA V3.0B, page 1063 or 1064.
+ # We are not supporting hypervisor or transactional semantics,
+ # so we skip enforcing those fields' properties.
+ comb += field(exp_msr, MSRb.IR).eq(0)
+ comb += field(exp_msr, MSRb.DR).eq(0)
+ comb += field(exp_msr, MSRb.FE0).eq(0)
+ comb += field(exp_msr, MSRb.FE1).eq(0)
+ comb += field(exp_msr, MSRb.EE).eq(0)
+ comb += field(exp_msr, MSRb.RI).eq(0)
+ comb += field(exp_msr, MSRb.SF).eq(1)
+ comb += field(exp_msr, MSRb.TM).eq(0)
+ comb += field(exp_msr, MSRb.VEC).eq(0)
+ comb += field(exp_msr, MSRb.VSX).eq(0)
+ comb += field(exp_msr, MSRb.PR).eq(0)
+ comb += field(exp_msr, MSRb.FP).eq(0)
+ comb += field(exp_msr, MSRb.PMM).eq(0)
+ comb += field(exp_msr, MSRb.TEs, MSRb.TEe).eq(0)
+ comb += field(exp_msr, MSRb.UND).eq(0)
+ comb += field(exp_msr, MSRb.LE).eq(1)
+
+ comb += [
+ Assert(dut.o.srr0.ok),
+ Assert(srr1_o.ok),
+ Assert(msr_o.ok),
+
+ Assert(dut.o.srr0.data == (op.cia + 4)[0:64]),
+ Assert(field(srr1_o, 33, 36) == 0),
+ Assert(field(srr1_o, 42, 47) == 0),
+ Assert(field(srr1_o, 0, 32) == field(msr_i, 0, 32)),
+ Assert(field(srr1_o, 37, 41) == field(msr_i, 37, 41)),
+ Assert(field(srr1_o, 48, 63) == field(msr_i, 48, 63)),
+
+ Assert(msr_o.data == exp_msr),
+ ]
+
comb += dut.i.ctx.matches(dut.o.ctx)
return m
if __name__ == '__main__':
unittest.main()
-