Bug 250

Summary: Wishbone B4 Streaming Formal correctness proof needed
Product: Libre-SOC's first SoC Reporter: Luke Kenneth Casson Leighton <lkcl>
Component: Formal VerificationAssignee: Luke Kenneth Casson Leighton <lkcl>
Status: CONFIRMED ---    
Severity: enhancement CC: libre-soc-bugs
Priority: ---    
Version: unspecified   
Hardware: PC   
OS: Linux   
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:
Bug Depends on:    
Bug Blocks: 175    

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.