Bug 421 - TRAP pipeline formal correctness proof needed
Summary: TRAP pipeline formal correctness proof needed
Status: IN_PROGRESS
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Samuel A. Falvo II
URL:
Depends on:
Blocks: 325
  Show dependency treegraph
 
Reported: 2020-07-07 12:23 BST by Luke Kenneth Casson Leighton
Modified: 2020-12-02 19:47 GMT (History)
2 users (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 500
budget (EUR) for this task, excluding subtasks' budget: 500
parent task for budget allocation: 195
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
"samuel"=400 "lkcl"={amount=100, paid=2020-10-19}


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-07-07 12:23:18 BST
TRAP pipeline formal correctness proof needed
Comment 1 Luke Kenneth Casson Leighton 2020-07-17 21:44:56 BST
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/trap/main_stage.py;hb=HEAD

if you look at the fixedtrap wiki page containing the pseudocode, traps nominally in PowerISA do testing of 5 bits.  however what we have added here is an unofficial "microcoding" system using two extra parameters to the Record OpSubset: traotype and trapaddr.

traptype when set will make an *unconditional* trap that *does not* need RA or RB.
Comment 2 Luke Kenneth Casson Leighton 2020-07-17 22:21:58 BST
here is the pseudocode pages for the ops implemented in TRAP.

https://libre-soc.org/openpower/isa/fixedtrap/
https://libre-soc.org/openpower/isa/sprset/
https://libre-soc.org/openpower/isa/system/

if you look closely at the regs they use (and set) you will notice that td/tw, sc, rfid, mtmsr and mfmsr all have very similar register usage profiles, hence why we put them all in the same pipeline.

in fact sc does basically nearly the exact same thing as an unconditional trap, just with an address 0xc00 instead of 0x700
Comment 3 Samuel A. Falvo II 2020-07-18 04:46:31 BST
    comb += msr_o.data[MSR.ME].eq((msr_i[MSR.HV] & srr1_i[MSR.HV]) |
                                  (~msr_i[MSR.HV] & srr1_i[MSR.HV]))


Per DeMorgan's Theorems, isn't this statement the same as:

    comb += msr_o.data[MSR.ME].eq(srr1_i[MSR.HV])

?
Comment 4 Samuel A. Falvo II 2020-07-18 04:49:25 BST
I must be doing something stupifyingly stupid.  I'm just not able to satisfy the properties for the RFID instruction.

I can only guess that I'm unable to understand the order of precedence by which bits in the output MSR are set.  Several bits of the output has a plurality of drivers, and I suspect they're interacting in non-obvious ways.
Comment 5 Samuel A. Falvo II 2020-07-18 05:12:11 BST
(In reply to Samuel A. Falvo II from comment #4)
> I must be doing something stupifyingly stupid.  I'm just not able to satisfy
> the properties for the RFID instruction.
> 
> I can only guess that I'm unable to understand the order of precedence by
> which bits in the output MSR are set.  Several bits of the output has a
> plurality of drivers, and I suspect they're interacting in non-obvious ways.

WIP pushed to the repo.
Comment 6 Luke Kenneth Casson Leighton 2020-07-18 10:11:47 BST
(In reply to Samuel A. Falvo II from comment #3)
>     comb += msr_o.data[MSR.ME].eq((msr_i[MSR.HV] & srr1_i[MSR.HV]) |
>                                   (~msr_i[MSR.HV] & srr1_i[MSR.HV]))
> 
> 
> Per DeMorgan's Theorems, isn't this statement the same as:
> 
>     comb += msr_o.data[MSR.ME].eq(srr1_i[MSR.HV])
> 
> ?

that's a bug, yay!  spec - in the pseudo-code - is this:

    MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
    MSR[3] <- (MSR[3] & SRR1[3])

but the words say this:

    If MSR3=1 then bits 3 and 51 of SRR1 are placed into
    the corresponding bits of the MSR.

do those look consistent to you? (nobody has really properly
reviewed the pseudocode in the spec so inconsistencies are
expected)

i've updated main_stage.py to use an if statement rather
than the & / | masking for bits 51 and 3.
Comment 7 Luke Kenneth Casson Leighton 2020-07-18 10:53:00 BST
ok so i read the spec here a bit more closely, and the msr_copy
function is being used to copy a range of bits from SRR1 to MSR,
which, if, following that, some bits of SRR1/MSR were set, then
some bits in MSR need to be *restored* i.e. the original (msr_i)
needs to overwrite those bits, instead.

i think the best thing to suggest, here, sam, is for the formal
proof to do what the *pseudocode* does, *not* what trap main_stage.py
does.

however i think what i am going to have to do is to alter the
pseudo-code and write to the openpower-hdl-cores list (again)
to notify them of a discrepancy in the pseudo-code.
Comment 8 Luke Kenneth Casson Leighton 2020-07-18 11:05:11 BST
i started writing it out (to do the same thing as MSR51) and this:

    MSR[3] <- (MSR[3] & SRR1[3]) | ((¬MSR[3] & MSR[3]))

basically that last part is zero and *reduces* to

    MSR[3] <- (MSR[3] & SRR1[3])

so yes the spec is correct.

therefore, samuel, i suggest ignoring main_stage.py entirely
and converting that pseudo-code into Asserts.  nothing fancy,
no functions called, no use of is_ok, no use of full_function_bits.

just straight line-for-line direct translation.

that way, anyone looking at the pseudo-code and the proof side-by-side
can go "ths line is correct, this line is correct, this line is correct"
and we stand a chance of getting it right.

as you know, the point of the proofs is to have clarity, not speed.
Comment 9 Luke Kenneth Casson Leighton 2020-07-19 05:16:09 BST
https://git.libre-soc.org/?p=nmutil.git;a=commitdiff;h=aeed18a63d687cdaa9c00b98d46c66583fef6e2d

the python function you're looking for is "__eq__"

see the SelectableInt class for an example.

although in this case i think "matches" is a better name because otherwise people may make the same error.
Comment 10 Samuel A. Falvo II 2020-07-20 22:31:10 BST
(In reply to Luke Kenneth Casson Leighton from comment #6)
> that's a bug, yay!  spec - in the pseudo-code - is this:
> 
>     MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
>     MSR[3] <- (MSR[3] & SRR1[3])

Where do I find this and similar relevant pseudocode?  I've looked through the wiki without success.  I've found a POWER9 ISA manual online, but it lacks anything like the detail given above.  I've checked out the OpenPOWER ISA spec 3.0b that is linked from the wiki, and ... I have to admit I'm deeply flustered by my inability to locate useful information in that document.
Comment 11 Samuel A. Falvo II 2020-07-20 22:34:29 BST
(In reply to Luke Kenneth Casson Leighton from comment #6)
>     If MSR3=1 then bits 3 and 51 of SRR1 are placed into
>     the corresponding bits of the MSR.
> 
> do those look consistent to you? (nobody has really properly
> reviewed the pseudocode in the spec so inconsistencies are
> expected)

In this particular case, yes; but it requires some thought to see it.

If MSR[3]=1, then MSR[3] and MSR[51] are overwritten.

If MSR[3]=0, then MSR[3] and MSR[51] are to remain stable.  But, since MSR[3] is already 0, the logical AND of MSR[3] with SRR1[3] will result in a 0, thus keeping this bit stable.
Comment 12 Luke Kenneth Casson Leighton 2020-07-20 23:18:36 BST
(In reply to Samuel A. Falvo II from comment #10)
> (In reply to Luke Kenneth Casson Leighton from comment #6)
> > that's a bug, yay!  spec - in the pseudo-code - is this:
> > 
> >     MSR[51] <- (MSR[3] & SRR1[51]) | ((¬MSR[3] & MSR[51]))
> >     MSR[3] <- (MSR[3] & SRR1[3])
> 
> Where do I find this and similar relevant pseudocode?

https://libre-soc.org/openpower/isa/

i believe i add the links at the top of each source file.

i added the ones to  proof_main_stage.py a few days ago?

>  I've looked through
> the wiki without success.  I've found a POWER9 ISA manual online, but it
> lacks anything like the detail given above. 

actually the pseudocode is taken directly from the v3.0B spec, using pdf2txt and a *lot* of hand editing of the resultant dog's dinner mess.

> I've checked out the OpenPOWER
> ISA spec 3.0b that is linked from the wiki, and ... I have to admit I'm
> deeply flustered by my inability to locate useful information in that
> document.

i use xpdf, and its search capability is pretty quick given it's a 1500 page document.

start at the top and search "rfid" or "twi" and the sections which describe each instruction come up pretty quickly.
Comment 13 Samuel A. Falvo II 2020-07-20 23:27:15 BST
I should be more precise; I can find the instruction pseudo-code for TWI, et. al. easily enough.  What's missing is when the pseudocode says "TRAP" and dead-ends there.  What does that mean, precisely?  Even the chapter on Interrupts says that the behavior of traps is dependent on what causes the trap, and unless I missed something, nothing in that chapter mentions any of the trap instructions outside of system call.  I cannot find the place in the specs where fixed-point facility traps are discussed (even if only by reference).
Comment 14 Luke Kenneth Casson Leighton 2020-07-21 00:00:45 BST
(In reply to Samuel A. Falvo II from comment #13)
> I should be more precise; I can find the instruction pseudo-code for TWI,
> et. al. easily enough.  What's missing is when the pseudocode says "TRAP"
> and dead-ends there.

ah, yes. i found that particularly obtuse.
i had to ask / work it out.

see trap function in ISACaller and in trap main_stage.py

CIA is stored in SRR0
NIA is set to 0x700
MSR is stored in SRR1
MSR is set to something.


>  What does that mean, precisely?  Even the chapter on
> Interrupts says that the behavior of traps is dependent on what causes the
> trap,

sigh yes there is a boatload of different behaviours, a whole ton of flags, you will see a reference to where they start.

the 0x700 trap has its own definitions and meaning of the bits

0xc00 exception has different meanings.

it does all make sense once you know the context.


> and unless I missed something, nothing in that chapter mentions any of
> the trap instructions outside of system call.

to be honest i have no idea what tdi, twi etc are used for.

and again to be honest i am not going to worry about it.  all that matters is getting the functionality right.

i agree it would be nice to know how rhey are used but i learned from my reverse enhineering days very quickly that understanding or lack of is *not* necessarily an impediment to forward progress.  it is a false correlation to believe so.


>  I cannot find the place in
> the specs where fixed-point facility traps are discussed (even if only by
> reference).

this might be a good question to ask on openhdl-cores openpower foundation list.
Comment 15 Samuel A. Falvo II 2020-07-21 00:18:39 BST
OK, new commit pushed; I reworked the SC properties and implemented the RFID properties following the documented pseudocode.  Looks like bits 29-31 of MSR is not set right when executing RFID.  Is this another bug?
Comment 16 Luke Kenneth Casson Leighton 2020-07-21 00:22:40 BST
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/trap/main_stage.py;h=39f4326d1697d70a86aadbd892bbeef2057c4970;hb=HEAD#l153

reference to book chapter section which explains PI.PRIV flag definitions.

these bitfields do *not* mean anything for exception address 0xc00, they *only* mean something for 0x700 (trap address).

btw yes that really is address 0x700 as in physical memory address 0x00000700
Comment 17 Luke Kenneth Casson Leighton 2020-07-21 00:30:05 BST
(In reply to Samuel A. Falvo II from comment #15)
> OK, new commit pushed; I reworked the SC properties and implemented the RFID
> properties following the documented pseudocode.  Looks like bits 29-31 of
> MSR is not set right when executing RFID.  Is this another bug?

let's check.

  87                 with m.If((field(dut.i.msr, 29, 31) != 0b010) |
  88                           (field(dut.i.msr, 29, 31) != 0b000)):
  89                     comb += Assert(field(msr_o.data, 29, 31) == field(srr1_i, 29, 31))
 
first, is an "Else" is missing there?


let's grab the pseudocode

if (MSR[29:31] != 0b010) | (SRR1[29:31] != 0b000) then
    MSR[29:31] <- SRR1[29:31]

ah! the 2nd comparison, line 88, should be dut.i.srr1 != 0b000

you have dut.i.msr != 0b000
Comment 18 Luke Kenneth Casson Leighton 2020-07-21 00:48:48 BST
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/trap/formal/proof_main_stage.py;h=48221f2945dd115b31bf34dfc7fb5b3919c1d601;hb=HEAD#l28

should that be +1 on 63-start i.e. 64-start because python slice?
Comment 19 Samuel A. Falvo II 2020-07-21 05:23:57 BST
(In reply to Luke Kenneth Casson Leighton from comment #18)
> https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/trap/formal/
> proof_main_stage.py;h=48221f2945dd115b31bf34dfc7fb5b3919c1d601;hb=HEAD#l28
> 
> should that be +1 on 63-start i.e. 64-start because python slice?

Yes, thank you.  Good catch.

I'm noticing that the trap logic does not drive o.msr.ok; should it?  According to the SC pseudo-code, MSR is updated, along with SRR0 and SRR1.
Comment 20 Luke Kenneth Casson Leighton 2020-07-21 10:50:57 BST
commit 6530c0ccadadf834dc66e95941ae27c01de52da4 (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Tue Jul 21 10:50:37 2020 +0100

    corrections to trap proof see
    https://bugs.libre-soc.org/show_bug.cgi?id=421#c17 and
    https://bugs.libre-soc.org/show_bug.cgi?id=421#c18

commit 2595e209a67e8721436bbb4caeadf2ae0e9d90b1
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Tue Jul 21 10:45:33 2020 +0100

    use alias for msr_i in trap proof

commit 0949e113f0979adb56e1e8af4106d39bfd56b55f
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Tue Jul 21 10:41:36 2020 +0100

    correct trap spec page interrupt ref
Comment 21 Luke Kenneth Casson Leighton 2020-07-21 10:58:29 BST
(In reply to Samuel A. Falvo II from comment #19)
> (In reply to Luke Kenneth Casson Leighton from comment #18)
> > https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/trap/formal/
> > proof_main_stage.py;h=48221f2945dd115b31bf34dfc7fb5b3919c1d601;hb=HEAD#l28
> > 
> > should that be +1 on 63-start i.e. 64-start because python slice?
> 
> Yes, thank you.  Good catch.

committed (see comment #20)

> I'm noticing that the trap logic does not drive o.msr.ok; should it? 
> According to the SC pseudo-code, MSR is updated, along with SRR0 and SRR1.

err... err... ah.
https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L621

yep: a trap does not actually modify MSR.  iinteresting.

even for exceptions (which also write NIA and SRR1) they're still not
modifying MSR, it's *SRR1* that contains the modifications (setting
one of the trap bits as defined in section 6.5.9 book III)

if exception occurs write *SRR1*:
https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L1037

how was this not caught by the trap unit test? moo? :)
Comment 22 Luke Kenneth Casson Leighton 2020-07-21 11:16:35 BST
https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L478

damn.  completely missed this.  that when SRR1 is written to, bits
in MSR are also changed.  i cut/paste the microwatt code so as to
action it, but missed it

https://bugs.libre-soc.org/show_bug.cgi?id=325#c2

ok give me a mo to update that.
Comment 23 Luke Kenneth Casson Leighton 2020-07-21 14:12:48 BST
samuel: you were right, several bits need updating in the MSR.
which *sigh* means it needed first copying.  i'm going to make
some additional changes: move cia and msr into the *input record*
(CompTrapOpSubset in trap_input_record.py) and likewise for
spr_input_record.py

commit d8443042357b41ffaf57f480ff2e1d5b8343c73c (HEAD -> master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Tue Jul 21 14:10:54 2020 +0100

    add msr exception bits setting function in hardware
    and do same thing in ISACaller trap
Comment 24 Luke Kenneth Casson Leighton 2020-07-22 12:47:05 BST
https://libre-soc.org/openpower/isatables/fields.text

hi samuel, trap proof progressing well. comments:

         with m.If(field(op.insn, 20, 26) == 1):

please don't do this.  use the fields/forms.  without the fields/forms it is impossible to read the proof and crossreference it to the spec.

the only locations where this practice is still used is where microwatt code has not yet had the field/form identified.

now to return back to the field/form, you will find this extremely difficult because the raw bits *contain no information*.

this difficulty is precisely why the decision to use fields/forms was made.

in addition some fields are not contiguous, they are spread across *multiple bits* in a non-obvious order.

the last thing we need is "manual construction" duplicating exactly what DecodeFields *already does*.

if this is of concern then we should have a proof of *DecodeFields*.
Comment 25 Luke Kenneth Casson Leighton 2020-07-22 13:06:00 BST
samuel: regarding system call (sc) LEV, this is in the spec (v3.0B, p952):

setting of the MSR is affected by the contents of the
LEV field. LEV values greater than 1 are reserved. Bits
0:5 of the LEV field (instruction bits 20:25) are treated
as a reserved field.

    Programming Note
If LEV=1 the hypervisor is invoked. This is the only
way that executing an instruction can cause hyper-
visor state to be entered.

note: like microwatt, we are *not* supporting hypervisor mode (yet).
we're code-tracking microwatt, so the proof needs to cover what
parts of the spec that *microwatt* implements, rather than "purely
and strictly the spec".
Comment 26 Luke Kenneth Casson Leighton 2020-07-22 13:13:10 BST
(In reply to Luke Kenneth Casson Leighton from comment #24)
> https://libre-soc.org/openpower/isatables/fields.text
> if this is of concern then we should have a proof of *DecodeFields*.

or, i don't mind this - at all:

    sc_fields = decoder.fields.FormSC
    LEV = sc_fields.LEV[0:-1]
    comb += lev.eq(LEV)
    comb += Assert(op.insn[31-20:31-27] == lev) # check lev gets correct bits

followed by using *lev* in the ongoing assertions, likewise for TO.

that i like.

but referring directly to the bits themselves such that information and
clarity is completely lost, when people like myself have had huge difficulty
working with PowerISA bit-numbering?  mmm... no.

you can see even in the example above, i got it wrong, because i forgot
that the fields are in *PowerISA* order, which is, according to p4 section
1.3.2 Notation, in the ***REVERSE*** order from normal conventions.

bit 0 is the **MSB** in PowerISA notation.

the use of FieldSelectableInt (which is behind the Decoder Fields) takes
care of that automatically for us.
Comment 27 Luke Kenneth Casson Leighton 2020-07-22 13:48:00 BST
commit bb40a98bcbce1bab7eb86cf4ba0d1d3788cd86ca (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Wed Jul 22 13:42:53 2020 +0100

    code-shuffle, add comments

samuel i've added some code-comments and shuffled the Asserts, which allow
humans to read the pseudo-code (in line order), and stand a chance of
verifying it.

the use of the actual field names (MSR.HV) *actually prevents* this
rather than aids and assists in it, because the soc.consts file containing
the MSR numbering class has to be opened, side-by-side with proof_main_stage.py
*and* with the spec PDF...
Comment 28 Luke Kenneth Casson Leighton 2020-07-22 15:57:04 BST
commit 64087f35f6b1e10429615836ec9077b55e8e85fd (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Wed Jul 22 15:48:18 2020 +0100

    field number ordering wrong way round?
    see https://bugs.libre-soc.org/show_bug.cgi?id=325#c107
Comment 29 Samuel A. Falvo II 2020-07-24 06:41:33 BST
Addressed comments; will resume with where I left off tomorrow.
Comment 30 Luke Kenneth Casson Leighton 2020-07-25 12:10:16 BST
commit ad905e82a09f3daa051d267608d7283ff8fa5e03 (HEAD -> master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Sat Jul 25 12:09:30 2020 +0100

    make trap proof section more readable
Comment 31 Samuel A. Falvo II 2020-07-26 21:40:42 BST
I've completed implementing the properties for the trap pipeline; however, there seems to be an irreconcilable issue with the trap pipeline.  For some reason, during the execution of MTMSRD, (IBM) bit 30 of MSR remains in the wrong state, and I've not been able to figure out why.  I've double-checked the properties against the documented specs in the V3.0B specs (page 978); I've also reviewed the code in main_stage.py.  I can't locate the discrepency.  I will need someone else to take over from here.

Everything else, so far at least, seems to run OK.

Can someone please double-check and advise?  Thanks.

(I'm going to move this task to complete in my wiki page; but, if needed, I'll move it back to in progress.)
Comment 32 Luke Kenneth Casson Leighton 2020-07-26 22:31:14 BST
(In reply to Samuel A. Falvo II from comment #31)

> discrepency.  I will need someone else to take over from here.

ok cando.

> 
> Everything else, so far at least, seems to run OK.

superb.  will take a look tomorrow.

> Can someone please double-check and advise?  Thanks.
> 
> (I'm going to move this task to complete in my wiki page; but, if needed,
> I'll move it back to in progress.)

ok next one is shift_rot or mul.
Comment 33 Luke Kenneth Casson Leighton 2020-07-27 12:50:44 BST
gaah, that was a handful :)

first, i had to put in a series of individual Asserts rather than
assign to expected_msr then check it in one go.  this allowed me
to tell which *part* of the MSR field was wrong, and i confirmed
that yes it was something to do with bit 30.

after doing that i found that um actually there wasn't a "problem",
until i added the "else" clause:

                    with m.Else():
                        comb += Assert(F(msr_od, 29, 31) == F(msr_i, 29, 31))

*then* it failed, and at that point i went "oink" and found that this
was *missing* from trap main_stage.py

                    # put *back* bits 29-31 (MSB0 notation)
                    bits = field_slice(29, 31)
                    with m.If((msr_i[bits] == Const(0b010, 3)) &
                               (a_i[bits] == Const(0b000, 3))):
                         comb += msr_o.data[bits].eq(msr_i[bits])

and that was the source of the problem.

hurrah for formal correctness proofs!

oh - OP_RFID pseudo-code, which i reviewed at the same time, turned out to be
an accidental amalgamation of V3.1B and v3.0B spec (MSR.S - bit 41 - is not
examined in v3.0B, where it is for v3.0B)

all in all a good outcome.  i think we can close this one soon.


commit 944dc6b7129d06a936643863bfb572a5ba70b19f (HEAD -> master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Mon Jul 27 12:44:44 2020 +0100

    fix trap proof, and trap main_stage, and pseudocode for rfid
    all a bit of a mess, really :)