[libre-riscv-dev] Paper: Scoreboards can deadlock

Luke Kenneth Casson Leighton lkcl at lkcl.net
Sat Jun 8 22:42:19 BST 2019


On Sat, Jun 8, 2019 at 5:52 PM Samuel Falvo II <sam.falvo at gmail.com> wrote:

> Still, I thought there might be some nugget of useful information in
> it especially with respect to their use of formal verification.  That
> part I haven't studied yet.

 the formal verification is just that the authors found a single
example that failed.  whether they used formal verification to find
it, well, they didn't actually publish the source code of their
techniques, so big deal.

 and, if they formally verified a flawed design because they didn't
study and implement it properly, that means the paper is useless on
two counts.

l.



More information about the libre-riscv-dev mailing list