Bug 306 - Formal Correctness Proof for ALU pipeline
Summary: Formal Correctness Proof for ALU pipeline
Status: IN_PROGRESS
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Mac OS
: --- enhancement
Assignee: Samuel A. Falvo II
URL:
Depends on: 429 337
Blocks: 195 305
  Show dependency treegraph
 
Reported: 2020-05-10 12:33 BST by Luke Kenneth Casson Leighton
Modified: 2021-04-20 14:38 BST (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:
"donated"={amount=400, paid=2020-12-06} "samuel"={amount=100}


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-05-10 12:33:23 BST
https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/alu/formal;hb=HEAD

* OP_ADD: done
* OP_CMP: done however bug in 32 bit not done
* OP_EXTS: done
* OP_CMPEQB: done however setting RT out and CR out not properly detected
Comment 1 Luke Kenneth Casson Leighton 2020-05-10 14:01:02 BST
python3 alu/formal/proof_main_stage.py ..
----------------------------------------------------------------------
Ran 2 tests in 312.563s

wooow :)
Comment 2 Michael Nolan 2020-05-10 14:46:03 BST
(In reply to Luke Kenneth Casson Leighton from comment #1)
> python3 alu/formal/proof_main_stage.py ..
> ----------------------------------------------------------------------
> Ran 2 tests in 312.563s
> 
> wooow :)

Yeah, adding shifts to the proof *really* slowed it down
Comment 4 Luke Kenneth Casson Leighton 2020-05-25 01:42:30 BST
hmm

the same thing we noted in Branch, for CMPEQB is also not being picked up n the main_stage.py

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

cmpeqb is only supposed to alter the CR, not the main register RT.

the formal proof is not picking that up.
Comment 5 Luke Kenneth Casson Leighton 2020-05-27 14:34:21 BST
  70         comb += Assume(a[32:64] == 0)
  71         comb += Assume(b[32:64] == 0)

michael in the alu proof should those be conditional? with m.If(op.is_32bit)?
Comment 6 Michael Nolan 2020-05-27 15:01:40 BST
(In reply to Luke Kenneth Casson Leighton from comment #5)
>   70         comb += Assume(a[32:64] == 0)
>   71         comb += Assume(b[32:64] == 0)
> 
> michael in the alu proof should those be conditional? with m.If(op.is_32bit)?

oh, yep. Fixed.
Comment 7 Luke Kenneth Casson Leighton 2020-05-27 15:06:22 BST
(In reply to Michael Nolan from comment #6)
> (In reply to Luke Kenneth Casson Leighton from comment #5)
> >   70         comb += Assume(a[32:64] == 0)
> >   71         comb += Assume(b[32:64] == 0)
> > 
> > michael in the alu proof should those be conditional? with m.If(op.is_32bit)?
> 
> oh, yep. Fixed.

star.
Comment 8 Luke Kenneth Casson Leighton 2020-07-14 21:29:10 BST
assigning to Samuel for review of formal_main_stage.py up to this point:

        # Assert that op gets copied from the input to output
        for rec_sig in rec.ports():
            name = rec_sig.name
            dut_sig = getattr(dut.o.ctx.op, name)
            comb += Assert(dut_sig == rec_sig)

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;hb=HEAD#l56
Comment 9 Luke Kenneth Casson Leighton 2020-07-14 21:31:41 BST
from commit git diff 685b7 769a8, samuel did this:

+        # Output context is the same as the input context.
+        comb += Assert(dut.o.ctx != dut.i.ctx)

this is the reasonable expectation: both are Records.  should it be
ok to Assert that one Record's contents equals the contents of another?
Comment 11 Samuel A. Falvo II 2020-08-18 23:27:44 BST
(In reply to Luke Kenneth Casson Leighton from comment #10)
> a bug in cmp was found
> 
> https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/main_stage.py;
> h=b2d2279cf80dec3670d70e5b65359c92a9794acf;
> hb=29d0566fd104ab8b9ffd0c460fc7c588a72a340b#l50
> 
> the proof needs updating to match

Can you explain the bug?  I see a link to line 50 of the main_stage.py file, but without more context, I don't know what I'm looking to fix in the proof.  Thanks.
Comment 12 Luke Kenneth Casson Leighton 2020-08-19 13:29:00 BST
(In reply to Samuel A. Falvo II from comment #11)

> Can you explain the bug?  I see a link to line 50 of the main_stage.py file,
> but without more context, I don't know what I'm looking to fix in the proof.
> Thanks.

ah sorry i should have recorded the diff-commit rather than a link to the line.
the "L" field was previously being completely ignored.

so where for example the pseudocode says this:

* cmp BF,L,RA,RB

    if L = 0 then
        a <-  EXTS((RA)[32:63] )
        b <- EXTS((RB)[32:63])
    else
        a <- (RA)
        b <- (RB)


we were in fact simply doing this:


* cmp BF,L,RA,RB

    a <- (RA)
    b <- (RB)


because this was in the proof *and* the HDL and there was no corresponding unit test to catch it, the bug went unnoticed for several months.