| |
|
|
   Next: Algorithms Up: VIS : A System Previous: Introduction
Capabilities of VISWe briefly describe the salient features of VIS. VIS has both an interactive command interface and a batch mode. For a detailed description of the full functionality of VIS, with examples of usage, refer to the VIS Manual [2].
Verilog front endVIS operates on an intermediate format called BLIF-MV, which is an extension of BLIF, the intermediate format for logic synthesis accepted by SIS [7]. VIS includes a stand-alone compiler from Verilog to BLIF-MV, called VL2MV, which supports a synthesizable subset of Verilog. VL2MV extracts a set of interacting finite state machines that preserves the behavior of the source Verilog program defined in terms of simulated results. Two new features have been added to Verilog:
Hierarchy and initializationWhen a BLIF-MV description is read into VIS, it is stored hierarchically as a tree of modules, which in turn consist of sub-modules. This hierarchy can be traversed in a manner similar to traversing directories in UNIX. Simulation and verification operations can be performed at any subtree of the hierarchy. It is possible to replace the subhierarchy rooted at the current node with a new hierarchy specified by a new BLIF-MV file, which might be a synthesized module or a manually abstracted module. VIS can also output the hierarchy below the current node to a BLIF-MV file.
Interaction with synthesisVIS can interact with SIS to optimize the existing logic by reading and writing the BLIF format, which SIS recognizes. Synthesis can be performed on any node of the hierarchy.
AbstractionManual abstraction can be performed by giving a file containing the names of variables to abstract. For each variable appearing in the file, a new primary input node is created to drive all the nodes that were previously driven by the variable. Abstracting a net effectively allows it to take any value in its range, at every clock cycle.
Fair CTL model checking and language emptiness check
VIS performs fair CTL model checking under Büchi fairness
constraints. In addition, VIS can perform language emptiness checking
by model checking the formula
Equivalence checkingVIS provides the capability to check the combinational equivalence of two designs. An important usage of combinational equivalence is to provide a sanity check when re-synthesizing portions of a network. VIS also provides the capability to test the sequential equivalence of two designs. Sequential verification is done by building the product finite state machine, and checking whether a state where the values of two corresponding outputs differ, can be reached from the set of initial states of the product machine. If this happens, a debug trace is provided. Both combinational and sequential verification are implemented using BDD-based routines.
SimulationVIS also provides traditional design verification in the form of a cycle-based simulator that uses BDD techniques. Since VIS performs both formal verification and simulation using the same data structures, consistency between them is ensured. VIS can generate random input patterns or accept user-specified input patterns. Any subtree of the specified hierarchy may be simulated.
Next: Algorithms Up: VIS : A System Previous: Introduction
Tom Shiple Thu Feb 8 16:55:08 PST 1996 |
| Contact |
| ©2002-2018 U.C. Regents |
. The language of a design
is given by sequences over the set of reachable states that do not
violate the fairness constraint. The language emptiness check can be
used to perform language containment by expressing the set of bad
behaviors as another component of the system. If model checking or
language emptiness fail, VIS reports the failure with a
counterexample, (i.e., behavior seen in the system that does not
satisfy the property - for model checking, or valid behavior seen in
the system - for language emptiness). This is called the ``debug''
trace. Debug traces list a set of states that are on a path to a fair
cycle and fail the CTL formula.