Bug 419 - MUL pipeline formal proof needed
Summary: MUL pipeline formal proof needed
Status: CONFIRMED
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: 482
Blocks: 195 323
  Show dependency treegraph
 
Reported: 2020-07-07 12:16 BST by Luke Kenneth Casson Leighton
Modified: 2021-11-29 21:29 GMT (History)
3 users (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 550
budget (EUR) for this task, excluding subtasks' budget: 550
parent task for budget allocation: 195
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
kc5tja = 500 lkcl = { amount = 50, submitted = 2021-04-24, paid = 2021-05-01 }


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:16:14 BST
a MUL pipeline formal correctness proof is needed
Comment 1 Luke Kenneth Casson Leighton 2020-08-11 11:59:03 BST
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/mul/pipeline.py;h=f5a0f069b94e314fcfe43a74486f9d29b763e3f0;hb=HEAD#l10

samuel try a copy of this, add the extra stage.  i believe PipeModBase does the same thing as i described on the list (StageChain) which will have the advantahe you should be able to just drop it in place and use dut.i and dut.o
Comment 2 Samuel A. Falvo II 2020-08-18 23:16:52 BST
(In reply to Luke Kenneth Casson Leighton from comment #1)
> samuel try a copy of this, add the extra stage.  i believe PipeModBase does
> the same thing as i described on the list (StageChain) which will have the
> advantahe you should be able to just drop it in place and use dut.i and dut.o

I spent some time trying to understand what you're suggesting here.  I tried to just instantiate a MulBasePipe as the DUT, but I get 13 screensful of errors because it doesn't support the expected interface for .i and .o members.

I don't understand how copying the code in that class would help though; can you clarify?  Thanks.
Comment 3 Luke Kenneth Casson Leighton 2020-08-19 03:32:05 BST
(In reply to Samuel A. Falvo II from comment #2)

> I don't understand how copying the code in that class would help though; can
> you clarify?  Thanks.

apologies, we need to speed things up, a lot.  i will explain why at an appropriate time.

https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=d3deda12916c450f05f7d03610f0ef79c9cbdafb

i have set up a triple chain using StageChain which you can see was being called from nmutil PipeModBase.  i had to work out how to use it because the last time i called StageChain was 18 months ago.

a dummy object is set up with a dut.i and dut.o so that the remaining cut/pasted code does not need significant mods.

you can go ahead and use dut.i and dut.o as if there was a single combinatorial block between them, from a single module.

stage 1 abs's its input
stage 2 does the mul
stage 3 works out which bits of result to use

however with all 3 chained together you can ignore that entirely and implement the  OP_MUL* microcode operations in any way you see fit that is preferably simple and clear.

however please do not be surprised to find that symbiyosys MUL runs as slow as molasses flowing downhill in arctic winter.  there is not a lot we can do about that.
Comment 4 Jacob Lifshay 2020-08-19 04:10:37 BST
(In reply to Luke Kenneth Casson Leighton from comment #3)
> however please do not be surprised to find that symbiyosys MUL runs as slow
> as molasses flowing downhill in arctic winter.  there is not a lot we can do
> about that.

Wow, molasses can be scary:
https://en.wikipedia.org/wiki/Great_Molasses_Flood
Comment 5 Samuel A. Falvo II 2020-08-19 05:14:53 BST
Can someone take a look at my latest commit?  I don't know what I'm doing with this, apparently.  Maybe I should look into other issues.
Comment 6 Luke Kenneth Casson Leighton 2020-08-19 07:25:12 BST
(In reply to Samuel A. Falvo II from comment #5)

> Can someone take a look at my latest commit?  I don't know what I'm doing
> with this, apparently.

neither do i!  i did however veery patiently investigate until i noticed
that OP_MUL_H32 is marked in the CSV file (major_31.csv) as being a 32-bit
op only, checked in pre_stage.py (eq32(is_32bit, xxx, zzz)) and then
realised, "argh, if we try to validate OP_MUL_H32 with is_32bit=False
it's not going to produce valid data"

so i added this:

            with m.Case(MicrOp.OP_MUL_H32):
                comb += Assume(rec.is_32bit) # OP_MUL_H32 is a 32-bit op

and it's now "working".  i say "working", i mean "running at 100% CPU for
the past 10 minutes"

>  Maybe I should look into other issues.

well, here's what i explained to Cole: the most important thing for this
project is that people are doing *something*, and *communicating*.

you can see how verbose things are on bugreports with Cole, and it took
quite a lot of reinforcement that that is *okay*, because talking things
things over in "English" is often far better.

if you're running into issues, *please don't wait an entire week*!  even
half an hour is far too long - a week is over 300x that reasonable limit!

[as long as it is on-topic] you cannot be too verbose in using the bugtracker
to think things through.  even if you type it and then find the answer
yourself: hit send anyway because it contains a record of your thoughts,
which is as useful for you (if they turn out later to be wrong) as it is for
project archiving and audit purposes.
Comment 7 Luke Kenneth Casson Leighton 2020-08-19 07:30:44 BST
commit 2e117c06cb6b147e59e80fcba6d060695c62766e (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Wed Aug 19 07:24:58 2020 +0100

    bit of a reorg of mul proof, tracking down missing
    Assume op.is_32bit == 0 for OP_MUL_H32

ok now we've worked out that OP_MUL_H32 is only suited to 32-bit,
the next step is to do the signed multiply.  this is the implementation
from decode/helpers.py of a python-based signed multiply:

# signed version of MUL
def MULS(a, b):
    a_s = a.value & (1 << (a.bits-1)) != 0
    b_s = b.value & (1 << (b.bits-1)) != 0
    result = abs(a) * abs(b)
    print("MULS", result, a_s, b_s)
    if a_s == b_s:
        return result
    return -result 

because - again - OP_MUL_H32 *only* works on 32-bit numbers, we can
do:

   a_s = a[31]
   b_s = b[31]

rather than mungy-mess above (which copes with variable-size numbers)
Comment 8 Jacob Lifshay 2020-08-19 07:32:57 BST
(In reply to Luke Kenneth Casson Leighton from comment #6)
> [as long as it is on-topic] you cannot be too verbose in using the bugtracker
> to think things through.  even if you type it and then find the answer
> yourself: hit send anyway because it contains a record of your thoughts,
> which is as useful for you (if they turn out later to be wrong) as it is for
> project archiving and audit purposes.

They're also useful so others can see the pitfalls you fell into for what they are and avoid them.
Comment 9 Luke Kenneth Casson Leighton 2020-08-19 22:26:45 BST
it occurs to me that perhaps the error encountered here is the same one as for shift proof.
Comment 10 Samuel A. Falvo II 2020-08-29 20:43:21 BST
I *think* I've completed this pipeline proof.
Comment 11 Luke Kenneth Casson Leighton 2020-08-29 21:01:37 BST
(In reply to Samuel A. Falvo II from comment #10)
> I *think* I've completed this pipeline proof.

excellent, looks reasonable: i threw some comments in, could you put some
comments in (brief ones) as to why m63.bool() & ~m63.all() works, what it's
doing?  and why the abs values are used and why check on sign-comparison?

also i believe you missed dut.o.o.ok, there are some other proofs that
create a signal named "ok", set it to 1 at the top, then in the
"default" of the switch set it to zero.  works a treat.

need to check xer_ov as well (different method, there)

then i think we're good here?
Comment 12 Samuel A. Falvo II 2020-08-29 23:28:26 BST
(In reply to Luke Kenneth Casson Leighton from comment #11)
> excellent, looks reasonable: i threw some comments in, could you put some
> comments in (brief ones) as to why m63.bool() & ~m63.all() works, what it's
> doing?  and why the abs values are used and why check on sign-comparison?

Done.

> also i believe you missed dut.o.o.ok, there are some other proofs that
> create a signal named "ok", set it to 1 at the top, then in the
> "default" of the switch set it to zero.  works a treat.

Thanks for this; FOR NOW, I'd like to delay adding this until I fix the most recent breakage.  I just committed my recent changes, which by all accounts should work.  However, line 113 (asserting xer_ov_o == dut.i.ctx.xer_ov) consistently fails **as long as** I assign the convenience variable xer_ov_o = dut.o.xer_ov.data.  If I replace xer_ov_o with the referent dut.o.xer_ov.data, it consistently works.

I cannot explain this behavior.  Why should this ever be the case?

> need to check xer_ov as well (different method, there)

Not sure what you mean here?  Can you clarify?
Comment 13 Luke Kenneth Casson Leighton 2020-08-29 23:39:03 BST
(In reply to Samuel A. Falvo II from comment #12)
> (In reply to Luke Kenneth Casson Leighton from comment #11)
> > excellent, looks reasonable: i threw some comments in, could you put some
> > comments in (brief ones) as to why m63.bool() & ~m63.all() works, what it's
> > doing?  and why the abs values are used and why check on sign-comparison?
> 
> Done.
> 
> > also i believe you missed dut.o.o.ok, there are some other proofs that
> > create a signal named "ok", set it to 1 at the top, then in the
> > "default" of the switch set it to zero.  works a treat.
> 
> Thanks for this; FOR NOW, I'd like to delay adding this until I fix the most
> recent breakage.  I just committed my recent changes, which by all accounts
> should work.  However, line 113 (asserting xer_ov_o == dut.i.ctx.xer_ov)
> consistently fails **as long as** I assign the convenience variable xer_ov_o
> = dut.o.xer_ov.data.  If I replace xer_ov_o with the referent
> dut.o.xer_ov.data, it consistently works.

oink.

> I cannot explain this behavior.  Why should this ever be the case?

no idea.

sounds like a bug that needs raising (on nmigen).  

> > need to check xer_ov as well (different method, there)
> 
> Not sure what you mean here?  Can you clarify?

xer_ov.ok and o.ok are crucial signals that tell the regfiles to actually write the result.

if they are not checked then there is the possibility that whilst data is produced it never actually hits the regfile.

therefore Assert(dut.o.o.ok == something) and Assert(dut.o.xer_ov.ok == something) are needed.
Comment 14 Luke Kenneth Casson Leighton 2020-08-29 23:48:33 BST
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/mul/post_stage.py;h=dbe560e96e61c5ffbd2897e8d8345529aa101bad;hb=HEAD#l42

but, first, these need fixing.

* o.ok should never be set unconditionally.  this says "results are being produced all the time" which is Bad.

* xer_ov.ok should only be set if there is the possibility of an overflow: on MUL L64

will raise as a new bug
Comment 15 Samuel A. Falvo II 2020-08-30 00:39:46 BST
(In reply to Luke Kenneth Casson Leighton from comment #13)
> oink.

Fixed!

> xer_ov.ok and o.ok are crucial signals that tell the regfiles to actually
> write the result.

Right.  That's what I thought, but wasn't 100% sure.
Comment 16 Luke Kenneth Casson Leighton 2020-08-30 11:06:24 BST
(In reply to Samuel A. Falvo II from comment #15)
> (In reply to Luke Kenneth Casson Leighton from comment #13)
> > oink.
> 
> Fixed!
> 
> > xer_ov.ok and o.ok are crucial signals that tell the regfiles to actually
> > write the result.
> 
> Right.  That's what I thought, but wasn't 100% sure.

ok you implemented something slightly differently, checking the OE flag
(this is output_stage.py's job, which is not part of the chain).  we
chained these together:

        pipe1 = MulMainStage1(pspec)
        pipe2 = MulMainStage2(pspec)
        pipe3 = MulMainStage3(pspec)

where in fu/mul/pipeline.py you can see that OE checking is handled here:

        out = DivMulOutputStage(self.pspec)  # do CR, XER and out-invert etc.

so any Assertions involving OE would be erroneous.

the xer_ov.ok flag (and o.ok flag) are quite simple, they just tell the
Register Files, "results are available if you want them".

there does exist a Formal Correctness Proof for OutputStage, it does need
updating.
Comment 17 Luke Kenneth Casson Leighton 2020-08-30 11:06:52 BST
commit d8d6b488a97e638fdf497da3a2c1622937243a82 (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Sun Aug 30 11:00:37 2020 +0100

    tidyup on mul proof
Comment 18 Samuel A. Falvo II 2020-09-03 23:27:58 BST
Thanks for cleaning up the code; it reads a lot better.  I do have some questions though.

(In reply to Luke Kenneth Casson Leighton from comment #16)
> the xer_ov.ok flag (and o.ok flag) are quite simple, they just tell the
> Register Files, "results are available if you want them".

Can you help me understand why xer_ov.ok is reset only in the default case?  As I understand the ISA specs, xer_ov.ok should only be set when OE=1.  I feel like I'm missing something.

> there does exist a Formal Correctness Proof for OutputStage, it does need
> updating.

I looked in the fu/mul hierarchy for this correctness proof, but did not find it.  Are you perhaps referring to alu/formal/proof_output_stage.py ?
Comment 19 Luke Kenneth Casson Leighton 2020-09-04 00:27:53 BST
(In reply to Samuel A. Falvo II from comment #18)
> Thanks for cleaning up the code; it reads a lot better.  I do have some
> questions though.

> Can you help me understand why xer_ov.ok is reset only in the default case? 
> As I understand the ISA specs, xer_ov.ok should only be set when OE=1.  I
> feel like I'm missing something.

OutputStage, which is *not included in the chain in this proof*, handles OE checking.

check for yourself:

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/mul/formal/proof_main_stage.py;h=0cf767f341668663a4f4c736af5aea5625c1c0d2;hb=HEAD#l88

is OutputStage in that chain? no it is not.

therefore trying to Assert things that *are not part of the test* is simply never going to work, is it?

> > there does exist a Formal Correctness Proof for OutputStage, it does need
> > updating.
> 
> I looked in the fu/mul hierarchy for this correctness proof, but did not
> find it. 

yes.  it's in the alu dir.

> Are you perhaps referring to alu/formal/proof_output_stage.py ?

yes.

if we were to include OutputStage in the chain at line 88, then the contents of alu proof_output_stage.py would need to be duplicated in their entirety in mul proof, wouldn't they?

which would be a waste of effort.  therefore we don't do that.
Comment 20 Samuel A. Falvo II 2020-09-04 03:34:07 BST
(In reply to Luke Kenneth Casson Leighton from comment #19)
> therefore trying to Assert things that *are not part of the test* is simply
> never going to work, is it?

I'm just going by what is in the instruction documentation.

I think I see now, though; in OutputStage.py, there's a block of code which tests for the OE flag, and sets *its own* ov.ok output to 1 if set.  It completely ignores any ov.ok signal from previous stages.

Apologies if this all seems like I'm being daft; I'm just trying to get a grasp of the bigger picture.