Contents

• Introduction to VIS
  • What is VIS ?
  • History
  • Overview of VIS
    • VIS-v Philosophy
    • VIS-s Philosophy
• Describing Designs for VIS
  • Verilog HDL
  • VL2MV: from Verilog to BLIF-MV
  • Features of Verilog Supported by VL2MV
    • Assignments
    • Nondeterminism
    • Symbolic Variables
  • Implicit vs. Explicit Clocking
  • Verilog for VL2MV: Hints and Traps
  • BLIF-MV
  • BLIF
  • Nondeterminism and Incomplete Specification
  • Example: a Traffic Light Controller
• Introduction to Formal Verification
  • Model Checking of Temporal Logic
    • Computation Tree Logic
    • Specification of Properties in CTL
    • Fairness Constraints
  • Properties and Fairness Conditions of Traffic Light Controller in CTL
  • Language Containment
• Formal Verification in VIS
  • Representing the System for Verification
    • Building the Flattened Network
    • Ordering
    • Computing FSM Information
    • Advanced Ordering
  • FSM Traversal and Image Computation
  • Specifying Fairness Constraints
  • Language Emptiness
  • Model Checking Operations
    • Performing Model Checking
    • Debugging for Model Checking
    • Checking Invariants
    • Advanced Model Checking: Abstraction and Reduction
  • Combinational and Sequential Equivalence
  • Simulation
• Synthesis in VIS
  • Writing and Reading from SIS
  • Flow of Operations for Synthesis
  • Example of Synthesis of Traffic Light Controller
• Commands in VIS
• List of Commands in VIS
• References
• About this document ...