Workspaces ---- apbd asves asvpapers bear blast caltrop cases concurrency cosi dif diva dopcenter dopresence dopsysadmin eecsx44 elab embedded embeddedadmin giotto hyinfo m2t2 mescal metropolis mica mobies msgadmin murieh mvsis nephest ransom recons robosysadmin savg sec seminar smartnets video webmaster

Next: Introduction to VIS Up: No Title Previous: No Title 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 ... Yuji Kukimoto Tue Feb 6 11:58:14 PST 1996