[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 #5 from yuda at berkeley.edu ---
(In reply to Luke Kenneth Casson Leighton from comment #4)
> 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.

I see what you meant, verification is also an uncomfortable process for me.

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