From 9984b40168d554c6819adce1da187ec2066f90cf Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Tue, 21 Jul 2020 14:16:34 -0700 Subject: [PATCH] Refine properties to comply with spec --- src/soc/consts.py | 8 ++++ src/soc/fu/trap/formal/proof_main_stage.py | 51 +++++++++++++++++++--- src/soc/fu/trap/main_stage.py | 16 ++++++- 3 files changed, 66 insertions(+), 9 deletions(-) diff --git a/src/soc/consts.py b/src/soc/consts.py index 341dfc9b..ea301db1 100644 --- a/src/soc/consts.py +++ b/src/soc/consts.py @@ -4,12 +4,20 @@ class MSR: SF = (63 - 0) # Sixty-Four bit mode HV = (63 - 3) # Hypervisor state + UND = (63 - 5) # Undefined behavior state (see Bk 2, Sect. 3.2.1) + TSs = (63 - 29) # Transactional State (subfield) + TSe = (63 - 30) # Transactional State (subfield) + TM = (63 - 31) # Transactional Memory Available + VEC = (63 - 38) # Vector Available + VSX = (63 - 40) # VSX Available S = (63 - 41) # Secure state EE = (63 - 48) # External interrupt Enable PR = (63 - 49) # PRoblem state FP = (63 - 50) # FP available ME = (63 - 51) # Machine Check int enable FE0 = (63 - 52) # Floating-Point Exception Mode 0 + TEs = (63 - 53) # Trace Enable (subfield) + TEe = (63 - 54) # Trace Enable (subfield) FE1 = (63 - 55) # Floating-Point Exception Mode 1 IR = (63 - 58) # Instruction Relocation DR = (63 - 59) # Data Relocation diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py index 0a1afbdb..5de01254 100644 --- a/src/soc/fu/trap/formal/proof_main_stage.py +++ b/src/soc/fu/trap/formal/proof_main_stage.py @@ -54,6 +54,36 @@ class Driver(Elaboratable): # start of properties with m.Switch(op.insn_type): with m.Case(MicrOp.OP_SC): + expected_msr = Signal(len(msr_o)) + comb += expected_msr.eq(op.msr) + comb += [ + expected_msr[MSR.IR].eq(0), + expected_msr[MSR.DR].eq(0), + expected_msr[MSR.FE0].eq(0), + expected_msr[MSR.FE1].eq(0), + expected_msr[MSR.EE].eq(0), + expected_msr[MSR.RI].eq(0), + expected_msr[MSR.SF].eq(1), + expected_msr[MSR.TM].eq(0), + expected_msr[MSR.VEC].eq(0), + expected_msr[MSR.VSX].eq(0), + expected_msr[MSR.PR].eq(0), + expected_msr[MSR.FP].eq(0), + expected_msr[MSR.PMM].eq(0), + expected_msr[MSR.TEs:MSR.TEe+1].eq(0), + expected_msr[MSR.UND].eq(0), + ] + + 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) + + with m.If(op.msr[MSR.TSs:MSR.TSe+1] == 0b10): # V3.0B, pg 1064 + 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 += [ Assert(dut.o.srr0.ok), Assert(srr1_o.ok), @@ -66,15 +96,22 @@ class Driver(Elaboratable): 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[0:16] == msr_i[0:16]), - Assert(msr_o[22:27] == msr_i[22:27]), - Assert(msr_o[31:64] == msr_i[31:64]), + Assert(msr_o == expected_msr), Assert(msr_o[MSR.IR] == 0), # No LPCR register input, Assert(msr_o[MSR.DR] == 0), # so assuming AIL=0. - Assert(msr_o[MSR.FE0] == 0), - Assert(msr_o[MSR.FE1] == 0), - Assert(msr_o[MSR.EE] == 0), - Assert(msr_o[MSR.RI] == 0), + Assert(msr_o[MSR.FE0] == 0), # V3.0B, pg 1063 + Assert(msr_o[MSR.FE1] == 0), # V3.0B, pg 1063 + Assert(msr_o[MSR.EE] == 0), # V3.0B, pg 1063 + Assert(msr_o[MSR.RI] == 0), # V3.0B, pg 1063 + Assert(msr_o[MSR.SF] == 1), # V3.0B, pg 1064 + Assert(msr_o[MSR.TM] == 0), # V3.0B, pg 1064 + Assert(msr_o[MSR.VEC] == 0), # V3.0B, pg 1064 + Assert(msr_o[MSR.VSX] == 0), # V3.0B, pg 1064 + Assert(msr_o[MSR.PR] == 0), # V3.0B, pg 1064 + Assert(msr_o[MSR.FP] == 0), # V3.0B, pg 1064 + Assert(msr_o[MSR.PMM] == 0), # V3.0B, pg 1064 + Assert(msr_o[MSR.TEs:MSR.TEe+1] == 0), # V3.0B, pg 1064 + Assert(msr_o[MSR.UND] == 0), # V3.0B, pg 1064 ] with m.If(field(op.insn, 20, 26) == 1): comb += Assert(msr_o[MSR.HV] == 1) diff --git a/src/soc/fu/trap/main_stage.py b/src/soc/fu/trap/main_stage.py index 5f711ff4..99a5bec9 100644 --- a/src/soc/fu/trap/main_stage.py +++ b/src/soc/fu/trap/main_stage.py @@ -77,7 +77,7 @@ class TrapMainStage(PipeModBase): comb += msr_copy(srr1_o.data, msr_i) # old MSR comb += srr1_o.ok.eq(1) - def msr_exception(self, m, trap_addr): + def msr_exception(self, m, trap_addr, msr_hv=None): """msr_exception - sets bits in MSR specific to an exception. the full list of what needs to be done is given in V3.0B Book III Section 6.5 p1063 however it turns out that for the @@ -96,6 +96,10 @@ class TrapMainStage(PipeModBase): comb += msr_o.data[MSR.DR].eq(0) comb += msr_o.data[MSR.RI].eq(0) comb += msr_o.data[MSR.LE].eq(1) + comb += msr_o.data[MSR.FE0].eq(0) + comb += msr_o.data[MSR.FE1].eq(0) + if msr_hv is not None: + comb += msr_o.data[MSR.HV].eq(msr_hv) comb += msr_o.ok.eq(1) def ispec(self): @@ -250,11 +254,19 @@ class TrapMainStage(PipeModBase): # scv is not covered here. currently an illegal instruction. # raising "illegal" is the decoder's job, not ours, here. + # According to V3.0B, Book II, section 3.3.1, the System Call + # instruction allows you to trap directly into the hypervisor + # if the opcode's LEV sub-field is equal to 1. + trap_to_hv = Signal(reset_less=True) + lev = Signal(6, reset_less=True) + comb += lev.eq(op[31-26:32-20]) + comb += trap_to_hv.eq(lev == Const(1, 6)) + # jump to the trap address, return at cia+4 self.trap(m, 0xc00, cia_i+4) # and update several MSR bits - self.msr_exception(m, 0xc00) + self.msr_exception(m, 0xc00, msr_hv=trap_to_hv) # TODO (later) #with m.Case(MicrOp.OP_ADDPCIS): -- 2.30.2