X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsoc%2Ffu%2Ftrap%2Fformal%2Fproof_main_stage.py;h=1816afacbcbcc9aae19dd94e066e9f1793aa729d;hb=07fd5bf7bab87056f705cc58cbfb316157811551;hp=511ad9cb0962b90a82be7fec46411decacdb2924;hpb=14d7655b1afd1b4540b98f4ecc672c6ce0edfd3a;p=soc.git diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py index 511ad9cb..1816afac 100644 --- a/src/soc/fu/trap/formal/proof_main_stage.py +++ b/src/soc/fu/trap/formal/proof_main_stage.py @@ -19,7 +19,7 @@ from nmigen.cli import rtlil 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 @@ -28,15 +28,6 @@ from soc.fu.trap.pipe_data import TrapPipeSpec 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): """ """ @@ -59,6 +50,9 @@ 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): @@ -66,10 +60,8 @@ class Driver(Elaboratable): # 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) @@ -115,40 +107,50 @@ class Driver(Elaboratable): 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), @@ -169,37 +171,24 @@ class Driver(Elaboratable): 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), @@ -215,17 +204,6 @@ class Driver(Elaboratable): 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 @@ -234,7 +212,7 @@ class Driver(Elaboratable): 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 @@ -243,15 +221,10 @@ class Driver(Elaboratable): # 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] @@ -265,9 +238,18 @@ class Driver(Elaboratable): # 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: