Bug 332 - Formal correctness proof needed for CR pipeline
Summary: Formal correctness proof needed for CR pipeline
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Windows
: --- enhancement
Assignee: Michael Nolan
URL:
Depends on:
Blocks: 195 314
  Show dependency treegraph
 
Reported: 2020-05-20 17:34 BST by Michael Nolan
Modified: 2021-04-20 14:37 BST (History)
2 users (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 300
budget (EUR) for this task, excluding subtasks' budget: 300
parent task for budget allocation: 195
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
"donated"={amount=300, paid=2020-12-06}


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Michael Nolan 2020-05-20 17:34:09 BST

    
Comment 1 Michael Nolan 2020-05-20 17:34:59 BST
Needed: 
 - OP_MCRF                                    - DONE
 - OP_CROP - this is crand, cror, crxor, etc. - DONE
 - OP_MTCRF                                   - DONE
 - OP_MFCR                                    - DONE
 - OP_ISEL                                    - review needed
Comment 4 Luke Kenneth Casson Leighton 2020-05-23 11:59:17 BST
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
Comment 5 Michael Nolan 2020-05-23 14:28:54 BST
(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.
Comment 6 Luke Kenneth Casson Leighton 2020-05-23 14:40:18 BST
(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().
Comment 7 Luke Kenneth Casson Leighton 2020-05-23 19:43:28 BST
(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.
Comment 8 Luke Kenneth Casson Leighton 2020-05-27 15:09:09 BST
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.