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: Describing Designs for Up: No Title Previous: Contents Introduction to VIS   This document introduces VIS (Verification Interacting with Synthesis). We describe what VIS is, what it can do, how to write limited Verilog code for its input, its commands, and an extended example for the new user. For more details, see the VIS home page http://embedded.eecs.berkeley.edu/ Respep/Research/vis/doc/packages/index.html. What is VIS ? VIS is a verification and synthesis system for finite-state hardware systems, which is being developed at Berkeley and Boulder. It improves upon first generation tools like HSIS and SMV by: providing a better programming environment, providing some new capabilities, and improving performance in some cases. VIS is divided into three parts: a common front end for reading in a description of a design, verification (VIS-v), and synthesis (VIS-s). History Many first generation tools for automatic formal verification were based on two theoretical approaches. The first is temporal logic model checking, where the properties to be checked are expressed as formulas in a temporal logic, and the system is expressed as a finite state system. In particular, Computational Tree Logic (CTL) model checking is a technique pioneered by Clarke and Emerson to verify whether a finite state system satisfies properties expressed as formulas in a branching-time temporal logic called CTL. SMV, a system developed at CMU, belongs to this class of tools. Certain properties are not expressible in CTL, but they can be expressed as -automata. The second approach, language containment, requires the description of the system and properties as -automata, and verifies correctness by checking that the language of the system is contained in the language of the property. Note that certain types of CTL properties involving existential quantification are not expressible by -automata. COSPAN, a system developed at Bell Labs, offers language containment. A combination of both approaches is offered by the HSIS [6] system, which was developed at the University of California, Berkeley. Our experience with verification tools (in particular HSIS) led to the conclusion that sometimes, the simpler and more limited the approach, the more efficient it can be. A number of design decisions that we made for HSIS made it unacceptably slow for some large examples. With these problems in mind, we set about writing a tool that was more efficient, easily extendible, and offered a good programming environment, in order that it can be more easily upgraded in the future as more efficient algorithms are developed. VIS also has the capability to interface with SIS to optimize logic modules; hence, VIS is an integrated system for hierarchical synthesis, as well as verification. We plan to pursue research on the interaction between verification and synthesis in the future; hence the name VIS, verification interacting with synthesis. Overview of VIS Fig. 1.1 presents of an overview of VIS.   Figure 1.1:   Block diagram of VIS. VIS has three main parts: a front-end to read and traverse a hierarchical system described in BLIF-MV, which may have been compiled from a high-level language like Verilog; a verification core, VIS-v, to perform model checking of Fair CTL and test language emptiness; and a path to SIS, VIS-s, to optimize parts of the logic. VIS-v Philosophy We decided to offer limited but efficient capabilities. We felt that in the future, it would be easy to add more features, as they are required, using a well defined programming interface. In line with this keep it simple philosophy, VIS provides the following verification capabilities. Only CTL formulas can be checked. Language containment may be handled in a later release. However, we do handle language emptiness checks. Fairness constraints must be of Büchi type, i.e., sets of states that must be visited infinitely often. However, the internal VIS data structures do have the capability to support more complicated fairness constraints. VIS-s Philosophy VIS can interact with SIS to assist the task of verification by simplifying parts of the system. Another objective is to support a full-fledged hierarchical synthesis flow, that translates a Verilog description into an optimized multi-level circuit at the gate level. Unlike existing logic optimization systems like SIS, VIS can support hierarchical synthesis. Next: Describing Designs for Up: No Title Previous: Contents Yuji Kukimoto Tue Feb 6 11:58:14 PST 1996

Contact

©2002-2018 U.C. Regents