[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 mailing list