[libre-riscv-dev] [Bug 151] introductory formal verification tutorial using the PriorityPicker
bugzilla-daemon at libre-riscv.org
bugzilla-daemon at libre-riscv.org
Wed Jan 8 04:06:08 GMT 2020
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.
More information about the libre-riscv-dev
mailing list