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

[bugzilla-daemon at libre-riscv.org]

http://bugs.libre-riscv.org/show_bug.cgi?id=63

--- Comment #4 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
https://github.com/m-labs/nmigen/blob/master/nmigen/test/test_lib_fifo.py#L147

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.