[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 #8 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
hmmm, actually... by writing both, it may be possible to write a formal proof
that shows equivalence between the two.

something like:

p1.i.eq(p2.i)
Assert(p2.o == p1.o)

where p2.i is the input to the module.

basically the solver would know, because p2.i is the input, to generate a test
of all possible values for p2.i and confirm that the outputs for both p2 and p1
are identical *for* all those inputs.

exactly how the SAT solvers do that is beyond my knowledge, i haven't
investigated: i am treating them as a "black box" at the moment.

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