from nmutil.extend import exts
from nmutil.formaltest import FHDLTestCase
-from soc.consts import MSR, PI, TT
+from soc.consts import MSR, MSRb, PI, TT, field
from soc.decoder.power_enums import MicrOp
from soc.fu.trap.trap_input_record import CompTrapOpSubset
-def field(r, start, end=None):
- """Answers with a subfield of the signal r ("register"), where
- the start and end bits use IBM conventions. start < end.
- """
- if end is None:
- return r[3-start]
- return r[63-end:64-start]
-
-
class Driver(Elaboratable):
"""
"""
comb += op.eq(rec)
+ d_fields = dut.fields.FormD
+ sc_fields = dut.fields.FormSC
+
# start of properties
with m.Switch(op.insn_type):
# TDI/TWI/TD/TW. v3.0B p90-91
###############
with m.Case(MicrOp.OP_TRAP):
- # TODO: put back use of fields, do not access insn bits direct
- # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
- to = Signal(5)
- comb += to.eq(op.insn[31-10:31-5])
+ to = Signal(len(d_fields.TO))
+ comb += to.eq(d_fields.TO[0:-1])
a_i = Signal(64)
b_i = Signal(64)
expected_msr = Signal(len(msr_o.data))
comb += expected_msr.eq(op.msr)
- comb += expected_msr[MSR.IR].eq(0)
- comb += expected_msr[MSR.DR].eq(0)
- comb += expected_msr[MSR.FE0].eq(0)
- comb += expected_msr[MSR.FE1].eq(0)
- comb += expected_msr[MSR.EE].eq(0)
- comb += expected_msr[MSR.RI].eq(0)
- comb += expected_msr[MSR.SF].eq(1)
- comb += expected_msr[MSR.TM].eq(0)
- comb += expected_msr[MSR.VEC].eq(0)
- comb += expected_msr[MSR.VSX].eq(0)
- comb += expected_msr[MSR.PR].eq(0)
- comb += expected_msr[MSR.FP].eq(0)
- comb += expected_msr[MSR.PMM].eq(0)
- comb += expected_msr[MSR.TEs:MSR.TEe+1].eq(0)
- comb += expected_msr[MSR.UND].eq(0)
- comb += expected_msr[MSR.LE].eq(1)
-
- with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10):
- comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(0b01)
- with m.Else():
- comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(
- op.msr[MSR.TSs:MSR.TSe+1]
- )
+ 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
+ #
+ # saf2: no it's not. Proof by substitution:
+ #
+ # field(R,MSRb.TEs,MSRb.TEe).eq(0)
+ # == field(R,53,54).eq(0)
+ # == R[field_slice(53,54)].eq(0)
+ # == R[slice(63-54, (63-53)+1)].eq(0)
+ # == R[slice(9, 11)].eq(0)
+ # == R[9:11].eq(0)
+ #
+ # Also put proof in py-doc for field().
+
+ 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)
- 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)
+ # Per V3.0B, page 1075
+ comb += field(expected_srr1, 33, 36).eq(0)
+ comb += field(expected_srr1, 42).eq(0) # TM_BAD_THING
+ comb += field(expected_srr1, 43).eq(traptype[0]) # FP
+ comb += field(expected_srr1, 44).eq(traptype[4]) # ILLEG
+ comb += field(expected_srr1, 45).eq(traptype[1]) # PRIV
+ comb += field(expected_srr1, 46).eq(traptype == 0) # TRAP
+ comb += field(expected_srr1, 47).eq(traptype[3]) # ADDR
comb += [
Assert(msr_o.ok),
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.
- comb += expected_msr[MSR.IR].eq(0)
- comb += expected_msr[MSR.DR].eq(0)
- comb += expected_msr[MSR.FE0].eq(0)
- comb += expected_msr[MSR.FE1].eq(0)
- comb += expected_msr[MSR.EE].eq(0)
- comb += expected_msr[MSR.RI].eq(0)
- comb += expected_msr[MSR.SF].eq(1)
- comb += expected_msr[MSR.TM].eq(0)
- comb += expected_msr[MSR.VEC].eq(0)
- comb += expected_msr[MSR.VSX].eq(0)
- comb += expected_msr[MSR.PR].eq(0)
- comb += expected_msr[MSR.FP].eq(0)
- comb += expected_msr[MSR.PMM].eq(0)
- comb += expected_msr[MSR.TEs:MSR.TEe+1].eq(0)
- comb += expected_msr[MSR.UND].eq(0)
- comb += expected_msr[MSR.LE].eq(1)
-
- with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10):
- comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(0b01)
- with m.Else():
- comb += expected_msr[MSR.TSs:MSR.TSe+1].eq(
- op.msr[MSR.TSs:MSR.TSe+1]
- )
-
- # Power ISA V3.0B, Book 2, Section 3.3.1
- # TODO: put back use of fields, do not access insn bits direct
- # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
- with m.If(field(op.insn, 20, 26) == 1):
- comb += expected_msr[MSR.HV].eq(1)
- with m.Else():
- comb += expected_msr[MSR.HV].eq(0)
+ # 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)
+ 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)
comb += [
Assert(dut.o.srr0.ok),
Assert(msr_o.data == expected_msr),
]
- # TODO: put back use of fields, do not access insn bits direct
- # see https://bugs.libre-soc.org/show_bug.cgi?id=421#c24
- # XXX what is this for? it is not possible to identify
- # it because the "direct access to insn bits" provides
- # absolutely no clue as to its purpose.
- # also: this is likely to be wrong because of PowerISA
- # field ordering (see V3.0B p4 section 1.3.4)
- with m.If(field(op.insn, 20, 26) == 1):
- comb += Assert(msr_o[MSR.HV] == 1)
- with m.Else():
- comb += Assert(msr_o[MSR.HV] == 0)
###################
# RFID. v3.0B p955
comb += [
Assert(msr_o.ok),
Assert(nia_o.ok),
- ]
+ ]
# Note: going through the spec pseudo-code, line-by-line,
# in order, with these assertions. idea is: compare
# which field it is (3 == HV etc.)
# spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
- with m.If(msr_i[3]): # HV
- comb += Assert(msr_o[51] == srr1_i[51]) # ME from SRR1
+ with m.If(field(msr_i, 3)): # HV
+ comb += Assert(field(msr_o, 51) == field(srr1_i, 51)) # ME
with m.Else():
- comb += Assert(msr_o[51] == msr_i[51]) # ME from MSR (in)
-
- comb += [
- # spec: MSR[3] <- (MSR[3] & SRR1[3])
- Assert(msr_o[3] == (srr1_i[3] & msr_i[3])), # HV
- ]
+ comb += Assert(field(msr_o, 51) == field(msr_i, 51)) # ME
# if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
# MSR[29:31] <- SRR1[29:31]
# check EE (48) IR (58), DR (59): PR (49) will over-ride
comb += [
- Assert(msr_o[48] == (srr1_i[48] | srr1_i[48])), # EE
- Assert(msr_o[58] == (srr1_i[58] | srr1_i[58])), # IR
- Assert(msr_o[59] == (srr1_i[59] | srr1_i[59])), # DR
+ Assert(
+ field(msr_o, 48) ==
+ field(srr1_i, 48) | field(srr1_i, 49)
+ ),
+ Assert(
+ field(msr_o, 58) ==
+ field(srr1_i, 58) | field(srr1_i, 49)
+ ),
+ Assert(
+ field(msr_o, 59) ==
+ field(srr1_i, 59) | field(srr1_i, 49)
+ ),
]
# remaining bits: straight copy. don't know what these are:
projects / soc.git / blobdiff