Needed: - OP_MCRF - DONE - OP_CROP - this is crand, cror, crxor, etc. - DONE - OP_MTCRF - DONE - OP_MFCR - DONE - OP_ISEL - review needed
* 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
* 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
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
(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.
(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().
(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.
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.