[libre-riscv-dev] [Bug 197] New: Formal correctness proof needed of the 6600-style Out-of-Order execution engine

[bugzilla-daemon at libre-riscv.org]

http://bugs.libre-riscv.org/show_bug.cgi?id=197

            Bug ID: 197
           Summary: Formal correctness proof needed of the 6600-style
                    Out-of-Order execution engine
           Product: Libre Shakti M-Class
           Version: unspecified
          Hardware: PC
                OS: Linux
            Status: CONFIRMED
          Severity: enhancement
          Priority: ---
         Component: Formal Verification
          Assignee: lkcl at lkcl.net
          Reporter: lkcl at lkcl.net
                CC: libre-riscv-dev at lists.libre-riscv.org
   NLnet milestone: ---

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

-- 
You are receiving this mail because:
You are on the CC list for the bug.