Shyam,
Thank you for your feedback. I have taken the liberty of posting this
on the vis-users mailing list, because I think it involves all users.
I agree with you that the current verilog frontend is a limiting factor
for Vis. However, a verilog frontend is very hard to write. ST has
written vl2mv for his master's thesis, and for such a project, he has
done a heroic job. After ST, noone has taken up this challenge.
It would be great if we could find someone to take over the project and
extend the frontend. However, I don't know who would do it.
As an alternative, there is a way to create Blif through a commercial
design compiler (see the FAQ). Have you explored that option? We would
work with you to figure out a workable solution.
Roderick.
Shyam Pullela wrote:
> Hi VIS Group,
>
> Thanks for the update and your continuous effort in upgrading VIS.
> I have a small suggestion for future improvements. I think any tool's
> real use is better tested by industrial examples. One thing that is
> preventing
> me from using VIS effectively in industry is it's Verilog front-end.
> Unfortunately, the Verilog subset that vl2mv accepts is too small for
> most of the designs I come across.
>
> In my previous company, we used to use a very restricted form of Verilog
> to make it compatible with some of our internal cycle-based simulaotrs.
> Fortunately that subset was very close to what vl2mv can accept so I used
> to be able to use VIS on most of desings. No that I moved to a different
> company, designers are using regular full set of Verilog which makes it
> almost
> impossible to use VIS.
>
> I know that main purpose of the group is to study MC and improve the
> algorithms
> for MC. But I feel making if a bit more robust in Verilog front-end will
> make the
> tool more usable in industry thus giving the academia a better understanding
> of
> real problems in industry.
>
> My 2 cents.
>
> Cheers,
>
> -- Shyam
>
> ---------------------------------------------------------------------------------------------
>
> Shyam Pullela, Manager, HW Engineering
> (408)527-1701
> Cisco Systems Inc., San Jose, CA 95134
> spullela@cisco.com
> ---------------------------------------------------------------------------------------------
>
> >
> > DESCRIPTION
> >
> > Formal verification system with Verilog HDL front end. Computation
> > model is a set of synchronously communicating FSMs. Emphasis is on
> > fair CTL (computation tree logic) model checking, with error trace
> > generation. Supports, as proof of concept, cycle-based simulation,
> > combinational equivalence checking, and sequential equivalence
> > checking. Has synthesis capabilities and links to the sequential
> > synthesis tool, SIS. Jointly developed by Univ. of California at
> > Berkeley,
> > Univ. of Colorado at Boulder.
> >
> > 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 <HintsFileName> : guided symbolic state space
> > traverse
> > check_invariant -g <HintsFileName> : 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 <HintsFileName>
> >
> > 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 <HintsFileName>
> > check_invariant -g <HintsFileName>
> >
> > 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 <depth> : sets the cluster depth for SPFD
> > computation.
> > spfd_pilo -f <file> : use simulation vectors from specified
> > file. These vectors are used to compute
> > switching activity of nodes in the circuit.
> > spfd_pilo -S <method-number> : selects one of several methods to
> > choose the node to be optimized.
> > spfd_pilo -m <method-number> : 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.
This archive was generated by hypermail 2b30 : Fri May 18 2001 - 11:42:01 MDT