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: References Up: No Title Previous: Commands in VIS List of Commands in VIS   The following list contains a one line summary of all the commands available within VIS. The list can also be found in http://embedded.eecs.berkeley.edu/Respep/Research/vis/doc/packages /cmdIndex.html. Fig. A.1 graphically illustrates the suite of commands available within VIS, and their dependencies. A command cannot be executed before its predecessors (unless the predecessor is also a successor). Default aliases are defined, type alias to list them.   Figure A.1:   A Flow Chart of Commands in VIS. alias: provide an alias for a command build_partition_mdds: build a partition of MDDs for the current network cd: change the current node check_invariant: checks all states reachable in flattened network satisfy specified invariants comb_verify: verifies the combinational equivalence of two networks compute_reach: compute the set of reachable states of the FSM dynamic_var_ordering: control the application of dynamic variable ordering echo: merely echoes the arguments flatten_hierarchy: create a flattened network help: provide on-line information on commands history: a UNIX-like history mechanism inside the VIS shell init_verify: create and initialize a flattened network for verification lang_empty: performs BDD based check of language emptiness under Buchi fairness ls: list all the child nodes at the current node model_check: performs BDD based fair CTL model checking on a network print_bdd_stats: print the BDD statistics for the flattened network print_fairness: print the fairness constraints of the flattened network print_hierarchy_stats: print the statistics of the current node 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_models: list all the models and their statistics print_network: print the flattened network print_network_stats: print statistics about the flattened network print_partition: write a file in the "dot" format describing the partition graph print_partition_stats: print statistics about the partition graph 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 set of fairness constraints read_verilog: read a verilog file reset_fairness: reset the fairness constraints seq_verify: verifies the sequential equivalence of nodes in two networks set: set an environment variable simulate: simulate the flattened network source: execute commands from a file static_order: order the MDD variables of the flattened network test_det_and_comp_spec: test if the outputs are completely specified and deterministic test_network_acyclic: determine whether the network is acyclic time: provide a simple elapsed time value unalias: removes 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 Next: References Up: No Title Previous: Commands in VIS Yuji Kukimoto Tue Feb 6 11:58:14 PST 1996

Contact

©2002-2018 U.C. Regents