Formal Verification in VIS
 

 


next up previous contents
Next: Synthesis in VIS Up: No Title Previous: Introduction to Formal

Formal Verification in VIS

 

In this chapter we describe the usage and the relation between the VIS commands that perform formal verification. The main sections are:

  1. building an internal representation of the finite-state system,
  2. FSM traversal,
  3. specification of fairness constraints,
  4. language emptiness,
  5. model checking,
  6. equivalence checking, and
  7. simulation.

Representing the System for Verification

In this section, we describe the steps involved in converting a BLIF-MV description into an internal FSM representation.

Building the Flattened Network

The compound init_verify command executes the entire set of required initialization commands. When a BLIF-MV description is read into VIS, it is stored as a ``hierarchy'' tree, which is a hierarchical description of the design; it consists of modules (also called hnodes) that in turn consist of sub-modules (also hnodes) that are related in some fashion. This relation is represented as a table, which implements the output function in terms of the sub-module inputs. The print_hierarchy_stats command in VIS prints hierarchy information, and the print_models command lists statistics on all the models in the hierarchy. Other useful print commands are print_io and print_latches.

The hierarchy can be described by a tree. The root of the tree is the main module, and the leaves are lower level instantiations of modules. The hierarchy in VIS can be traversed in a manner similar to traversing directories in UNIX. It is possible to reach a desired node in the tree by walking up and down with the cd command. At any node simulation, verification and synthesis operations can be performed. The command pwd prints the name of the current node. The command ls lists all the nodes (submodules) in the current node; ls -R lists all the nodes in the current subtree.

The first step towards verification consists of ``flattening'' this hierarchical description into a single network (netlist of multi-valued logic gates). The output is computed from the inputs of the design by the network circuit, which consists of logic gates, interconnections between them, and latches to represent the sequential elements. The flatten_hierarchy command creates this network, and the print_network command can be used to print it. Other related commands are print_network_stats command that prints statistics about the network, and test_network_acyclic command that checks the network for combinational cycles. On the Traffic Light Controller example these commands work as follows : 

 
UC Berkeley, VIS Release 1.0 (compiled 11-Dec-95 at 10:36 AM)
VIS> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> print_hierarchy_stats
Model name = main, Instance name = main
inputs = 0, outputs = 0, variables = 12, tables = 3, latches = 0, children = 4
vis> print_models
Model name = hwy_control
inputs = 4, outputs = 3, variables = 49, tables = 44, latches = 1
subckts = 0
Model name = sensor
inputs = 0, outputs = 1, variables = 12, tables = 11, latches = 1
subckts = 0
Model name = main
inputs = 0, outputs = 0, variables = 12, tables = 3, latches = 0
subckts = 4
Model name = timer
inputs = 1, outputs = 2, variables = 40, tables = 38, latches = 1
subckts = 0
Model name = farm_control
inputs = 4, outputs = 3, variables = 49, tables = 44, latches = 1
subckts = 0
vis> flatten_hierarchy
vis> print_network_stats 
main  combinational=142  pi=0  po=0  latches=4  pseudo=2  const=40  edges=206
vis> test_network_acyclic
Network has no combinational cycles
vis> ls
farm_control
hwy_control
sensor
timer
vis> cd hwy_control
vis> print_io 
inputs: car_present enable_hwy long_timer short_timer
outputs: enable_farm hwy_light hwy_start_timer
vis> print_latches
hwy_light 
vis> flatten_hierarchy
vis> print_network_stats
hwy_control  combinational=45  pi=4  po=3  latches=1  pseudo=0  const=12  edges=68

Note that when a node is arrived at for the first time, there is no network for that node until flatten_hierarchy is called for that node.

Also flatten_hierarchy automatically checks each table in the network for being deterministic (except for pseudo-inputs) and completely specified. Since this checking takes some time, it can be turned off safely using the option flatten_hierarchy -b, after a BLIF-MV file has been checked once.

Ordering

