[libre-riscv-dev] [Bug 306] New: Formal Correctness Proof for ALU pipeline

[libre-riscv-dev] [Bug 306] New: Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

            Bug ID: 306
           Summary: Formal Correctness Proof for ALU pipeline
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Mac OS
            Status: CONFIRMED
          Severity: enhancement
          Priority: ---
         Component: Formal Verification
          Assignee: lkcl@lkcl.net
          Reporter: lkcl@lkcl.net
                CC: libre-riscv-dev@lists.libre-riscv.org
   NLnet milestone: ---

https://git.libre-soc.org/?p=soc.git;a=tree;f=src/soc/alu/formal;hb=HEAD

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
    NLnet milestone|---                         |NLNet.2019.10.Formal

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
           Assignee|lkcl@lkcl.net               |mtnolan2640@gmail.com

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
    parent task for|                            |198
  budget allocation|                            |
 total budget (EUR)|0                           |400
  for completion of|                            |
       task and all|                            |
           subtasks|                            |

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

--- Comment #1 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
python3 alu/formal/proof_main_stage.py ..
----------------------------------------------------------------------
Ran 2 tests in 312.563s

wooow :)

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

--- Comment #2 from Michael Nolan <mtnolan2640@gmail.com> ---
(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

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

--- Comment #3 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
* OP_EXTS proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=32d9da2bd849d3ae9b59bdec7a4add0c35908922

* OP_CMP and OP_CMPEQB proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=ca79ab18a7fa9bdabeca860448d79b5d11dc222f

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
           See Also|                            |https://bugs.libre-soc.org/
                   |                            |show_bug.cgi?id=331

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
    parent task for|198                         |195
  budget allocation|                            |

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

--- Comment #4 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

--- Comment #5 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
  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)?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

--- Comment #6 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline

[bugzilla-daemon]

https://bugs.libre-soc.org/show_bug.cgi?id=306

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev