Command Documentation

_ctlp_test

test the CTL parser

_ctlsp_test

test the CTL* parser

_grab_test

Performs invairant checking on a flattened network with the GRAB abstraction refinement algorithm.

_init_state_formula

write resettability condition as a CTL formula

_mAig_test

_memory_profile

It shows the amount of memory used by every pacakge.

_ntm_test

test the ntm package

_tbl_test

test the functionality of the tbl package.

_tst_test

template for implementing commands

alias

provide an alias for a command

approximate_model_check

perform ACTL model checking on an abstracted and flattened network

bdd_sat_bounded_model_check

performs an LTL bounded model checking on a flattened network

bounded_model_check

Performs a SAT-based LTL model checking on a flattened network

build_partition_maigs

build a partition of MAIGs for the flattened network

build_partition_mdds

build a partition of MDDs for the flattened network

cd

change the current node

check_invariant

check all states reachable in flattened network satisfy specified invariants

cnf_sat

Perform SAT solving with CNF input

collapse_child

Collapses a parent (which is the current node) and a given child node into the parent

comb_verify

verify the combinational equivalence of two flattened networks

compute_reach

compute the set of reachable states of the FSM

decompose_child

Partitions Node components into child nodes.

dynamic_var_ordering

control the application of dynamic variable ordering

echo

merely echo the arguments

flatten_hierarchy

create a flattened network

help

provide on-line information on commands

history

list previous commands and their event numbers

incremental_ctl_verification

Verify a set of CTL formulas by means of an incremental model checking algorithm.

init_verify

create and initialize a flattened network for verification

iterative_model_check

Perform CTL model checking on an abstracted system with automatic refinement algorithm.

lang_empty

perform language emptiness check on a flattened network

ls

list all the child nodes at the current node

ltl2snf

Trnalate LTL formula into Separated Normal Form.

ltl_model_check

perform LTL model checking on a flattened network

ltl_to_aut

translate LTL formulae into Buechi automata

model_check

perform fair CTL model checking on a flattened network

network_sweep

sweeps the network to ensure that deterministic constants are removed

print_aig_stats

print statistics about the AND/INVERTER graph.

print_ardc_options

print information about the ARDC options currently in use

print_bdd_stats

print the BDD statistics for the flattened network

print_fairness

print the fairness constraint of the flattened network

print_guided_search_options

print information about guided_search_options in use

print_hd_options

print information about the HD options currently in use

print_hierarchy_stats

print the statistics of the current node

print_hybrid_options

print information about the hybrid image computation options currently in use

print_img_info

print information about the image method currently in use

print_io

print the names of inputs/outputs in the current node

print_latches

print the names of latches in the current node

print_mlp_options

print information about the MLP image computation options currently in use

print_models

list all the models and their statistics

print_network

print information about the flattened network

print_network_dot

print a dot description of the flattened network

print_network_stats

print statistics about the flattened network

print_partition

print the "dot" format describing the partition graph

print_partition_aig_dot

print a dot description of the AND/INVERTER graph that was built for the flattened network

print_partition_stats

print statistics about the partition graph

print_tfm_options

print information about the transition function based image computation options currently in use

pwd

print out the full path of the current node from the root node

quit

exit VIS

read_blif

read a blif file

read_blif_mv

read a blif-mv file

read_fairness

read a fairness constraint

read_order

Read and reorder variable order from a file.

read_verilog

read a verilog file

regression_test

perform regression test with the information given in arguments file

res_verify

Verifies a combinational circuit using residue arithmetic.

reset_fairness

reset the fairness constraint

restruct_fsm

Restructre the STG of a finite state machine to reduce power dissipation.

seq_verify

verify the sequential equivalence of two flattened networks

set

set an environment variable

set_bdd_parameters

Creates a table with the value of all the flags currently active in VIS and calls the function bdd_set_parameters with the manager of the current place in the hierarchy and the table.

simulate

simulate the flattened network

source

execute commands from a file

spfd_pdlo

Perform SPFD-based simultaneous placement and logic optimization.

spfd_pilo

Perform SPFD-based placement independent logic optimization.

static_order

order the MDD variables of the flattened network

synthesize_network

Synthesizes a network using ZDD factorization method.

test_network_acyclic

determine whether the network is acyclic

time

provide a simple elapsed time value

truesim

Simulate the flattened network

unalias

remove the definition of an alias.

unset

unset an environment variable

usage

provide a dump of process statistics

which

look for a file called name

write_blif

determinize, encode and write an hnode to a blif file

write_blif_mv

write a blif-mv file

write_order

write the current order of the MDD variables of the flattened network

write_smv

write an smv file