The next step towards verification consists of converting this network representation into a functional description that represents the output and next state variables as a function of the inputs and current state variables. We use the BDD (binary decision diagram) and its extension the MDD (multivalued decision diagram) to represent boolean and discrete functions. Before creating the MDDs, it is necessary to order the variables in the support of the MDD. This is accomplished by the static_order command, which gives an initial ordering. Networks with combinational cycles cannot be ordered. If the MDD variables have already been ordered, then static_order does nothing. To undo the current ordering, reinvoke the command flatten_hierarchy. At any stage the current variable ordering can be written out to a file using the write_order command.

Computing FSM Information

The build_partition_mdds command computes the transition function MDDs. Depending on the partitioning method selected, the MDDs for the combinational outputs (COs) are built in terms of either the combinational inputs (CIs) or some subset of intermediate nodes of the network. The MDDs built are stored in a DAG called a ``partition''. The vertices of a partition correspond to the CIs, COs, and any intermediate nodes used. Each vertex has a multi-valued function (represented by an MDD) expressing the function of the corresponding network node in terms of the partition vertices in its transitive fanin. Hence, the MDDs of the partition represent a partial collapsing of the network. The inout method represents one extreme where no intermediate nodes are used, and total represents the other extreme where every node in the network has a corresponding vertex in the partition. If no method is specified on the command line, then the value of the flag partition_method is used as default (this flag is set by the command set partition_method), unless it does not have a value, in which case the inout method is used. The partition graph can be printed to a file with the print_partition command. Another related command is the print_partition_stats command that prints statistics on the partition graph.

The complete set of commands included by init_verify are:

  1. flatten_hierarchy,
  2. static_order, and
  3. build_partition_mdds. 

UC Berkeley, VIS Release 1.0 (compiled 11-Dec-95 at 10:36 AM)
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> flatten_hierarchy
vis> static_order
vis> build_partition_mdds
vis> print_partition_stats
Method Inputs-Outputs, 8 sinks, 10 sources, 14 total vertices, 78 mdd nodes

Advanced Ordering

Dynamic ordering of variables may be enabled and disabled using the dynamic_var_ordering command. Dynamic ordering is a technique to reorder the MDD variables to reduce the size of the existing MDDs. The commands flatten_hierarchy and static_order must be invoked before this command. Available methods for dynamic reordering are window and sift. Dynamic ordering may be time consuming, but can often reduce the size of the MDDs dramatically.

Dynamic ordering is best invoked explicitly (using the dynamic_var_ordering -f <method> option) after the build_partition_mdds and print_img_info commands. If dynamic ordering finds a good ordering, then you may wish to save this ordering (using write_order <file>) and reuse it (using static_order -s <method> <file>). With option dynamic_var_ordering -e <method> dynamic ordering is automatically enabled whenever a certain threshold on the overall MDD size is reached. Enabling dynamic ordering may slow down the verification, but it can make the difference between completing and not completing a verification task. 

 
UC Berkeley, VIS Release 1.0 (compiled 13-Dec-95 at 8:36 AM)
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> init_verify
vis> print_partition_stats
Method Inputs-Outputs, 8 sinks, 10 sources, 14 total vertices, 78 mdd nodes
vis> write_order
# UC Berkeley, VIS Release 1.0 (compiled 13-Dec-95 at 8:36 AM)
# network name: main
# generated: Wed Dec 13 14:13:57 1995
#
# name               type            mddId vals levs
sensor.rand_choice  pseudo-input         0    2 (0)
timer.state         latch                1    3 (1, 2)
hwy_light           latch                2    3 (3, 4)
car_present         latch                3    2 (5)
car_present$NS      shadow               4    2 (6)
farm_light          latch                5    3 (7, 8)
timer.rand_choice   pseudo-input         6    2 (9)
timer.state$NS      shadow               7    3 (10, 11)
farm_light$NS       shadow               8    3 (12, 13)
hwy_light$NS        shadow               9    3 (14, 15)
vis> dynamic_var_ordering -f sift
Dynamic variable ordering forced with method sift....
vis> print_partition_stats
Method Inputs-Outputs, 8 sinks, 10 sources, 14 total vertices, 70 mdd nodes
vis> write_order
# UC Berkeley, VIS Release 1.0 (compiled 13-Dec-95 at 8:36 AM)
# network name: main
# generated: Wed Dec 13 14:14:20 1995
#
# name               type            mddId vals levs
sensor.rand_choice  pseudo-input         0    2 (0)
timer.state         latch                1    3 (1, 2)
hwy_light           latch                2    3 (3, 6)
farm_light          latch                5    3 (4, 5)
car_present$NS      shadow               4    2 (7)
car_present         latch                3    2 (8)
timer.rand_choice   pseudo-input         6    2 (9)
timer.state$NS      shadow               7    3 (10, 11)
farm_light$NS       shadow               8    3 (12, 13)
hwy_light$NS        shadow               9    3 (14, 15)
vis> write_order tlc.sift
vis> quit


