Contents

• 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
  • Decomposing large data structures
  • Exploiting Symmetry
  • Decomposing large structures in the implementation
  • Case analysis
  • Data type reductions
  • Proof by induction
  • Instruction processors
  • An out-of-order instruction processor
  • Bit vectors as scalarsets
  • Propagation of unknown values
  • Conditional proof statements, and course-of-values induction
  
  
• Synchronous Verilog
  • Basic concepts
  • Example - traffic light controller
  • Example - buffer allocation controller
  • Synthesizable Verilog and SMV
  • Symmetry and Synchronous Verilog
  
  
• Handling very large input files
• About this document ...