[libre-riscv-dev] formal proof NLnet proposal in
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Mon Sep 23 19:24:11 BST 2019
The two primary keywords in verilog (and yosys, and therefore in nmigen)
are "assert" and "assume".
In nmigen there is a nice set of wrapper operators one of which is called
You can Assert() that a condition involving a signal from the Past() holds
This is what the nmigen FIFO proof does, because it makes sure that the
data going IN to the FIFO equals the data coming OUT of the pipe, 2 cycles
later, on a 2 entry FIFO, by Asserting Past(Past(din))== dout
In some ways if you are used to python assert statements it is dead easy.
Hendrick the stuff you did, which you described several months back, is at
the level of z3 solver and yices.
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
More information about the libre-riscv-dev