/projects/vis/vis/mips/bin/vis
UC Berkeley, VIS Release 1.0 (compiled 13-Dec-95 at 8:36 AM)
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> flatten_hierarchy -b
vis> static_order -s input_and_latch tlc.sift
vis> write_order
# UC Berkeley, VIS Release 1.0 (compiled 13-Dec-95 at 8:36 AM)
# network name: main
# generated: Wed Dec 13 14:34:08 1995
#
# name               type            mddId vals levs
sensor.rand_choice  pseudo-input         0    2 (0)
timer.state         latch                1    3 (1, 2)
hwy_light           latch                2    3 (3, 4)
farm_light          latch                3    3 (5, 6)
car_present$NS      shadow               4    2 (7)
car_present         latch                5    2 (8)
timer.rand_choice   pseudo-input         6    2 (9)
timer.state$NS      shadow               7    3 (10, 11)
farm_light$NS       shadow               8    3 (12, 13)
hwy_light$NS        shadow               9    3 (14, 15)

Dynamic ordering moves around binary valued variables, possibly separating a group of variables which encode a single multi-valued variable. Note, however, that the resolution of reading and writing variable ordering files is at the multi-valued variable level, not the bit-level. Therefore when the ordering found by dynamic ordering is read back, the BDD variables which encode the MDD variables do not necessarily occupy the same levels as reported in the file tlc.sift. See for example variable hwy_light in the example above. The only information that is used from the file tlc.sift is the order of the MDD variables in the first column. By editing the file tlc.sift any order can be imposed. Given an ordering of MDD variables, BDD variables which encode them are assigned to the first adjacent available levels.

FSM Traversal and Image Computation

FSM traversal is the core computation in design verification. Efficient traversal requires grouping the MDDs, in a manner optimal for traversal. To traverse the FSM, the present state, input, and next state variables are organized for easy manipulation. All this information is included in an FSM data structure created in the compute_reach command. This also invokes traversal of the entire reachable state set of the FSM representing the design, and may be invoked with different verbosity options to get varying amounts of traversal information. On subsequent calls to compute_reach, the reachability computation is not reperformed, but statistics can be printed using -v.

The reachability computation makes extensive use of image computation. There are several user-settable options that affect the performance of image computation. The documentation for the set command lists these options. Use the command set image_method to change the image computation method, and then re-initialize verification (starting at the flatten_hierarchy command gif). The print_img_info prints current image information. Notice that while print_partition_stats prints information on the next state functions, print_img_info prints information on the next state transition relations. The command print_img_info creates transition relations from transition functions by clustering several functions together. The result is a partitioned transition relation. It is often a good idea to force dynamic variable reordering (for instance, dynamic_var_ordering -f sift) at this point to reorder these relation MDDs. The reachability computation is an optional step of the model checking algorithm; unreachable states may be used as don't cares to minimize the BDD representation.

