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

[Yehowshua]

This error highlights the need for formal on the scoreboard.
https://bugs.libre-soc.org/show_bug.cgi?id=336#c54

Symbiotic EDA has a wonderful tutorial on how to specify 
hazard dependencies as formal constraints.
https://www.youtube.com/watch?v=tgTt-8UqSMU

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.

Cheers,
	Yehowshua