From: Samuel A. Falvo II Date: Tue, 21 Jul 2020 21:16:34 +0000 (-0700) Subject: Refine properties to comply with spec X-Git-Tag: semi_working_ecp5~644 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9984b40168d554c6819adce1da187ec2066f90cf;p=soc.git Refine properties to comply with spec --- 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):