The following illustrates the command compute_reach on the Traffic Light Controller: 

 
UC Berkeley, VIS Release 1.0 (compiled 11-Dec-95 at 10:36 AM)
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> init_verify
vis> compute_reach -v 1
Computing reachable states using the iwls95 image computation method.
Printing Information about Image method: IWLS95
        Threshold Value of Bdd Size For Creating Clusters = 1000
                (Use "set image_cluster_size value " to set this to desired value)
        Verbosity = 0
                (Use "set image_verbosity value " to set this to desired value) 
        W1 =  6 W2 = 1 W3 = 1 W4 = 2
                (Use "set image_W? value " to set these to desired values) 
        Shared Bdd Size of    1 components is         97
********************************
Reachability analysis results:
FSM depth =                  8
reachable states =          20
MDD size =                   8
analysis time =              0

Specifying Fairness Constraints

Fairness constraints are used to restrict the behavior of the design. Each fairness condition specifies a set of states in the machine, and requires that in any acceptable behavior these states must be traversed infinitely often (i.e., these states must be on a cycle). Such constraints are called ``Büchi fairness'' constraints. Fairness constraints are stored in fairness files (with extension .fair by convention); the syntax for fairness files can be found in http://embedded.eecs.berkeley.edu/Respep /Research/vis/doc/packages/read_fairnessCmd.html. A fairness file is read in by the read_fairness command. Active fairness conditions can be displayed by means of print_fairness. The reset_fairness command is used to reset the fairness constraint to ``true''; by default, there is one fairness condition that contains all states.

Fairness constraints remove unwanted behavior from a system. They are a powerful, but dangerous tool, because it is easy to make a faulty system pass wanted properties by a careless use of fairness constraints.

Language Emptiness

The language of a design is given by sequences over the set of reachable states that do not violate the fairness constraint. If the language is empty, we know that the system does not exhibit any behavior. VIS supports the command lang_empty as an alias for model checking the formula . This is relevant in the context of language containment, where the properties to be verified are also specified as automata and a modified system, consisting of the behavior of the system that does not satisfy the property, is tested for emptiness. Before invoking model checking, lang_empty can also be used to ensure that the system is non-trivial. This is pertinent because the fairness constraint specified may make the entire system ``unfair'', and an empty system passes all universal properties.

VIS produces a debug trace to help the designer understand the cause of the failure. Common corrective actions are the correction of an error in the original system description or addition of fairness constraints.

The language emptiness trace for the Traffic Light Controller example with a fairness constraint is: 

 
UC Berkeley, VIS Release 1.0 (compiled 14-Dec-95 at 1:04 AM)
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> init_verify
vis> read_fairness tlc.fair
vis> print_fairness
Fairness constraints:
!(timer.state=START);
!(timer.state=SHORT);
vis> lang_empty -i
# LE: language is not empty
# LE: generating path to fair cycle
# LE: path to fair cycle:


--State 0:
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

This indicates that there is valid behavior in the system, and an example of this is given; a closed path that begins at the initial state, where no car is present , the farm light is red , the highway light is green , and the timer is in its start state . From the initial state the machine loops through a fair cycle, which has 8 states, and is described below. Note that this trace is differential for both states and inputs; only variables that have changed in the last step are printed. 

 
# LE: fair cycle:


--State 0:
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

--Goes to state 1:
car_present:YES
timer.state:SHORT

--On input:
sensor.rand_choice:1
timer.rand_choice:1

--Goes to state 2:
timer.state:LONG

--On input:
<Unchanged>

--Goes to state 3:
hwy_light:YELLOW
timer.state:START

--On input:
timer.rand_choice:0

--Goes to state 4:
timer.state:SHORT

--On input:
timer.rand_choice:1

--Goes to state 5:
car_present:NO
farm_light:GREEN
hwy_light:RED
timer.state:START

--On input:
sensor.rand_choice:0
timer.rand_choice:0

--Goes to state 6:
car_present:YES
farm_light:YELLOW

--On input:
sensor.rand_choice:1

--Goes to state 7:
timer.state:SHORT

--On input:
timer.rand_choice:1

--Goes to state 8:
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

--On input:
sensor.rand_choice:0
timer.rand_choice:0

Model Checking Operations

Performing Model Checking

