[libre-riscv-dev] [Bug 198] New: Formal correctness proofs are needed for low-level libraries in LibreSOC

[bugzilla-daemon at libre-riscv.org]

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

            Bug ID: 198
           Summary: Formal correctness proofs are needed for low-level
                    libraries in LibreSOC
           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: ---

Formal proofs turn out to provide 100% code-coverage if written correctly,
whereas standard testbench units tests typically do not, even when dozens,
hundreds or tens of thousands are provided.  Therefore, to greatly simplify
the development and also increase effectiveness of unit tests, formal
proofs are to be written on the low-level HDL libraries used in Libre-SOC.
this includes nmutil and the SoC code itself.  This is *different* from
the *high-level* formal correctness proofs (bug #194 and bug #195)
https://git.libre-riscv.org/?p=nmutil.git;a=summary
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.