[libre-riscv-dev] [Bug 211] formal proof of PowerDecoder stage2 needed

bugzilla-daemon at libre-riscv.org bugzilla-daemon at libre-riscv.org
Mon Mar 9 14:03:03 GMT 2020


Michael Nolan <mtnolan2640 at gmail.com> changed:

           What    |Removed                     |Added
                 CC|                            |mtnolan2640 at gmail.com

--- Comment #1 from Michael Nolan <mtnolan2640 at gmail.com> ---
I'm somewhat hesitant to try and prove the stage-1 decoder, since the proof
would essentially be making a duplicate of the decoder separately, and checking
that the two are equivalent. I'm not entirely sure how useful that would be.

A formal proof for stage-2 on the other hand seems much more straightforward,
and would be more useful.

You are receiving this mail because:
You are on the CC list for the bug.

More information about the libre-riscv-dev mailing list