Bug 250 - Wishbone B4 Streaming Formal correctness proof needed
Summary: Wishbone B4 Streaming Formal correctness proof needed
Status: CONFIRMED
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
URL:
Depends on:
Blocks: 175
  Show dependency tree / graph
 
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:

Attachments
Add an attachment (proposed patch, testcase, etc.)

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.