[libre-riscv-dev] [Bug 63] queue (FIFO) library routine needed

bugzilla-daemon at libre-riscv.org bugzilla-daemon at libre-riscv.org
Tue Sep 10 03:45:39 BST 2019


--- Comment #4 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---

Here it is, the use of "Assert" and so on. Nmigen, like chisel3, is an AST that
generates RTL, in this case yosys intermediary language.

Past is just a wrapper that creates AST representing the formal test that
something was true in the previous clock cycle.

This can be used twice in succession and by placing data into a queue of length
2, if it takes 2 cycles to appear on the output then the assertion passes and
the proof holds.

The FIFO Code in nmigen was so difficult to unit test through "normal" unit
tests that the developers only felt comfortable using formal proofs.

I talked about how chisel3 could have AST classes added which output
SystemVerilog "assert" statements on sw-dev a couple weeks back. It really
should not be difficult however would need to go via FIRRTL.

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

More information about the libre-riscv-dev mailing list