[libre-riscv-dev] formal proof NLnet proposal in

[Luke Kenneth Casson Leighton]

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
"Past".

You can Assert() that a condition involving a signal from the Past() holds
true.

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.

L.




-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68