Bug 197

Summary: Formal correctness proof needed of the 6600-style Out-of-Order execution engine
Product: Libre-SOC's first SoC Reporter: Luke Kenneth Casson Leighton <lkcl>
Component: Formal VerificationAssignee: Luke Kenneth Casson Leighton <lkcl>
Status: RESOLVED FIXED    
Severity: enhancement CC: libre-soc-bugs
Priority: High    
Version: unspecified   
Hardware: PC   
OS: Linux   
See Also: https://bugs.libre-soc.org/show_bug.cgi?id=81
NLnet milestone: NLNet.2019.10.032.Formal total budget (EUR) for completion of task and all subtasks: 5000
budget (EUR) for this task, excluding subtasks' budget: 0 parent task for budget allocation: 158
child tasks for budget allocation: 342 879 The table of payments (in EUR) for this task; TOML format:
Bug Depends on: 879    
Bug Blocks: 158    

Description Luke Kenneth Casson Leighton 2020-03-02 13:19:55 GMT 
A formal proof is needed which demonstrates the effectiveness and
correctness of the out-of-order execution engine: register dependencies,
memory dependencies, and the use of a "revolving door" set of SR Latches.
This is tricky because SR NOR Latches are not normally used in "industry"
designs.  Consequently we need to formally prove that the HDL functions
correctly.
https://git.libre-riscv.org/?p=soc.git;a=summary