TRAP pipeline formal correctness proof needed
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.
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
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]) ?
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.
(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.
(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.
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.
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.
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.
(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.
(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.
(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.
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).
(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.
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?
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
(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
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?
(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.
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
(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? :)
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.
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
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*.
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".
(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.
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...
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
Addressed comments; will resume with where I left off tomorrow.
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
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.)
(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.
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 :)