queue needed with the following features: * between 1 and N entries * first-word write-through capability * "pipeline" mode which guarantees data delivery once available note: SyncFIFO in nmigen uses Memory which cannot accept only 1 entry note: SyncFIFO fwft mode *FAILS* on FPGAs, making it necessary to have SyncFIFOBuffered on FPGAs, and SyncFIFO on ASICs. this makes it impossible to go from a tested FPGA design straight to an ASIC layout. current code (adapted to conform to nmigen FIFOInterface API) here: https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/add/queue.py;h=e52ab5e9eb74cbd516b5b0daa8681023714055b3;hb=25a0ec563bd7837b43a1d04036b2a5945c97023b
Dear Luke, I finished writing a FIFO generator in chisel3. https://github.com/redpanda3/soDLA/blob/test/src/main/scala/slibs/FIFO.scala Haven't been tested yet. Can you have a try and make some comments? Best, redpanda
http://bitsbytesgates.blogspot.com/2017/08/chisel-sharpening-verification.html?m=1 Hi, Ok so the truth is, I find writing code from scratch so extraordinarily difficult that it is not just a "good idea" to have unit tests, I simply cannot write code e without them. This is why we copied queue.py and language translated it, because its usage in ASICs means that even without unit tests it has been at least deployed. The "graphs" that are mentioned as a requested feature are achievable very simply with yosys "show modulename" after conversion to verilog and read_verilog command. They are extraordinarily useful and help avoiding making obvious costly but "logically high level language correct" design oddities. Beyond that, honestly and plainly, for goodness sake write full coverage unit tests. The best ones are formal tests and nmigen has some for SyncFIFO.
(In reply to Luke Kenneth Casson Leighton from comment #2) > http://bitsbytesgates.blogspot.com/2017/08/chisel-sharpening-verification. > html?m=1 > > Hi, > > Ok so the truth is, I find writing code from scratch so extraordinarily > difficult that it is not just a "good idea" to have unit tests, I simply > cannot write code e > without them. > > This is why we copied queue.py and language translated it, because its usage > in ASICs means that even without unit tests it has been at least deployed. > > The "graphs" that are mentioned as a requested feature are achievable very > simply with yosys "show modulename" after conversion to verilog and > read_verilog command. > > They are extraordinarily useful and help avoiding making obvious costly but > "logically high level language correct" design oddities. > > Beyond that, honestly and plainly, for goodness sake write full coverage > unit tests. The best ones are formal tests and nmigen has some for SyncFIFO. OK, I see. I will let you know when it is been tested. Best, Yuda
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.
(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.
happy with the queue.py code, there are unit tests at the pipeline API level that pass. formal proof testing is to be added from another NLNet proposal