[libre-riscv-dev] daily kan-ban update 22may2020
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Fri May 22 16:39:02 BST 2020
On Fri, May 22, 2020 at 4:20 PM Michael Nolan <mtnolan2640 at gmail.com> wrote:
> Today I reworked the formal proof for the CR FU by adding a translation
> layer so I could use most of the existing proof on the new interface.
retrospectively this may have been the best way to do it, due to the
awkwardness of indexing dynamic bit-masked groups.
> I also ported the branch FU to use the new CR interface.
confirmed the unit tests run.
> This afternoon I
> will probably work on writing a proof for the branch unit, and work some
> on the bperm module with Cole.
More information about the libre-riscv-dev