Bug 63 - queue (FIFO) library routine needed
Summary: queue (FIFO) library routine needed
Status: PAYMENTPENDING FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Source Code (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on:
Blocks: 62
  Show dependency treegraph
 
Reported: 2019-04-19 08:56 BST by Luke Kenneth Casson Leighton
Modified: 2020-09-21 16:37 BST (History)
2 users (show)

See Also:
NLnet milestone: NLnet.2019.02
total budget (EUR) for completion of task and all subtasks: 800
budget (EUR) for this task, excluding subtasks' budget: 800
parent task for budget allocation: 62
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2019-04-19 08:56:15 BST
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
Comment 1 yuda 2019-09-10 02:58:54 BST
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
Comment 2 Luke Kenneth Casson Leighton 2019-09-10 03:20:53 BST
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.
Comment 3 yuda 2019-09-10 03:30:42 BST
(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
Comment 4 Luke Kenneth Casson Leighton 2019-09-10 03:45:39 BST
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.
Comment 5 yuda 2019-09-10 04:02:21 BST
(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.
Comment 6 Luke Kenneth Casson Leighton 2019-11-19 14:38:23 GMT
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