From: Luke Kenneth Casson Leighton Date: Fri, 24 Jul 2020 09:40:32 +0000 (+0100) Subject: code review comments for trap and proof X-Git-Tag: semi_working_ecp5~589 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c0d37306316246c12b79e0982e97689531f97e9;p=soc.git code review comments for trap and proof --- diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py index 823a58f2..52218efb 100644 --- a/src/soc/fu/trap/formal/proof_main_stage.py +++ b/src/soc/fu/trap/formal/proof_main_stage.py @@ -120,14 +120,29 @@ class Driver(Elaboratable): 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) - comb += expected_srr1[63-36:63-32].eq(0) + # 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]) @@ -169,6 +184,10 @@ class Driver(Elaboratable): 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) @@ -197,6 +216,13 @@ class Driver(Elaboratable): 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 + + # XXX restore HV check + # https://bugs.libre-soc.org/show_bug.cgi?id=325#c125 + # 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) | @@ -208,6 +234,9 @@ class Driver(Elaboratable): field(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) == diff --git a/src/soc/fu/trap/main_stage.py b/src/soc/fu/trap/main_stage.py index 1632bfb1..43bc2c24 100644 --- a/src/soc/fu/trap/main_stage.py +++ b/src/soc/fu/trap/main_stage.py @@ -103,6 +103,10 @@ class TrapMainStage(PipeModBase): comb += msr_o.data[MSR.VEC].eq(0) comb += msr_o.data[MSR.FP].eq(0) comb += msr_o.data[MSR.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(msr_o.data, MSRb.TEs, MSRb.TEe).eq(0) comb += msr_o.data[MSR.UND].eq(0) if msr_hv is not None: @@ -218,11 +222,16 @@ class TrapMainStage(PipeModBase): for stt, end in [(1,12), (13, 32)]: comb += msr_o.data[stt:end].eq(a_i[stt:end]) msr_check_pr(m, msr_o.data) + + # XXX code removed, needs reverting. + # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c124 + # XXX + comb += msr_o.ok.eq(1) # move from MSR with m.Case(MicrOp.OP_MFMSR): - # TODO: some of the bits need zeroing? apparently not + # some of the bits need zeroing? apparently not comb += o.data.eq(msr_i) comb += o.ok.eq(1) @@ -242,6 +251,11 @@ class TrapMainStage(PipeModBase): # don't understand but it's in the spec. again: bits 32-34 # are copied from srr1_i and need *restoring* to msr_i + + # XXX bug introduced here. this needs to be field_slice(31, 29) + # see https://bugs.libre-soc.org/show_bug.cgi?id=325#c126 + # XXX + bits = field_slice(29, 31) # bits 29, 30, 31 (Power notation) with m.If((msr_i[bits] == Const(0b010, 3)) & (srr1_i[bits] == Const(0b000, 3))): @@ -257,16 +271,8 @@ class TrapMainStage(PipeModBase): # 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. - - # XXX see https://bugs.libre-soc.org/show_bug.cgi?id=325#c104 - # do not access op.insn bits directly: PowerISA requires - # that fields be REVERSED and that has not been done here, - # where self.fields.FormNNN has that handled. - - # in addition, we are following *microwatt* - which has - # not implemented hypervisor. therefore this is incorrect - # behaviour. see execute1.vhdl - # https://github.com/antonblanchard/microwatt/ + # however we are following *microwatt* - which has + # not implemented hypervisor. # jump to the trap address, return at cia+4 self.trap(m, 0xc00, cia_i+4)