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

[bugzilla-daemon@libre-soc.org]

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