[Libre-soc-bugs] [Bug 590] New: Formally verify experiments/icache.py

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=590

            Bug ID: 590
           Summary: Formally verify experiments/icache.py
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Linux
            Status: CONFIRMED
          Severity: normal
          Priority: Normal
         Component: Source Code
          Assignee: colepoirier at gmail.com
          Reporter: colepoirier at gmail.com
                CC: cestrauss at gmail.com,
                    libre-soc-bugs at lists.libre-soc.org, lkcl at lkcl.net
            Blocks: 485
             Group: editcomments
          Deadline: 2021-02-28
   NLnet milestone: NLNet.2019.10.Formal

Hi Luke and Cesar,

I have the (perhaps overly ambitions) intention of formally verifying the
icache.py module by the end of the month. I'm slightly at a loss as to how to
begin the process given how large and complex this module is; I am not sure if
the module should have a proof for each sub-function which then get collected
into a proof of the whole module?

Any help you can provide me in getting started, and almost definitely along the
way as well is immensely appreciated!

Presently, I'm taking inspiration from Cesar's excellent
fu/compunits/formal/proof_fu.py, with detailed comments for each of the N
properties that must hold for the formal verification to pass.


Referenced Bugs:

https://bugs.libre-soc.org/show_bug.cgi?id=485
[Bug 485] Create I-Cache from microwatt icache.vhdl
-- 
You are receiving this mail because:
You are on the CC list for the bug.