[libre-riscv-dev] [Bug 332] New: Formal correctness proof needed for CR pipeline

[libre-riscv-dev] [Bug 332] New: Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

            Bug ID: 332
           Summary: Formal correctness proof needed for CR pipeline
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Windows
            Status: CONFIRMED
          Severity: enhancement
          Priority: ---
         Component: Formal Verification
          Assignee: lkcl@lkcl.net
          Reporter: mtnolan2640@gmail.com
                CC: libre-riscv-dev@lists.libre-riscv.org
   NLnet milestone: ---

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

--- Comment #1 from Michael Nolan <mtnolan2640@gmail.com> ---
Needed: 
 - OP_MCRF
 - OP_CROP - this is crand, cror, crxor, etc.
 - OP_MTCRF
 - OP_MFCR

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

Michael Nolan <mtnolan2640@gmail.com> 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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

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

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |lkcl@lkcl.net

--- Comment #2 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
* OP_CROP proof -
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=16ac8bcd32bd2998d58488ca236f8ff721eccaf6
* OP_MTCRF proof -
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=7d16e4157873bb5ad17c0bb9a0d646b15b0e2b1b

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

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

           What    |Removed                     |Added
----------------------------------------------------------------------------
    parent task for|                            |198
  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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

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

           What    |Removed                     |Added
----------------------------------------------------------------------------
 total budget (EUR)|0                           |200
  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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

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

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

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

--- Comment #3 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
* MCRF proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=b9a3b94d0ed88221b1ca19027bf8f23b806c8e8b
* MFCR proof
https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=78e6e9f800a3dbfad854bf5a4afaf48307275960

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

--- Comment #4 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
michael could you check this when you have a moment?

commit 27440addbb83c3c13949246b495b8c474b1c2c90 (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Sat May 23 11:58:43 2020 +0100

    add CR_ISEL formal proof to CR pipeline

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

--- Comment #5 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #4)
> michael could you check this when you have a moment?
> 
> commit 27440addbb83c3c13949246b495b8c474b1c2c90 (HEAD -> master,
> origin/master)
> Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
> Date:   Sat May 23 11:58:43 2020 +0100
> 
>     add CR_ISEL formal proof to CR pipeline

I changed it so the proof of isel uses the full CR register. Part of the reason
that proof is written the way it is, is I'd already proven that the CR
operations worked when we were using the old interface where it would always
take in the full CR. I wanted to prove that the new way was exactly equivalent
to the old way, so I kept the old proof machinery that used the full CR
register, and added on a way to translate the new interface to that. I think
it's useful to keep doing it that way, so I modified your isel proof to do the
same thing.

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

--- Comment #6 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Michael Nolan from comment #5)
> (In reply to Luke Kenneth Casson Leighton from comment #4)
> > michael could you check this when you have a moment?
> > 
> > commit 27440addbb83c3c13949246b495b8c474b1c2c90 (HEAD -> master,
> > origin/master)
> > Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
> > Date:   Sat May 23 11:58:43 2020 +0100
> > 
> >     add CR_ISEL formal proof to CR pipeline
> 
> I changed it so the proof of isel uses the full CR register.

ok, cool.  we do now have two CR_ISEL case statements, and now two test_isel().

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #6)

> ok, cool.  we do now have two CR_ISEL case statements,

ok i see, the first one is for setup, the second for actual isel "proof".

i will delete one of the test_isel()s.

-- 
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 332] Formal correctness proof needed for CR pipeline

[bugzilla-daemon]

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

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

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

--- Comment #8 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
spotted that the CR proof needs to check Data.ok, currently doing that now.

the reason we "get away" with things working right now is because assigning
a Signal to a Record is done in a bit-wise fashion.  the extra bit (Data.ok)
is therefore totally ignored, not just when assigned, but also in the formal
proofs.

-- 
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