The model_check command calls model checking in VIS. A description of the syntax of CTL for VIS is presented in http://embedded.eecs.berkeley.edu/Respep/Research/vis/doc/ctl/ctl ctl.html. By convention CTL properties are in a file with extension .ctl. The following illustrates the functioning of model_check on the Traffic Light Controller example. Note that in this session the fairness constraints are not read in. Debugging error traces is explained in the next section. 

 
UC Berkeley, VIS Release 1.0 (compiled 14-Dec-95 at 1:04 AM)
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> init_verify
vis> model_check -i tlc.ctl


MC: formula passed --- AG(!((farm_light=GREEN * hwy_light=GREEN)))

This indicates that the property passed (i.e. the system satisfies the property). 

 
MC: formula failed --- AG(((car_present=YES * timer.state=LONG) -> AF(farm_light=GREEN)))
MC: Calling debugger

This indicates that the property failed, and gives the following error trace that shows behavior seen in the system that does not satisfy the property. 

 

--State
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

fails AG(((car_present=YES * timer.state=LONG) -> AF(farm_light=GREEN)))
--Counter example is a path to a state where 
((car_present=YES * timer.state=LONG) -> AF(farm_light=GREEN)) is false

--State 0:
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

--Goes to state 1:
car_present:YES
timer.state:SHORT

--On input:
sensor.rand_choice:1
timer.rand_choice:1

--Goes to state 2:
timer.state:LONG

--On input:
<Unchanged>

--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG

fails ((car_present=YES * timer.state=LONG) -> AF(farm_light=GREEN))


--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG

passes (car_present=YES * timer.state=LONG)


--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG

passes car_present=YES


--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG

passes timer.state=LONG

--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG

fails AF(farm_light=GREEN)

--A fair path on which farm_light=GREEN is always false:

--Fair path stem:

--State 0:
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG

--Goes to state 1:
hwy_light:YELLOW
timer.state:START

--On input:
sensor.rand_choice:1
timer.rand_choice:0

--Fair path cycle:

--State 0:
car_present:YES
farm_light:RED
hwy_light:YELLOW
timer.state:START

--Goes to state 1:
<Unchanged>

--On input:
sensor.rand_choice:1
timer.rand_choice:0

This is the end of the debug trace for this CTL formula. The command model_check continues with the next formula. 

 
MC: formula failed --- AG(AF(hwy_light=GREEN))
MC: Calling debugger

This indicates that the property failed, and it is followed by an error trace that shows behavior seen in the system that does not satisfy the property. To save space, we omit the error trace. 

 
MC: formula passed --- !(AG((car_present=YES -> AF(farm_light=GREEN))))
This indicates that the property passed (i.e. the system satisfies the property).

Debugging for Model Checking

