[libre-riscv-dev] [Bug 151] introductory formal verification tutorial using the PriorityPicker

[bugzilla-daemon at libre-riscv.org]

http://bugs.libre-riscv.org/show_bug.cgi?id=151

--- Comment #4 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Jacob Lifshay from comment #3)

> Related: priority picker where LSB has highest priority can be implemented
> with:
> 
> i = Signal(32)
> o = Signal(32)
> 
> m.d.comb += o.eq(i & -i)

nice!  that... hmmm, i wonder if that property can be exploited mathematically
for the formal proof?

hardware-wise it would be nooowhere near as efficient as what Seymour Cray came
up with (a O(N) cascade of NAND and NOT gates) so it's not something we want to
deploy in production.  the proofs don't get put into actual silicon, though.

here's the installation process:
https://symbiyosys.readthedocs.io/en/latest/

you'll each need to go through that, and also install nmigen.  i *strongly*
recommend using debian - or last resort ubuntu.  if you try windows or macosx,
you will get into a world of pain.

the critical solvers to have are yices3 and z3.  if you really really want to
you could add super_prove, amy and boolector.

the tutorial there ("a simple BMC example") is a good idea to try out as a
by-rote test of symbiyosis.

once you've each confirmed that working we can move to nmigen.

-- 
You are receiving this mail because:
You are on the CC list for the bug.