[libre-riscv-dev] daily kan-ban update 22may2020

[Luke Kenneth Casson Leighton]

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.

excellent.