[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 #2 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
example code which is extremely good and has comprehensively well-written
formal mathematical proofs:
http://chiselapp.com/user/kc5tja/repository/kestrel-3/dir?ci=f84f6c3126376ab2&name=cores/cpu

here is a sophisticated one involving "things that occur in the past":
http://chiselapp.com/user/kc5tja/repository/kestrel-3/artifact/217f2862441726f5

see UpCounterCSRFormal. this one uses "Past" to check (assert) that data
which comes "into" the hardware comes *out* of the hardware at the required
number of "ticks" (clock cycles) in the future.  actually, by comparing
"right now" to "Past()".

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