From 017647f06850a2cd8be5adda5ac9b9e7dc405211 Mon Sep 17 00:00:00 2001 From: "Samuel A. Falvo II" Date: Fri, 24 Jul 2020 08:21:29 -0700 Subject: [PATCH] WIP: addressing code review, restoring proofs, etc. --- src/soc/consts.py | 50 ++++++++++++++--- src/soc/fu/trap/formal/proof_main_stage.py | 65 ++++++++++++---------- src/soc/fu/trap/main_stage.py | 21 ++++--- 3 files changed, 92 insertions(+), 44 deletions(-) diff --git a/src/soc/consts.py b/src/soc/consts.py index 48d5ddf5..ff204488 100644 --- a/src/soc/consts.py +++ b/src/soc/consts.py @@ -22,25 +22,59 @@ def field_slice(msb0_start, msb0_end, field_width=64): """ if msb0_start >= msb0_end: raise ValueError( - "start ({}) must be less than end ({})".format(start, end) + "start ({}) must be less than end ({})".format(msb0_start, msb0_end) ) # sigh. MSB0 (IBM numbering) is inverted. converting to python # we *swap names* so as not to get confused by having "end, start" - end = (field_width-1) - msb0_start - start = (field_width-1) - msb0_end + lsb0_end = (field_width-1) - msb0_start + lsb0_start = (field_width-1) - msb0_end - return slice(start, end + 1) + return slice(lsb0_start, lsb0_end + 1) -def field(r, start, end=None): +def field(r, msb0_start, msb0_end=None, field_width=64): """Answers with a subfield of the signal r ("register"), where the start and end bits use IBM conventions. start < end, if end is provided. The range specified is inclusive on both ends. + + Answers with a subfield of the signal r ("register"), + where the start and end bits use IBM "MSB 0" conventions. + If end is not provided, a single bit subfield is returned. + + see: https://en.wikipedia.org/wiki/Bit_numbering#MSB_0_bit_numbering + + * assertion: msb0_start < msb0_end. + * The range specified is inclusive on both ends. + * field_width specifies the total number of bits (note: not bits-1) + + Example usage: + + comb += field(insn, 0, 6, field_width=32).eq(17) + # NOTE: NEVER DIRECTLY ACCESS OPCODE FIELDS IN INSTRUCTIONS. + # This example is purely for illustrative purposes only. + # Use self.fields.FormXYZ.etcetc instead. + + comb += field(msr, MSRb.TEs, MSRb.TEe).eq(0) + + Proof by substitution: + + field(insn, 0, 6, field_width=32).eq(17) + == insn[field_slice(0, 6, field_width=32)].eq(17) + == insn[slice((31-6), (31-0)+1)].eq(17) + == insn[slice(25, 32)].eq(17) + == insn[25:32].eq(17) + + field(msr, MSRb.TEs, MSRb.TEe).eq(0) + == field(msr, 53, 54).eq(0) + == msr[field_slice(53, 54)].eq(0) + == msr[slice((63-54), (63-53)+1)].eq(0) # note cross-over! + == msr[slice(9, 11)].eq(0) + == msr[9:11].eq(0) """ - if end is None: - return r[63 - start] + if msb0_end is None: + return r[(field_width - 1) - msb0_start] else: - return r[field_slice(start, end)] + return r[field_slice(msb0_start, msb0_end)] # Listed in V3.0B Book III Chap 4.2.1 diff --git a/src/soc/fu/trap/formal/proof_main_stage.py b/src/soc/fu/trap/formal/proof_main_stage.py index 52218efb..f550e23c 100644 --- a/src/soc/fu/trap/formal/proof_main_stage.py +++ b/src/soc/fu/trap/formal/proof_main_stage.py @@ -123,6 +123,18 @@ class Driver(Elaboratable): # 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) @@ -131,18 +143,6 @@ class Driver(Elaboratable): expected_srr1 = Signal(len(srr1_o.data)) comb += expected_srr1.eq(op.msr) - # 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]) @@ -184,10 +184,6 @@ 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) @@ -216,12 +212,17 @@ 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 + # Note: going through the spec pseudo-code, line-by-line, + # in order, with these assertions. idea is: compare + # *directly* against the pseudo-code. therefore, leave + # numbering in (from pseudo-code) and add *comments* about + # which field it is (3 == HV etc.) - # XXX restore HV check - # https://bugs.libre-soc.org/show_bug.cgi?id=325#c125 + # spec: MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51])) + with m.If(field(msr_i, 3)): # HV + comb += Assert(field(msr_o, 51) == field(srr1_i, 51)) # ME + with m.Else(): + 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] @@ -234,14 +235,20 @@ 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) == - (field(srr1_i, bit) | field(srr1_i, 49)) - ) + comb += [ + Assert( + field(msr_o.data, 48) == + field(srr1_i, 48) | field(srr1_i, 49) + ), + Assert( + field(msr_o.data, 58) == + field(srr1_i, 58) | field(srr1_i, 49) + ), + Assert( + field(msr_o.data, 59) == + field(srr1_i, 59) | field(srr1_i, 49) + ), + ] # remaining bits: straight copy. don't know what these are: # just trust the v3.0B spec is correct. diff --git a/src/soc/fu/trap/main_stage.py b/src/soc/fu/trap/main_stage.py index 72bdaf4d..80cb913c 100644 --- a/src/soc/fu/trap/main_stage.py +++ b/src/soc/fu/trap/main_stage.py @@ -220,9 +220,15 @@ class TrapMainStage(PipeModBase): 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 + # Per https://bugs.libre-soc.org/show_bug.cgi?id=325#c123, + # this actually *is* in the microwatt code now. + # + # hypervisor stuff. here: bits 3 (HV) and 51 (ME) were + # copied over by msr_copy but if HV was not set we need + # the *original* (msr_i) bits + with m.If(~msr_i[MSR.HV]): + comb += msr_o.data[MSR.HV].eq(msr_i[MSR.HV]) + comb += msr_o.data[MSR.ME].eq(msr_i[MSR.ME]) comb += msr_o.ok.eq(1) @@ -243,16 +249,17 @@ class TrapMainStage(PipeModBase): # MSR was in srr1: copy it over, however *caveats below* comb += msr_copy(msr_o.data, srr1_i, zero_me=False) # don't zero + with m.If(field(msr_i, 3)): # HV + comb += field(msr_o, 51).eq(field(srr1_i, 51)) # ME + with m.Else(): + comb += field(msr_o, 51).eq(field(msr_i, 51)) # ME + # check problem state msr_check_pr(m, msr_o.data) # 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))): -- 2.30.2