[libre-riscv-dev] Using formal to expose bugs in scoreboard
yimmanuel3 at gatech.edu
Mon Jun 8 04:11:36 BST 2020
This error highlights the need for formal on the scoreboard.
Symbiotic EDA has a wonderful tutorial on how to specify
hazard dependencies as formal constraints.
I imagine it shouldn’t be too hard to turn that tutorial into
something that can fit the scoreboard.
You would keep repairing until the asserts pass basically.
More information about the libre-riscv-dev