Bug 197 - Formal correctness proof needed of the 6600-style Out-of-Order execution engine
Summary: Formal correctness proof needed of the 6600-style Out-of-Order execution engine
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: High enhancement
Assignee: Luke Kenneth Casson Leighton
URL:
Depends on: 879
Blocks: 158
  Show dependency tree / graph
 
Reported: 2020-03-02 13:19 GMT by Luke Kenneth Casson Leighton
Modified: 2023-09-05 20:10 BST (History)
1 user (show)

See Also:
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:

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-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