If model checking or language emptiness checks fail, VIS reports the failure with a counterexample, i.e., an error trace of sample ``bad'' behavior (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.

In the previous section, the second and third properties fail during model checking. This may be rectified by reading in the fairness constraints previously described for the Traffic Light Controller example. If the fairness constraints are read in, the valid behavior is restricted and these properties pass. In particular, the fairness constraint !(timer.state=START) disallows behavior, where the system stays forever in the state: 

car_present:YES
farm_light:RED
hwy_light:YELLOW
timer.state:START

--On input:
sensor.rand_choice:1
timer.rand_choice:0

More precisely, the fairness constraint disallows behavior, where there is a car in the farm road, but the timer is stuck in its initial state, by forcing the timer to progress in finite time to the next state. 

UC Berkeley, VIS Release 1.0 (compiled 11-Dec-95 at 10:36 AM)
vis> read_fairness tlc.fair
vis> model_check tlc.ctl


MC: formula passed --- AG(!((farm_light=GREEN * hwy_light=GREEN)))

MC: formula passed --- AG(((car_present=YES * timer.state=LONG) -> AF(farm_light=GREEN)))

MC: formula passed --- AG(AF(hwy_light=GREEN))

MC: formula passed --- !(AG((car_present=YES -> AF(farm_light=GREEN))))

Checking Invariants

An important class of CTL formulas is invariants. These are formulas of the form , where is a quantifier-free formula. The semantics of is that is true in all reachable states. The command check_invariant implements an algorithm that is specialized for these formulas. In the following example, is the formula 

!((farm_light = GREEN) * (hwy_light = GREEN));
contained in the file tlc.invar. 

UC Berkeley, VIS Release 1.0 (compiled 13-Dec-95 at 8:36 AM)
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> init_verify
vis> check_invariant tlc.invar

INV: formula passed --- !((farm_light=GREEN * hwy_light=GREEN))

Advanced Model Checking: Abstraction and Reduction

When performing model checking and checking invariant properties, one can use the reduce option -r, to perform model checking on a ``pruned'' FSM, i.e., one where parts that do not affect the formula (directly or indirectly) have been removed.

This mechanism can be combined with the abstraction mechanism available through the command flatten_hierarchy <file>. <file> contains the names of variables to abstract. For each variable x appearing in <file>, a new primary input node named x$ABS is created to drive all the nodes that were previously driven by x. Hence, the node x will not have any fanouts; however, x and its transitive fanins will remain in the network. Abstracting a net effectively allows it to take any value in its range, at every clock cycle. This mechanism can be used to perform manual abstractions.

We show an example, where the file tlc.abstract contains the variable timer.start. By abstracting timer.start, the timer module is disconnected from the rest of the Traffic Light Controller.

Then we perform model checking of the CTL property read from the file tlc.reduce.ctl: 

AG((timer.state = START) -> AF (timer.state = LONG));
This property refers only to the timer module. Since the timer has been disconnected, the rest of the system can be pruned away when testing this property. As expected this property fails, since no fairness constraint has been read in. 

 
UC Berkeley, VIS Release 1.0 (compiled 15-Dec-95 at 2:18 PM)
Sourcing .visrc of Tiziano 
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> flatten_hierarchy tlc.abstract
vis> static_order        
vis> build_partition_mdds
vis> model_check -i -r tlc.reduce.ctl

MC: formula failed --- AG((timer.state=START -> AF(timer.state=LONG)))

MC: Calling debugger

--State
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

fails AG((timer.state=START -> AF(timer.state=LONG)))
since (timer.state=START -> AF(timer.state=LONG)) is false at this state

--State
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

fails (timer.state=START -> AF(timer.state=LONG))


--State
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

passes timer.state=START

--State
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

fails AF(timer.state=LONG)

--A fair path on which timer.state=LONG is always false:

--Fair path stem:

--State 0:
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

--Fair path cycle:

--State 0:
car_present:NO
farm_light:RED
hwy_light:GREEN
timer.state:START

--Goes to state 1:
<Unchanged>

--On input:
sensor.rand_choice:0
timer.rand_choice:0

In this particular example, the same effect of ``restricted'' model checking can be obtained by changing (using the cd command) to the timer node and performing model checking. When at the timer node, the inputs to timer from the rest of the system are considered free inputs. Notice that the names of variables in the CTL property in the file tlc.reduce.ctl must be revised as follows: 

AG((state = START) -> AF (state = LONG));
since the convention for names is to drop the current node and all nodes above from the namepath. 

 
UC Berkeley, VIS Release 1.0 (compiled 14-Dec-95 at 1:04 AM)
Sourcing .visrc of Tiziano 
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> cd timer
vis> init_verify 
vis> model_check tlc.reduce.ctl

MC: formula failed --- AG((state=START -> AF(state=LONG)))

However, there are more complex situations that cannot be emulated so simply.

Combinational and Sequential Equivalence

In VIS it is also possible to check the equivalence of two networks. The command comb_verify verifies the combinational equivalence of two flattened networks. In particular, any set of functions (the roots), defined over any set of intermediate variables (the leaves), can be checked for equivalence between two networks. Roots and leaves are subsets of the nodes of a network, with the restriction that the leaves should form a complete support for the roots. The correspondence between the roots and the leaves in the two networks is specified in a file. The default option assumes that the roots are the combinational outputs and the leaves are the combinational inputs. Two networks are declared combinationally equivalent iff they have the same outputs for all combinations of inputs and pseudo-inputs. An important usage of comb_verify is to provide a sanity check when using SIS to re-synthesize portions of a network, as explained in Chapter 5.

The command seq_verify tests the sequential equivalence of two networks. In this case the set of leaves has to be the set of all primary inputs. This produces the constraint that both networks should have the same number of primary inputs. The set of roots can be an arbitrary subset of nodes. Moreover, no pseudo-inputs should be present in the two networks being compared. Sequential verification is done by building the product finite state machine. The command verifies whether any state, where the values of two corresponding roots differ, can be reached from the set of initial states of the product machine. If this happens, a debug trace is provided.

Simulation

 

Simulation, although not ``formal verification'', is an alternate method for design verification. After the command build_partition_mdds is invoked, the network can also be simulated. In VIS we provide internal simulation of the BLIF-MV description generated by VL2MV, via the simulate command. Thus, VIS encompasses both formal verification and simulation capabilities. simulate can generate random input patterns or accept user-specified input patterns. 

UC Berkeley, VIS Release 1.0 (compiled 15-Dec-95 at 10:24 PM)
vis> read_blif_mv tlc.mv
Warning: Some variables are unused in model main.
vis> init_verify
vis> simulate -n 10
# UC Berkeley, VIS Release 1.0 (compiled 15-Dec-95 at 10:24 PM)
# Network: main
# Simulation vectors have been randomly generated


.inputs  sensor.rand_choice timer.rand_choice 
.latches car_present farm_light hwy_light timer.state 
.outputs 
.initial NO RED GREEN START 

.start_vectors

# sensor.rand_choice timer.rand_choice ; car_present farm_light hwy_light timer.state ; 

0 0 ; NO  RED    GREEN  START ; 
1 1 ; NO  RED    GREEN  START ; 
0 0 ; YES RED    GREEN  SHORT ; 
1 0 ; NO  RED    GREEN  SHORT ; 
1 1 ; YES RED    GREEN  SHORT ; 
0 1 ; YES RED    GREEN  LONG  ; 
0 1 ; NO  RED    YELLOW START ; 
0 0 ; NO  RED    YELLOW SHORT ; 
0 0 ; NO  GREEN  RED    START ; 
1 0 ; NO  YELLOW RED    START ; 
# Final State : NO  YELLOW RED    START 
vis> cd farm_control
vis> simulate -n 10
There is no network. Use flatten_hierarchy.
vis> init_verify
vis> simulate -n 10
# UC Berkeley, VIS Release 1.0 (compiled 15-Dec-95 at 10:24 PM)
# Network: farm_control
# Simulation vectors have been randomly generated


.inputs  car_present enable_farm long_timer short_timer 
.latches farm_light 
.outputs enable_hwy farm_light farm_start_timer 
.initial RED 

.start_vectors

# car_present enable_farm long_timer short_timer ; farm_light ; enable_hwy farm_light farm_start_timer 

NO  1 0 0 ; RED    ; 0 RED    1 
YES 1 1 1 ; GREEN  ; 0 GREEN  1 
NO  1 0 1 ; YELLOW ; 1 YELLOW 0 
YES 0 0 0 ; RED    ; 0 RED    0 
NO  1 1 0 ; RED    ; 0 RED    1 
NO  1 1 1 ; GREEN  ; 0 GREEN  1 
YES 1 1 1 ; YELLOW ; 1 YELLOW 0 
NO  0 1 0 ; RED    ; 0 RED    0 
NO  0 0 0 ; RED    ; 0 RED    0 
YES 0 1 0 ; RED    ; 0 RED    0 
# Final State : RED

Any level of the specified hierarchy may be simulated. The user may traverse the hierarchy to reach the relevant level via the cd command. The init_verify command must be called to set up the appropriate internal data structures before simulation.


next up previous contents
Next: Synthesis in VIS Up: No Title Previous: Introduction to Formal


Yuji Kukimoto
Tue Feb 6 11:58:14 PST 1996
Contact 
©2002-2018 U.C. Regents