[Next] [Up] [Previous]

Getting started with SMV

K. L. McMillan

• Introduction
• Modeling, specifying and verifying
  • Sequential circuits and temporal properties
  • A three-way arbiter
  • A traffic light controller
• Symbolic model checking
  • A buffer allocation controller
• Refinement verification
  • Layers
  • Refinement maps
    • A very simple example
    • End-to-end verification
    • Refinement maps as types
    • The effect of decomposition
  • Decomposing large data structures
  • Exploiting Symmetry
  • Decomposing large structures in the implementation
  • Case analysis
    • A very simple example
    • Using case analysis over data paths
  • Data type reductions
    • A very simple example
    • A slightly larger example
  • Proof by induction
    • Induction over infinite sequences
    • A simple example
    • A circular buffer
    • Abstract variables
  • Instruction processors
    • A very simple example
    • Uninterpreted functions
    • What about outputs?
  • An out-of-order instruction processor
    • Tomasulo's algorithm
    • The abstract model
    • Implementation
    • Refinement maps
    • Case splitting
    • The proof
    • Abstract counterexamples
    • Multiple execution units
    • Proving non-interference
• Synchronous Verilog
  • Basic concepts
    • Synchrony
    • Wires and registers
    • Wait statements
    • Loops
    • Conditionals
    • Resolution
    • Embedded assertions
  • Example - traffic light controller
  • Example - buffer allocation controller
• About this document ...