Bug 250 - Wishbone B4 Streaming Formal correctness proof needed
Summary: Wishbone B4 Streaming Formal correctness proof needed
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
Depends on:
Blocks: 175
  Show dependency treegraph
Reported: 2020-03-13 15:20 GMT by Luke Kenneth Casson Leighton
Modified: 2020-09-21 03:39 BST (History)
1 user (show)

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


Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-03-13 15:20:36 GMT
Design unit tests as formal proofs in nmigen which can test both nmigen and (System-)Verilog Wishbone B4 Streaming Bus Function Models.  Example peripheral (I2S Audio Streaming) to also be tested.