[libre-riscv-dev] Using formal to expose bugs in scoreboard

Yehowshua 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 mailing list