Skip to content

Instantly share code, notes, and snippets.

@georgerennie

georgerennie/model_checkers.md

Created January 20, 2024 17:06
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save georgerennie/0aed5dd3e42add972471f692ed746d60 to your computer and use it in GitHub Desktop.
Save georgerennie/0aed5dd3e42add972471f692ed746d60 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
model_checkers.md

General architecture for a hardware model checking tool

Key Principles

  • Things should feel real time
    • Solvers should be able to communicate between threads rapidly for clause sharing, solver shutdown etc
    • Main thread should be only used for comms between/launching threads, UI/user scripts should run in their own thread so you don't get the case where e.g. you can't load a CEX while a script is running
  • Users should have the power to control proof performance in sound and intuitive ways
    • Tooling to safely do case splits, assume-guarantee etc.
    • Prefer hints for abstractions/invariants so that the engines can use CEGAR etc. techniques to patch them if they are incorrect in some cases, but report to the user if this is the case
    • Scripting should be easy, intuitive and flexible - Python
  • There should be strong defaults
    • Default engines, abstractions etc. should work out of the box and give reasonable results
  • Techniques should compose
    • Model checking engines should be oblivious to underlying proof procedure/netlist (whether it is SAT, SMT, gate-level, word-level, has additional abstraction/restriction etc)
    • Abstraction/restriction engines should be sound (CEGAR/PROGRESS) and be able to be combined in (relatively) arbitrary fashion
  • Composition of techniques should be managed by the environment
    • This can be done in a why3 way with a tree of proof obligations
    • A node can rely on either the conjunction (e.g. case splitting) or disjunction (e.g. a set of engines racing to prove the property) of its children
    • Proof checkers can appear as obligations in this
    • Things like case splitting therefore become modifications to the tree
  • Verification should be able to compose both functionally (abstractions, case splitting etc) and structurally (assume guarantee)
    • This should apply also to scripts - scripts for individual blocks should compose up to top level
  • Engines should be able to bubble up correct and useful information
    • Proof bounds
    • Invariants
    • Useful Abstractions?
    • CEXs
    • Coverage information
    • Witness circuits

Algorithms

Model checking

Abstraction/Reduction

Invariant hunting

Pre-processing

Decision Procedure

Equivalence checking

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment