RELEASE NOTES FOR VIS 1.4 Release 1.4 of VIS improves VIS 1.3 in the following areas: 1. Hybrid Image Computation 2. Guided Search for Reachability Analysis and Invariant Checking 3. Guided Search for CTL Model Checking 4. Least Fix-point Machine-By-Machine Approximate FSM Traversal (LMBM) 5. Iterative Abstraction-based Model Checking (IMC) 6. Lazy Sifting 7. SPFD-based Placement and Logic Optimization 8. Truesim 9. Arithmetic Functions with Extended Double Precision (EPD) 10. CUDD 2.3.1 11. Miscellaneous 1. Hybrid Image Computation --------------------------- Image computation is the key step in fix-point computation. Traditionally two techniques have been used: The transition relation method is based on conjunction of a partitioned transition relation, whereas the transition function method is based on splitting on an input or output variable recursively. The hybrid method chooses either splitting or conjunction at each recursion dynamically using the dependence matrix. This hybrid approach combines, in a unified framework, conjunction, input and output splitting, and a host of auxiliary techniques that can significantly speed up the computation. See: I.-H. Moon, J.H. Kukula, K. Ravi, F. Somenzi, "To Split or to Conjoin: The Question in Image Computation", Proceedings of the Design Automation Conference (DAC), pages 73-90, 2000. Also, the transition function method is implemented as a part of the hybrid computation. The transition function method itself can be used as an independent image method. However, we do not recommend to use this method in general cases, even though it may work well for approximate reachability analysis. The implementation of the transition function method is basically for experimental purposes. ** Usage: set image_method hybrid set image_method tfm Also refer to: print_hybrid_options and print_tfm_options 2. Guided Search for Reachability Analysis ------------------------------------------ VIS-1.4 introduces the use of hints to guide the exploration of the state space. This may result in orders-of-magnitude reductions in time and space requirements. Good hints can often be found with the help of simple heuristics by someone who understands the circuit well enough to devise simulation stimuli or verification properties for it. Hints are applied by constraining the transition relation of the system to be verified. They specify possible values for (subsets of) the primary inputs and state variables. The constrained traversal of the state space may proceed much faster than the standard breadth-first search, because the traversal with hints is designed to produce smaller BDDs. Once all states reachable following the hints have been visited, the system is unconstrained and reachability analysis proceeds on the original system. Given enough resources, the algorithm will therefore search all reachable states, unless a state that violates the invariant is found. See: K. Ravi, F. Somenzi, "Hints to accelerate Symbolic Traversal", Correct Hardware Design and Verification Methods (CHARME), pages 250-264, 1999. ** Usage: compute_reach -g : guided symbolic state space traverse check_invariant -g : guided search for invariant checking The file HintsFileName contains a series of hints. A hint is a formula that does not contain any temporal operators, so hints_file has the same syntax as a file of invariants used for check_invariant. Also refer to: model_check -g 3. Guided Search for CTL Model Checking --------------------------------------- Guided Search for CTL is an extension of Guided Search for reachability. It works much along the same lines, and has the same benefits. There are a few differences. First, for greatest fixpoints (EG, AU, and AF), it uses overapproximations of the transition relation, instead of underapproximations. Second, there is a distinction between local and global hints. Local hints are the default. They can be used for any kind of CTL formula, and will apply all hints to a subformula before moving up in the parse tree. Global hints are only applicable to ACTL and ECTL formulae, and evaluate the entire formula once for every hint. See: R. Bloem, K. Ravi, and F. Somenzi, "Symbolic Guided Search for CTL Model Checking", Proceedings of the Design Automation Conference (DAC), pages 29-34, 2000. ** usage: model_check -g HintsFileName : perform model check guided by the hints specified in HintsFileName Also refer to: compute_reach -g check_invariant -g 4. Least Fix-point Machine-By-Machine Approximate FSM Traversal (LMBM) ---------------------------------------------------------------------- The knowledge of the reachable states of a sequential circuit can dramatically speed up optimization and model checking. Since exact reachability may be intractable, approximate techniques are often preferable. Least Fix-point MBM (LMBM) method is such a technique. It is as efficient as MBM, but provably more accurate. LMBM can compute RFBF-quality approximations for all the large ISCAS-89 benchmark circuit in a total of less than 9000 seconds. For more information, see: I.-H. Moon, J. Kukula, T. Shiple, F. Somenzi, "Least Fixpoint Approximation for Reachability Analysis," International Conference on Computer-Aided Design (ICCAD), pages 41-44, 1999. ** Usage: set ardc_traversal_method 4: LMBM(least fix-point MBM, default) is selected for ARDC set ardc_traversal_method 5: TLMBM(combination of LMBM and TFBF) is selected for ARDC model_check -D 3 : model checking with ARDCs compute_reach -A 2 : compute over-approximate reachable states compute_reach -D : compute exact reachable states with the help of ARDCs check_invariant -D : check invariants with the help of ARDCs synthesize_network -r 3 : synthesize sequential network with ARDCs Also refer to: print_ardc_options 5. Iterative Abstraction-Based Model Checking (IMC) --------------------------------------------------- VIS-1.4 introduces an automatic abstraction/refinement algorithm for symbolic CTL model checking. This algorithm supports full CTL language without fairness constraints. The algorithm begins with initial upper- and/or lower-bound approximations that include some exact sub-transition relations of a determined set of latches for a given CTL formula. As long as a conclusive verification decision can't be reached due to potentially false positives and negatives, the system is refined. Two refinement methods are implemented: Latch Name Sorting and Latch Affinity Scheduling. For more information, See: J.-Y. Jang, I.-H. Moon, G.D. Hachtel, "Iterative Abstraction-based CTL Model Checking," Design Automation and Test in Europe (DATE), pages 502-507, 2000. IMC supersedes the AMC package, which may disappear in future releases. ** Usage: iterative_model_check -i 8 : iterative model checking with incremental refinement step set to 8 latches iterative_model_check -r 0 : iterative model checking using Latch Name Sorting refinement scheduling iterative_model_check -g 1 : iterative model checking using Positive Operational Graph only Also refer to: model_check, approximate_model_check, incremental_ctl_verification 6. Lazy Sifting --------------- Lazy sifting is a new variable reordering option that is specifically designed for sequential verification with the transition relation method (i.e., IWLS95 in VIS). Lazy sifting groups together corresponding present state and next state variables only when it expects the grouping to be beneficial. See: H. Higuchi and F. Somenzi, "Lazy Group Sifting for Efficient Symbolic State Traversal of FSMs," Proceedings of the International Conference on Computer-Aided Design (ICCAD), pages 45-49, 1999. ** Usage: dynamic_var_ordering -e lazy_sift 7. SPFD-based placement and logic optimization ---------------------------------------------- This is an algorithm based on Sets of Pairs of Functions to be Distinguished (SPFDs) that combines logic and placement optimization of combinational circuits mapped to LUT-based Field-Programmable Gate Arrays to improve circuit area and speed. The flexibilities in the circuit are represented by SPFDs. The package contains two commands: spfd_pilo - perform SPFD-based placement-independent logic optimization; and spfd_pdlo - simultaneous placement and logic optimization. spfd_pilo performs SPFD-based wire and node removal/replacement and reprogramming of combinational circuits mapped to LUT-based FPGAs to reduce the number of wires and nodes in the circuit. Instead of computing the flexibilities for every node in the network at once, the algorithm computes the flexibilities for one `cluster' at a time. Working with clusters allows us to avoid the BDD explosion problem and hence handle large circuits. The SPFDs are computed for the cluster and the cluster nodes are reprogrammed based on the flexibility derived. Switching activity (computed via simulation of user specified bit vectors or randomly generated bit vectors) is used to drive the choice of alternate function to be implemented at the node, in such a way that the total switching activity in the circuit is minimized. In the absence of bit vectors, an arbitrary implementation for a node is chosen from the bounds represented by SPFDs. The command spfd_pdlo implements a technique that tightly links the logic and placement optimization steps. The algorithm is based on simulated annealing. Two types of moves (directed towards global reduction in the cost function of total wire length), are performed: (1) wire removal/replacement, and (2) swapping of a pair of blocks in the FPGA. Feedback from placement is valuable in making informed choice of a target wire during logic optimization moves. This command produces a placement file which is used by VPR for routing. spfd_pdlo can be used only if VIS is linked with VPR 4.22, an FPGA place and route tool from the University of Toronto (http://www.eecg.toronto.edu/~vaughn/vpr/vpr.html). VPack, a tool to convert circuits (mapped to FPGA blocks) in .BLIF format to the .net format (used by VPR), is also needed. Please contact Balakrishna Kumthekar (kumtheka@avanticorp.com) for details on integrating VPR with VIS. See: B. Kumthekar and F. Somenzi, "Power and Delay Reduction via Simultaneous Logic and Placement Optimization in FPGAs," Design Automation and Test in Europe (DATE), pages 202-207, 2000. ** usage: spfd_pilo -D : sets the cluster depth for SPFD computation. spfd_pilo -f : use simulation vectors from specified file. These vectors are used to compute switching activity of nodes in the circuit. spfd_pilo -S : selects one of several methods to choose the node to be optimized. spfd_pilo -m : selects the heuristic to use in optimizing a selected node. See 'help spfd_pilo' and 'help spfd_pdlo' for various options. 8. Truesim ---------- Simulates a network with a set of input vectors. Before calling this command, the user should create a partition (using the command build_partition_mdds). The simulation vectors can be provided by the user (using -f vectors_file), or generated randomly. When -d option is used, it performs event-driven true delay simulation. The fanout count of the nodes is used as an estimate for the node delay. Primary inputs are assumed to have arrival times of zero. 9. Arithmetic Functions with extended double precision (EPD) ------------------------------------------------------------ This is an arithmetic function package for extended double precision format floating-point numbers. It supports the IEEE-754 double (64-bit) precision floating-point number format: both the big_endian and the little_endian. The range is from 2.2631E-4932 to 1.1897E+4932. This package is used internally to provide fast and accurate counting of the states in large FSMs like those encountered in approximate reachability analysis. 10. New version of the CUDD package. ----------------------------------- VIS-1.4 includes CUDD 2.3.1. Compared to the version that was included in VIS-1.3, the new version contains a number of bug fixes and several new functions. * Miscellaneous ============= ** One bug in the CAL package has been fixed. It affected platforms without the valloc function. ** Changes in supported platforms. Support for SunOS 5.8 (Solaris 2.8) on the Intel x86 platform has been added. Ultrix and SunOs 4 are no longer supported. ** Change of Verbosity level for debugging in model_check Debugging refers to the printing of an error-trace when a formula fails. The new debug levels are: -d0: no debugging (the old -d0) -d1: minimal debugging, with less verbosity than the old -d1 had -d2: minimal debugging with more verbosity (the old -d1) -d3: recursive debugging (the old -d2) -d4: interactive debugging (the old -d3) ** Early termination in Model Checking. In limited cases, VIS will terminate a model checking run before reaching a fixpoint. This may lead to a speedup. ** The set of fair states is not computed of there are no fairness constraints. This may lead to a speedup of the model_check command. ** Perl Script for pretty printing counter-examples. The Perl script visdbgpp, contributed by Toshi Isogai, can be run on counterexamples produced by vis to improve their readability. In particular, the script collects the bits of vectors and displays them on a single line. ** Counterexample generation. The states on an error trace now lie closer together, which means that, on average, fewer signal transitions will occur. ** Variable reordering. In flatten_hierarchy In VIS-1.4, variable reordering is invoked automatically during flatten_hierarchy. ** Changes of passing BDD cube arguments in VIS to CUDD. Some arguments in the CUDD functions are BDD cubes that are generated by the conjunctions of BDD variables on demand. VIS-1.4 pre-builds some BDD cubes that do not change, such as for present state variables, next state variables, and primary input variables. This speeds up significantly large runs, especially for approximate reachability analysis.