source: vis_dev/vis-2.1/NEWS @ 15

Last change on this file since 15 was 11, checked in by cecile, 13 years ago

Add vis

File size: 65.9 KB
Line 
1VIS NEWS                                        -*-indented-text-*-
2  History of user-visible changes.
3
4Please sent bug reports to vis-users@colorado.edu.  Please let us know what
5version of VIS you are running and what architecture you are running it on.
6
7======================================================================
8
9Version 2.1
10
11Release 2.1 of VIS improves VIS 2.0 in the following areas:
12
131. Revamped Bounded Model Checker with efficient termination criteria
142. Grab and Puresat algorithms for invariant checking based on
15   abstraction refinement
163. DnC algorithm for language emptiness check based on abstraction
17   refinement
184. CirCUs SAT solver.
195. Fate and Free Will algorithm for the analysis of counterexamples
206. Vacuity detection for CTL
217. Coverage estimation for CTL
228. Far Side algorithm for image computation
239. CUDD 2.4.1
2410. Miscellaneous
25
26
27Bounded Model Checking
28----------------------
29
30BMC in VIS 2.1 is much faster than it was in VIS 2.0.  The
31construction of the circuit data structure, the encoding of the
32property, the use of a faster SAT solver all have contributed to this
33improvement.
34
35BMC in VIS 2.1 can prove properties rather than just falsifying them.
36The following sequence of commands is used to perform bounded model
37checking with termination check:
38
39  read_blif_mv model.mv
40  flatten_hierarchy
41  build_partition_maigs
42  bounded_model_check -k 10 -r 2 model.ltl
43
44The termination check will be performed every other step.  The
45construction of the MDDs is not needed if termination check is needed
46for invariant properties only.  For details on the stopping criteria,
47see
48
49M. Awedh and F. Somenzi, "Proving More Properties with Bounded Model
50Checking," CAV 2004, pp. 96-108, LNCS 3114.
51
52Other new options to the bounded_model_check command allow one to
53control the formula encoding, the solver to be applied (CirCUs or
54zChaff) and, for the former, the incremental solving algorithm.
55
56A new command ltl2snf allows one to translate an LTL formula to
57separation normal form.
58
59
60Abstraction Refinement for Invariants
61-------------------------------------
62
63The check_invariant command allows the user the choice of one of two
64abstraction refinement algorithms for invariants.  The Grab algorithm
65uses BDD-based model checking on the abstract model and SAT for
66counterexample concretization check.  Its refinement strategy is
67game-theoretic.  It is run as follows:
68
69  read_blif_mv model.mv
70  flatten_hierarchy
71  build_partition_maigs
72  check_invariant -A3 model.inv
73
74By default, grab enables dynamic variable reordering for the abstract
75model.  One can override this behavior by explicitly building
76partition MDDs.  For details of the algorithm, see
77
78C. Wang, B. Li, H. Jin, G. D. Hachtel, and F. Somenzi, "Improving
79Ariadne's Bundle by Following Multiple Threads in Abstraction
80Refinement," ICCAD 2003, pp. 408-415.
81
82The puresat algorithm uses SAT as the only decision procedure for both
83abstract and concrete model.  It analyzes the proofs of
84unsatisfiability to produce refinements.  It is invoked as follows:
85
86  read_blif_mv model.mv
87  flatten_hierarchy
88  build_partition_maigs
89  check_invariant -A4 model.inv
90
91The algorithm is described in
92
93B. Li, C. Wang, and F. Somenzi, "Abstraction Refinement in Symbolic
94Model Checking Using Satisfiability as the Only Decision Procedure,"
95STTT, vol.7, n. 2, pp. 143-155.
96
97
98Abstraction Refinement for Language Emptiness
99--------------------------------------------
100
101The lang_empty command has a new option that runs the "Divide and
102Compose" (DnC) algorithm described in
103
104C. Wang, R. Bloem, G. D. Hachtel, K. Ravi, and F. Somenzi, "Divide and
105Compose: SCC Refinement for Language Emptiness", CONCUR 2001,
106pp. 456-471, LNCS 2154.
107
108The algorithm, which is based on refinement of the strongly connected
109components of the model, is invoked as follows:
110
111  read_blif_mv model.mv
112  init_verify
113  lang_empty -A 1
114
115
116CirCUs SAT solver
117-----------------
118
119VIS 2.1 includes the SAT solver CirCUs, a short description of which
120can be found in
121
122H. Jin, M. Awedh, and F. Somenzi, "CirCUs: A Satisfiability Solver
123Geared Towards Bounded Model Checking," CAV 2004, pp. 519-522, LNCS
1243114.
125
126CirCUs is an incremental SAT solver that accepts input in either
127circuit or CNF form.  It is the default solver for bounded model
128checking and abstraction refinement algorithms.  It can also be
129invoked from the VIS prompt as a stand-alone CNF SAT solver on a set
130of clauses described in DIMACS format:
131
132  cnf_sat input.cnf
133
134
135Fate and Free Will Algorithm
136----------------------------
137
138The counterexamples produced by model_check and check_invariant can be
139optionally generated with the Fate and Free Will algorithm of
140
141H. Jin, K. Ravi, and F. Somenzi, "Fate and Free Will in Error Traces,"
142STTT, vol. 6, n. 2, pp. 102-116.
143
144This algorithm is only available when vis is linked with the cu BDD
145package.  It assumes a partition of the inputs into variables
146controlled by the environment and variables controlled by the system,
147and divides a counterexample into fated and free segments.  In a fated
148segment, the values of the variables controlled by the environment
149suffice to impose progress toward violation of the property.  In a
150free segment, the other variables are also required.
151
152To run the Fate and Free Will algorithm, one prepares a file with the
153inputs that the system controls.  For a failing invariant, the
154invocation is like this:
155
156  read_blif_mv model.mv
157  init_verify
158  check_invariant -d1 -i -w system_inputs
159
160The last command is replaced by
161
162  model_check -d2 -i -w system_inputs
163
164for a CTL property.  The -W option can be used to assign all inputs to
165the system, while the -G option invokes a variant of the algorithm.
166
167
168Vacuity Detection for CTL
169-------------------------
170
171VIS 2.1 implements two algorithms for the detection of vacuity in CTL
172model checking.  A formula passes vacuously if it can be strengthened
173by replacement of one of its subformulae with "bottom" and still pass.
174Likewise, a formula fails vacuously if it can be weakened by
175replacement of one of its subformulae with "top" and still fail.
176
177The algorithm of Beer et al. (CAV 97) is invoked with the -B option as
178follows:
179
180  read_blif_mv model.mv
181  init_verify
182  model_check -B model.ctl
183
184This algorithm applies to a subset of ACTL and considers only passing
185properties.  If an error trace is requested with -d, in case of
186vacuous pass, an interesting witness is produced.
187
188The second algorithm for vacuity detection is an extension of the one
189describe in
190
191M. Purandare and F. Somenzi, "Vacuum Cleaning CTL Formulae," CAV 2002,
192pp. 485-499, LNCS 2404.
193
194This algorithm applies a thorough vacuity detection to all of CTL and
195to both passing and failing properties.  With -d, it produces
196interesting witnesses for passing properties and interesting
197counterexamples for failing ones.
198
199The current implementation is limited in its treatment of the
200operators <-> (equivalence) and ^ (exclusive or).
201
202
203Coverage Estimation for CTL
204---------------------------
205
206VIS 2.1 provides two algorithms for coverage estimation in CTL model
207checking.  Both are invoked with options passed to the model_check
208command.
209
210The first algorithm is the one of Hoskote et al. (DAC 1999).  It
211applies to a subset of ACTL.  The option is -C.  The second algorithm
212is an improved version of the same described in
213
214N. Jayakumar, M. Purandare, and F. Somenzi, "Dos and Don'ts of CTL
215State Coverage Estimation," DAC 2003, pp. 292-295.
216
217To invoke the improved coverage estimation algorithm one writes:
218
219  read_blif_mv model.mv
220  init_verify
221  model_check -I model.ctl
222
223
224Far Side Algorithm for Image Computation
225----------------------------------------
226
227By setting image_farside_method to 1, a user of VIS 2.1 can invoke the
228Far Side approach to image computation which applies a compositional
229method based on don't cares to speed up reachability analysis.  The
230algorithm is described in
231
232C. Wang, G. D. Hachtel, and F. Somenzi, "The Compositional Far Side of
233Image Computation," ICCAD 2003, pp. 334-340.
234
235See the documentation of the "set" command for the details.
236
237
238CUDD 2.4.1
239----------
240
241VIS-2.0 includes CUDD 2.4.1.  Compared to the version that was
242included in VIS-2.0, the new version has faster grabage collection,
243provides improved support for C++ compilation, contains a number of
244bug fixes and several new functions, including functions for the
245manipulation of prime implicants of a function.
246
247
248Miscellaneous
249-------------
250
251* Glu and vis can be built using g++ as compiler by configuring as
252  follows:
253
254  ./configure --enable-gcc=g++
255
256* The code in glu has gone through another round of rejuvenation.
257  This process allows vis to be built with recent versions of gcc (3.3
258  and later) without producing any type-punning warning.
259
260* Two bugs have been fixed in early termination detection in CTL model
261  checking.
262
263* A bug has been fixed in the treatment of multi-valued inputs.
264
265* Vis no longer crashes when compute_reach is invoked with the -i
266  option.
267
268* Timeout values for model_check, check_invariant, and lang_empty are
269  now in CPU time instead of elapsed time.  This is beneficial when
270  running regression tests in the presence of other processes.
271
272* The ctime command is no longer supported.
273
274
275======================================================================
276
277Version 2.0
278
279Release 2.0 of VIS improves VIS 1.4 in the following areas:
280
2811. LTL model checking
2822. SAT-based Bounded Model Checking (BMC)
2833. Minimum Lifetime Permutation (MLP) algorithm for conjuction scheduling
2844. Generalized SCC Hull (GSH) algorithm for greatest fixpoint
285   computation
2865. Lockstep algorithm for language emptiness
2876. Built-in regression test facility
2887. CUDD 2.3.2
2898. Miscellaneous
290
291
292LTL model checking
293------------------
294
295VIS-2.0 has a new command ltl_model_check that model checks LTL
296formulae.  The syntax for LTL is quite similar to that used for CTL.
297Another new command, ltl_to_aut, translates LTL formulae into Buechi
298automata.
299
300
301SAT-Based Bounded Model Checking
302--------------------------------
303
304VIS-2.0 has a new command bounded_model_check for bounded LTL model
305checking.  The SAT solver zchaff (http://www.ee.princeton.edu/~chaff/)
306must be in the executable path for this command to work.  The following
307sequence of commands is used to perform bounded model checking:
308
309  read_blif_mv model.mv
310  flatten_hierarchy
311  build_partition_maigs
312  bounded_model_check -k 10 model.ltl
313
314where "-k 10" specifies the bound on the length of the counterexample.
315
316
317Minimum Lifetime Permutation (MLP) Algorithm for Conjuction Scheduling
318----------------------------------------------------------------------
319
320The MLP algorithm can considerably speed up image computations.  It is
321selected by typing
322
323  set image_method mlp
324
325For details on the algorithm, see
326
327I-H. Moon, G. D. Hachtel, and F. Somenzi, "Border-Block Triangular
328Form and Conjunction Schedule in Image Computation," FMCAD 2000,
329pp. 73-90, LNCS 1954.
330
331
332Generalized SCC Hull (GSH) Algorithm for Greatest Fixpoint Computation
333----------------------------------------------------------------------
334
335The commands model_check, ltl_model_check, and lang_empty use a new
336algorithm for greatest fixpoint computations.  This algorithm has
337different "schedules" that can be controlled with the -S option.  For
338details on the algorithm, see
339
340K. Ravi, R. Bloem, and F. Somenzi, "A Comparative Study of Symbolic
341Algorithms for the Computation of Fair Cycles," FMCAD 2000,
342pp. 143-160, LNCS 1954.
343
344F. Somenzi, K. Ravi, and R. Bloem, "Analysis of Symbolic {SCC} Hull
345Algorithms," FMCAD 2002, To appear.
346
347
348Lockstep Algorithm for Language Emptiness
349-----------------------------------------
350
351In VIS-2.0, the commands ltl_model_check and lang_empty can use the
352lockstep algorithm to perform the language emptiness check.  The use
353of the lockstep algorithm as an alternative to the GSH algorithm is
354controlled by the -L option.  For details of Lockstep, see
355
356R. Bloem, H. N. Gabow, and F. Somenzi, "An Algorithm for Strongly
357Connected Component Analysis in n log n Symbolic Steps," FMCAD 2000,
358pp. 37-54, LNCS 1954.
359
360
361Built-in Regression Test Facility
362---------------------------------
363
364VIS-2.0 has a new command regression_test which allows users to
365compare runs of two different versions of vis, or runs with different
366options.
367
368
369CUDD 2.3.2
370----------
371
372VIS-2.0 includes CUDD 2.3.2.  Compared to the version that was
373included in VIS-1.4, the new version contains a number of bug fixes
374and several new functions.
375
376In particular, there is a new function that will compute the AND of
377two BDDs only if the result does not require the creation of too many
378nodes.  This function is used by VIS-2.0 to make clustering of the
379transition relation more robust.
380
381
382Miscellaneous
383-------------
384
385* Improved counterexample generation in model_check with -d3 and -d4.
386
387* Changes in verbosity level (-v option) of model_check.  The new
388  verbosity levels are:
389  -v0: unchanged (minimum verbosity)
390  -v1: essential statistics (new)
391  -v2: equivalent to the old -v1
392  -v3: equivalent to the old -v2
393
394* Fixed bug and extended early termination detection in CTL model
395  checking.
396
397* Fixed bug in guided search for CTL model checking which affected
398  counterexample generation with global hints.
399
400* Vis no longer crashes when a directory name is specified in a
401  command line instead of a regular file name.
402
403* Fixed several bugs in approximate_model_check,
404  incremental_ctl_verification, and iterative_model_check.
405
406* The code in glu has been substantially rejuvenated.
407
408======================================================================
409
410Version 1.4
411
412Release 1.4 of VIS improves VIS 1.3 in the following areas:
413
414 1. Hybrid Image Computation
415 2. Guided Search for Reachability Analysis and Invariant Checking
416 3. Guided Search for CTL Model Checking
417 4. Least Fix-point Machine-By-Machine Approximate FSM Traversal (LMBM)
418 5. Iterative Abstraction-based Model Checking (IMC)
419 6. Lazy Sifting
420 7. SPFD-based Placement and Logic Optimization
421 8. Truesim
422 9. Arithmetic Functions with Extended Double Precision (EPD)
42310. CUDD 2.3.1
42411. Miscellaneous
425
426
4271. Hybrid Image Computation
428---------------------------
429Image computation is the key step in fix-point computation.
430Traditionally two techniques have been used: The transition relation
431method is based on conjunction of a partitioned transition relation,
432whereas the transition function method is based on splitting on an
433input or output variable recursively.
434
435The hybrid method chooses either splitting or conjunction at each
436recursion dynamically using the dependence matrix.  This hybrid
437approach combines, in a unified framework, conjunction, input and
438output splitting, and a host of auxiliary techniques that can
439significantly speed up the computation. See: I.-H. Moon, J.H. Kukula,
440K. Ravi, F. Somenzi, "To Split or to Conjoin: The Question in Image
441Computation", Proceedings of the Design Automation Conference (DAC),
442pages 73-90, 2000.
443
444Also, the transition function method is implemented as a part of the
445hybrid computation.  The transition function method itself can be used
446as an independent image method.  However, we do not recommend to use
447this method in general cases, even though it may work well for
448approximate reachability analysis.  The implementation of the
449transition function method is basically for experimental purposes.
450
451** Usage:
452    set image_method hybrid
453    set image_method tfm
454
455Also refer to: print_hybrid_options and print_tfm_options
456
457
4582. Guided Search for Reachability Analysis
459------------------------------------------
460VIS-1.4 introduces the use of hints to guide the exploration of the
461state space.  This may result in orders-of-magnitude reductions in
462time and space requirements.  Good hints can often be found with the
463help of simple heuristics by someone who understands the circuit well
464enough to devise simulation stimuli or verification properties for it.
465Hints are applied by constraining the transition relation of the
466system to be verified.  They specify possible values for (subsets of)
467the primary inputs and state variables.  The constrained traversal of
468the state space may proceed much faster than the standard
469breadth-first search, because the traversal with hints is designed to
470produce smaller BDDs.  Once all states reachable following the hints
471have been visited, the system is unconstrained and reachability
472analysis proceeds on the original system.  Given enough resources, the
473algorithm will therefore search all reachable states, unless a state
474that violates the invariant is found.  See: K. Ravi, F. Somenzi,
475"Hints to accelerate Symbolic Traversal", Correct Hardware Design and
476Verification Methods (CHARME), pages 250-264, 1999.
477
478** Usage:
479    compute_reach -g <HintsFileName> : guided symbolic state space
480                                       traverse
481    check_invariant -g <HintsFileName> : guided search for invariant
482                                         checking
483
484The file HintsFileName contains a series of hints.  A hint is a
485formula that does not contain any temporal operators, so hints_file
486has the same syntax as a file of invariants used for check_invariant.
487
488Also refer to: model_check -g <HintsFileName>
489
490
4913. Guided Search for CTL Model Checking
492---------------------------------------
493Guided Search for CTL is an extension of Guided Search for
494reachability.  It works much along the same lines, and has the same
495benefits.  There are a few differences.  First, for greatest fixpoints
496(EG, AU, and AF), it uses overapproximations of the transition
497relation, instead of underapproximations.  Second, there is a
498distinction between local and global hints.  Local hints are the
499default.  They can be used for any kind of CTL formula, and will apply
500all hints to a subformula before moving up in the parse tree.  Global
501hints are only applicable to ACTL and ECTL formulae, and evaluate the
502entire formula once for every hint.  See: R. Bloem, K. Ravi, and
503F. Somenzi, "Symbolic Guided Search for CTL Model Checking",
504Proceedings of the Design Automation Conference (DAC), pages 29-34,
5052000.
506
507** usage:
508    model_check -g HintsFileName : perform model check guided by the
509                                   hints specified in HintsFileName
510 
511Also refer to: compute_reach -g <HintsFileName>
512               check_invariant -g <HintsFileName>
513
514
5154. Least Fix-point Machine-By-Machine Approximate FSM Traversal (LMBM)
516----------------------------------------------------------------------
517The knowledge of the reachable states of a sequential circuit can
518dramatically speed up optimization and model checking.  Since exact
519reachability may be intractable, approximate techniques are often
520preferable.  Least Fix-point MBM (LMBM) method is such a technique.
521It is as efficient as MBM, but provably more accurate.  LMBM can
522compute RFBF-quality approximations for all the large ISCAS-89
523benchmark circuit in a total of less than 9000 seconds.  For more
524information, see: I.-H. Moon, J. Kukula, T. Shiple, F. Somenzi, "Least
525Fixpoint Approximation for Reachability Analysis," International
526Conference on Computer-Aided Design (ICCAD), pages 41-44, 1999.
527
528** Usage:
529    set ardc_traversal_method 4: LMBM(least fix-point MBM, default)
530                                 is selected for ARDC
531    set ardc_traversal_method 5: TLMBM(combination of LMBM and TFBF)
532                                 is selected for ARDC
533    model_check -D 3           : model checking with ARDCs
534    compute_reach -A 2         : compute over-approximate reachable
535                                 states
536    compute_reach -D           : compute exact reachable states with
537                                 the help of ARDCs
538    check_invariant -D         : check invariants with the help of
539                                 ARDCs
540    synthesize_network -r 3    : synthesize sequential network
541                                 with ARDCs
542             
543Also refer to:  print_ardc_options
544
545
5465. Iterative Abstraction-Based Model Checking (IMC)
547---------------------------------------------------
548VIS-1.4 introduces an automatic abstraction/refinement algorithm for
549symbolic CTL model checking.  This algorithm supports full CTL
550language without fairness constraints.  The algorithm begins with
551initial upper- and/or lower-bound approximations that include some
552exact sub-transition relations of a determined set of latches for a
553given CTL formula.  As long as a conclusive verification decision
554can't be reached due to potentially false positives and negatives, the
555system is refined.  Two refinement methods are implemented: Latch Name
556Sorting and Latch Affinity Scheduling.  For more information, See:
557J.-Y. Jang, I.-H. Moon, G.D. Hachtel, "Iterative Abstraction-based CTL
558Model Checking," Design Automation and Test in Europe (DATE), pages
559502-507, 2000.  IMC supersedes the AMC package, which may disappear in
560future releases.
561
562** Usage:
563    iterative_model_check -i 8 : iterative model checking with
564                                 incremental refinement step set
565                                 to 8 latches
566    iterative_model_check -r 0 : iterative model checking using
567                                 Latch Name Sorting refinement
568                                 scheduling     
569    iterative_model_check -g 1 : iterative model checking using
570                                 Positive Operational Graph only
571
572Also refer to: model_check, approximate_model_check,
573incremental_ctl_verification
574
575
5766. Lazy Sifting
577---------------
578Lazy sifting is a new variable reordering option that is specifically
579designed for sequential verification with the transition relation
580method (i.e., IWLS95 in VIS).  Lazy sifting groups together
581corresponding present state and next state variables only when it
582expects the grouping to be beneficial.  See: H. Higuchi and
583F. Somenzi, "Lazy Group Sifting for Efficient Symbolic State Traversal
584of FSMs," Proceedings of the International Conference on
585Computer-Aided Design (ICCAD), pages 45-49, 1999.
586
587** Usage:
588   dynamic_var_ordering -e lazy_sift
589
590
5917. SPFD-based placement and logic optimization
592----------------------------------------------
593This is an algorithm based on Sets of Pairs of Functions to be
594Distinguished (SPFDs) that combines logic and placement optimization
595of combinational circuits mapped to LUT-based Field-Programmable Gate
596Arrays to improve circuit area and speed.  The flexibilities in the
597circuit are represented by SPFDs.  The package contains two commands:
598spfd_pilo - perform SPFD-based placement-independent logic optimization;
599and spfd_pdlo - simultaneous placement and logic optimization.
600
601spfd_pilo performs SPFD-based wire and node removal/replacement and
602reprogramming of combinational circuits mapped to LUT-based FPGAs to
603reduce the number of wires and nodes in the circuit.  Instead of
604computing the flexibilities for every node in the network at once, the
605algorithm computes the flexibilities for one `cluster' at a time.
606Working with clusters allows us to avoid the BDD explosion problem and
607hence handle large circuits.  The SPFDs are computed for the cluster
608and the cluster nodes are reprogrammed based on the flexibility
609derived.  Switching activity (computed via simulation of user specified bit
610vectors or randomly generated bit vectors) is used to drive the choice
611of alternate function to be implemented at the node, in such a way that
612the total switching activity in the circuit is minimized. In the absence
613of bit vectors, an arbitrary implementation for a node is chosen from
614the bounds represented by SPFDs.
615
616The command spfd_pdlo implements a technique that tightly links the
617logic and placement optimization steps.  The algorithm is based on
618simulated annealing.  Two types of moves (directed towards global
619reduction in the cost function of total wire length), are performed:
620(1) wire removal/replacement, and (2) swapping of a pair of blocks in
621the FPGA.  Feedback from placement is valuable in making informed
622choice of a target wire during logic optimization moves.  This command
623produces a placement file which is used by VPR for routing. spfd_pdlo
624can be used only if VIS is linked with VPR 4.22, an
625FPGA place and route tool from the University of Toronto
626(http://www.eecg.toronto.edu/~vaughn/vpr/vpr.html). VPack, a tool to
627convert circuits (mapped to FPGA blocks) in .BLIF format to the .net
628format (used by VPR), is also needed.
629
630Please contact Balakrishna Kumthekar (kumtheka@avanticorp.com) for details
631on integrating VPR with VIS.
632
633See: B. Kumthekar and F. Somenzi, "Power and Delay Reduction via
634Simultaneous Logic and Placement Optimization in FPGAs," Design
635Automation and Test in Europe (DATE), pages 202-207, 2000.
636
637** usage:
638     spfd_pilo -D <depth> : sets the cluster depth for SPFD
639                            computation.
640     spfd_pilo -f <file>  : use simulation vectors from specified
641                            file. These vectors are used to compute
642                            switching activity of nodes in the circuit.
643     spfd_pilo -S <method-number> : selects one of several methods to
644                            choose the node to be optimized.
645     spfd_pilo -m <method-number> : selects the heuristic to use in
646                            optimizing a selected node.
647
648     See 'help spfd_pilo' and 'help spfd_pdlo' for various options.
649
6508. Truesim
651----------
652Simulates a network with a set of input vectors. Before calling this
653command, the user should create a partition (using the command
654build_partition_mdds). The simulation vectors can be provided by the
655user (using -f vectors_file), or generated randomly. When -d option is
656used, it performs event-driven true delay simulation. The fanout count
657of the nodes is used as an estimate for the node delay. Primary inputs
658are assumed to have arrival times of zero.
659
6609. Arithmetic Functions with extended double precision (EPD)
661------------------------------------------------------------
662This is an arithmetic function package for extended double precision
663format floating-point numbers.  It supports the IEEE-754 double
664(64-bit) precision floating-point number format: both the big_endian
665and the little_endian.  The range is from 2.2631E-4932 to
6661.1897E+4932.  This package is used internally to provide fast and
667accurate counting of the states in large FSMs like those encountered
668in approximate reachability analysis.
669
67010. New version of the CUDD package.
671-----------------------------------
672VIS-1.4 includes CUDD 2.3.1.  Compared to the version that was
673included in VIS-1.3, the new version contains a number of bug fixes
674and several new functions.
675
676* Miscellaneous
677---------------
678
679** One bug in the CAL package has been fixed.  It affected platforms without
680the valloc function.
681
682** Changes in supported platforms.  Support for SunOS 5.8 (Solaris
6832.8) on the Intel x86 platform has been added.  Ultrix and SunOs 4 are
684no longer supported.
685
686** Change of Verbosity level for debugging in model_check
687Debugging refers to the printing of an error-trace when a formula
688fails.  The new debug levels are:
689-d0: no debugging (the old -d0)
690-d1: minimal debugging, with less verbosity than the old -d1 had
691-d2: minimal debugging with more verbosity (the old -d1)
692-d3: recursive debugging (the old -d2)
693-d4: interactive debugging (the old -d3)
694
695** Early termination in Model Checking.  In limited cases, VIS will
696terminate a model checking run before reaching a fixpoint.  This may
697lead to a speedup.
698
699** The set of fair states is not computed of there are no fairness
700constraints.  This may lead to a speedup of the model_check command.
701
702** Perl Script for pretty printing counter-examples.  The Perl script
703visdbgpp, contributed by Toshi Isogai, can be run on counterexamples
704produced by vis to improve their readability.  In particular, the
705script collects the bits of vectors and displays them on a single
706line.
707
708** Counterexample generation.  The states on an error trace now lie
709closer together, which means that, on average, fewer signal
710transitions will occur.
711
712** Variable reordering.  In flatten_hierarchy In VIS-1.4, variable
713reordering is invoked automatically during flatten_hierarchy.
714
715** Changes of passing BDD cube arguments in VIS to CUDD.  Some
716arguments in the CUDD functions are BDD cubes that are generated by
717the conjunctions of BDD variables on demand.  VIS-1.4 pre-builds some
718BDD cubes that do not change, such as for present state variables,
719next state variables, and primary input variables.  This speeds up
720significantly large runs, especially for approximate reachability
721analysis.
722
723
724============================================================
725
726Version 1.3
727
728* Introduction
729
730Release 1.3 of VIS improves VIS 1.2 in the following areas:
731
732** Approximate Reachability Don't Cares (ARDCs)
733** High Density Reachability Analysis.
734** On-the-Fly Invariant Checking.
735** Seeding Reachability Analysis via Simulation
736** Forward Model Checking
737** Abstraction-refinement based Incremental CTL Verification
738** Synthesis
739** State Transition Graph Restructuring for Low Power
740** Miscellaneous
741
742* Approximate Reachability Don't Cares (ARDCs)
743
744VIS-1.3 includes the use of ARDCs in model checking and reachability
745analysis. The power of using reachable states as a care set (RDCs) is
746well known; however, computing reachable states exactly is intractable
747in many large designs.  ARDCs are an overapproximation of the
748reachable states, which are then used as the care set.  Computing
749ARDCs is much cheaper than computing RDCs while their effectiveness in
750speeding up model checking is comparable to that of RDCs.  Therefore,
751ARDCs are good for large designs, especially those in which exact
752reachability analysis is intractable.  See: I.-H. Moon, J.-Y. Jang,
753G. D. Hachtel, F. Somenzi, "Approximate reachability don't cares for
754CTL model checking", ICCAD'98.
755
756** Usage:
757           model_check -D 3    : model checking with ARDCs
758           compute_reach -A 2  : compute over-approximate reachable
759                                 states
760           compute_reach -D    : compute exact reachable states with
761                                 the help of ARDCs
762           check_invariant -D  : check invariants with the help of
763                                 ARDCs
764           synthesize_network -r 3 : synthesize sequential network
765                                     with ARDCs
766
767Also refer to: print_ardc_options
768
769
770* High Density Reachability Analysis (HD)
771
772HD is an alternate approach to performing exact reachability
773analysis.  Using BDD subsetting techniques, the HD method tries to keep
774the sizes of the BDDs small during the traversal.  This is intended to
775keep the memory occupation under control as well as make the traversal
776more efficient by manipulating smaller BDDs.
777
778On large circuits, for which the default (breadth-first search) method
779does not complete, HD is likely to find many more reachable states.
780This is useful in invariant checking.
781For mid-size circuits, HD is sometimes faster in completing
782reachability analysis, but for smaller circuits, HD may result in too
783much overhead.  It is recommended to use this option when the default
784method for reachability analysis fails (runs out of memory or takes
785very long).  Refer to Ravi and Somenzi, "High-density reachability
786analysis", ICCAD'95.
787
788HD analysis only works with the CUDD package.
789 
790** Usage:
791           compute_reach -A 1: reachability analysis with HD approach.
792
793Also refer to: print_hd_options
794
795
796* On-the-Fly Invariant Checking
797
798Checking invariants is done by performing reachability analysis and
799checking if all invariants hold in the reachable states.  VIS-1.3
800does invariant checking during reachability computation (on-the-fly
801verification).  Invariants that fail are reported early, along with the
802counter examples if requested.
803
804Since reachability analysis can be expensive, one may use HD in
805invariant checking.  For circuits on which the default reachability
806analysis runs out of resources, HD will typically explore more
807reachable states, and more invariants may prove false.  However, the
808counter examples provided by using HD may not be of shortest length.
809
810HD invariant checking only works with the CUDD package.
811
812** Usage:
813           check_invariant -A 1 : check_invariant where HD is used for
814                                  reachability analysis
815
816One may also start with an overapproximation of the reachable
817states.  In this case, if all invariants hold on the overapproximation,
818verification is successfully completed.  If not, the algorithm will
819compute the exact reachable states as before, and check the
820invariants that failed with the overapproximation.
821
822** Usage:
823           check_invariant -A 2 : check_invariant where over
824                                  approximation is used for reachability
825                                  analysis.
826
827* Seeding Reachability Analysis via Simulation
828
829A new option rch_simulate can be used to use simulation to augment the
830set of initial states for reachability analysis. The value of the
831variable is the number of random input vectors that are simulated. The
832states reached in this way are considered as initial
833states. Augmenting the set of initial states may sometimes lead to
834faster reachability analysis, or may sometimes lead to better
835underapproximations, when reachability analysis is not carried out to
836completion. The commands affected by this option are compute_reach and
837check_invariant.
838
839** Usage:
840           set rch_simulate n : simulate n vectors prior to
841                                reachability analysis
842
843
844* Forward Model Checking
845
846VIS-1.3 includes the capability of forward model checking based on
847H. Iwashita, T. Nakata, F. Hirose, "CTL model checking based on
848forward state traversal", ICCAD'96.  Standard "backward" CTL model
849checking uses only preimage computations.  Forward model checking tries
850to use image computations in place of preimage computations as much as
851possible, because they are typically faster.
852According to our experiments, forward model checking gives drastic
853performance improvement in many designs, but we have also seen many
854cases in which forward model checking does much worse.  Performance
855depends on the design.
856
857** Usage:
858           model_check -F  : model checking based on forward traversal
859
860
861* Incremental CTL Verification
862
863The command "incremental_ctl_verification" (aliased to "icv")
864performs verification of CTL formulas following the incremental
865paradigm described in A. Pardo, G. Hachtel, "Incremental CTL model
866checking using BDD subsetting", DAC'98.  The algorithm starts with an
867initial simple approximation of the verification and then proceeds at
868refining the different evaluations until the formula can be proved
869conclusively.  The approximation technique currently adopted makes use
870of BDD approximation techniques.  As implemented in release 1.3,
871incremental_ctl_verification supports fairness constraints, but tends
872to be less efficient than model_check when they are specified.
873
874Incremental verification works only with the CUDD package.
875
876** Usage:
877           incremental_ctl_verification [options] ctl_file
878
879
880* Synthesis
881
882VIS 1.3 includes a new command "synthesize_network" (aliased to
883"synth") to transform both combinational and sequential circuits into
884multi-level boolean networks using symbolic factorization based on
885Zero-suppressed BDDs (ZDDs).  In the case of sequential circuits, only
886the combinational part of the circuit is synthesized: state encoding
887is not altered.  The emphasis of this algorithm is on the reduction of
888the number of literals in the factored form of the network.  The final
889multi-level circuit can be obtained in either the BLIF format or the
890equation format.  Designs described in BLIF or BLIF-MV format can be
891used as an input to this command.  However, multiple valued variables
892are not supported.  Hence, signals in the designs described in BLIF-MV
893need to be restricted to binary values.
894
895Synthesis can be used only when VIS is linked with the CUDD package.
896
897** Usage:
898           synthesize_network [options]
899
900* STG Restructuring for Low Power
901
902VIS-1.3 includes a new command "restruct_fsm".  This command
903implements a State Transition Graph (STG) restructuring algorithm
904that exploits the existence of equivalent states to decrease power
905dissipation, not necessarily by collapsing the equivalence states, but
906by redirecting transitions in the graph.  This algorithm is based on
907the monolithic transition relation.  The complexity of the algorithm
908in general increases with an increase in the size of the state
909transition graph, which depends on the number of state variables and
910primary inputs.  The algorithm can handle circuits described in both
911BLIF and BLIF-MV formats.  However, multi-valued variables are not
912supported.  Also, the final synthesized circuit (network implementation
913of the restructured STG) is available only in BLIF format.  The
914sequential circuit should have a single initial state.  For more
915details see, B. Kumthekar, I.-H. Moon, F. Somenzi, "A Symbolic
916Algorithm for Low-Power Sequential Synthesis", ISLPED 97.
917
918STG restructuring works only with the CUDD package.
919
920** Usage:
921           restruct_fsm [options]
922
923* Miscellaneous
924
925** New versions of CUDD and CAL packages.
926VIS-1.3 includes CUDD 2.3.0 and CAL 2.0.1.  Compared to the versions
927that were included in VIS-1.2, the new packages have better
928performance and improved statistics reporting.
929
930** Changes in configure
931Configure now defaults to using 32-bit pointers on DEC Alpha machines. 
932To use 64-bit pointers, invoke "configure" with "--enable-64."
933
934** gmake check
935"gmake check" now consistently runs the local executable using the
936examples in the master source directory.  Previously, there were
937different versions for local-area and central-area checks.
938
939** Native Compiler.
940The configuration scripts now try to use the native C compiler (cc) by
941default.  The use of gcc can be forced by running configure with the
942option --enable-gcc.  On AIX and SunOS, however, only gcc is
943supported.
944
945As a result, the following configuration options have been removed
946
947    --with-comp-mode=solaris
948    --with-comp-mode=mips
949    --with-comp-mode=alpha32
950    --with-comp-mode=alpha64
951
952Configure now defaults to using 32-bit pointers on DEC Alpha machines. 
953To use 64-bit pointers, invoke "configure" with "--enable-64."
954
955** Changes in supported platforms.
956VIS-1.3 has been tested under IRIX 5.3 with both cc and gcc.
957VIS-1.3 has been tested under HP-UX with cc. (Previously only gcc was
958supported.)
959VIS-1.3 linked with the CAL BDD package currently does not work under
960CYGWIN32.  When the problems are fixed, we shall issue a patch.
961
962** Uniformity across platforms.
963VIS-1.3 provides enhanced architecture independence.  For the commands
964model_check, approximate_model_check, compute_reach,
965incremental_ctl_verification, check_invariant, and lang_empty, the runs
966will be exactly the same on every platform with the same memory limits.
967Previously, invocations of reordering, and hence BDD sizes could differ
968from platform to platform.
969
970** Changes to static_order.
971The static_order command has changed substantially.  For combinational
972circuits, VIS-1.2 and earlier releases effectively generated random
973orders regardless of the method specified by the user.  (Sequential
974circuits did not have this problem.) The randomness of the orders was
975due to a bug that has been fixed in VIS-1.3.  For all
976circuits---combinational and sequential---the default ordering method
977is a new algorithm called "interleave."  The new default method is
978substantially more memory efficient than the previous default method
979(merge_left).  The quality of the resulting orders is comparable.
980
981** New -v option for dynamic_var_ordering.
982The option -v 1 can be specified to cause VIS to write a one-line
983message whenever dynamic reordering is executed.  The message reports
984the reduction in BDD or ZDD size, and on the time taken by reordering.
985This option is only effective with CUDD.
986
987** New -i option for comb_verify and seq_verify.
988It is now possible to print statistics on BDD usage and performance
989when running combinational or sequential verification.  This is done
990by specifying the -i option for comb_verify and seq_verify.  It is
991important to notice that these two commands use a local BDD manager,
992which is destroyed before control is returned to the user.  It is not
993therefore possible to use print_bdd_stats to inspect the statistics of
994the BDD package when invoking either of the two commands.
995
996** Default method for build_partition_mdds changed to inout.
997The default method has been changed to inout, because this has been
998found to produce better results than frontier in many cases.  The
999frontier method can build the partition MDDs in more cases than the
1000inout method; the latter, however, tends to give better performance
1001during model checking.
1002
1003** set ctl_change_bracket [yes/no]
1004VIS-1.3 includes this set command option for the CTL parser.  VL2MV
1005automatically converts "[]" to "<>" in node names, therefore the CTL
1006parser does the same thing.  However, in some cases a user does not
1007want to change bracket type in the CTL formulas.  This can be
1008accomplished by setting this set command option to "no."  The default
1009is "yes". The commands affected are check_invariant, model_check,
1010approximate_model_check, and incremental_ctl_verification.
1011
1012** Printing time for model checking
1013VIS-1.3 includes printing time for model checking.  If verbosity is set on,
1014then the model checking time for both each formula and total will be printed
1015out.
1016
1017** Incremental reachability analysis and invariant checking.
1018In VIS-1.3 it is possible to perform reachability analysis
1019incrementally.  The -d option of compute_reach specifies how many
1020steps (image computations) should be performed at most before
1021returning control to the user.  If compute_reach is invoked more than
1022once with the -d option, each time reachability analysis starts from
1023the previous result.  If check_invariant is invoked after
1024compute_reach has been invoked with the -d option, the partial
1025reachability results are used to speed up verification.
1026
1027** Completeness and determinism check in flatten_hierarchy
1028The check for completeness and determinism performed by
1029flatten_hierarchy that was previously optional is now always
1030performed. The -b option to flatten_hierarchy and init_verify has no
1031effect in VIS-1.3 and is retained for compatibility with existing
1032scripts. It may disappear in future releases. Users of VIS-1.3 will
1033observe modest increases in the time taken to flatten the
1034hierarchy.
1035
1036
1037Version 1.2
1038
1039* Introduction
1040
1041** Improvements
1042
1043*** Over 10x performance improvement in model checking for many  examples
1044*** extended CTL syntax
1045*** better access to the BDD parameters and statistics
1046*** enhanced user interface
1047*** improved portability and flexibility of configuration
1048
1049** New verification algorithms
1050
1051*** approximate_model_check: model checking of ACTL formulae for systems
1052    that are too large for model_check
1053*** res_verify: residue based verification of arithmetic circuits
1054
1055* Performance improvement in model checking
1056
1057** We have changed image computation (the underlying operation of
1058   model checking) to make the best use of don't care sets. The don't
1059   cares arise from unreachable states, and using them appropriately
1060   reduces the BDD sizes significantly, leading to improved
1061   performance of model checking. In addition, we have fixed a
1062   performance bug that caused repeated computation of simplified
1063   transition relations. We performed a performance comparison with
1064   VIS 1.1 on a set of examples, and on some cases we observed more
1065   than 30x performance improvement. In fact, on some examples VIS 1.2
1066   could finish model checking in about 26 secs whereas VIS 1.1 took
1067   about 2400 secs.
1068
1069** The model checking runs that use don't cares (-D option different
1070   from 0) are those that benefit the most from the changes in VIS
1071   1.2. In general it is not trivial to tell whether -D 1 or -D 0 will
1072   produce the faster CPU time. An empirical approach consists of
1073   running "compute_reach -t 300" (reachability for 5
1074   minutes). Depending upon the progress in reachable state
1075   computation, one can then invoke model checking with -D 0 or -D 1.
1076
1077* Approximate Model Checking
1078
1079** VIS 1.2 includes a new command approximate_model_check, a model
1080   checker that performs ACTL model checking on an abstracted and
1081   flattened network.  The command is designed to tackle the state
1082   explosion problem we encounter when dealing with large and complex
1083   circuits. Based on the initial size of the group (of latches), the
1084   command constructs an over- or under-approximation of the
1085   transition relation of the system. These approximations may not
1086   contain every detail of the exact system. However they may contain
1087   enough information to determine whether the formula is positive or
1088   negative.  Starting from an initial coarse approximation, the
1089   command makes its effort to prove whether the given ACTL formula is
1090   true or false. When the procedure fails to prove correctness of the
1091   formula with initial approximations, it automatically refines the
1092   approximations. It repeats the process until the algorithm produces
1093   a reliable result or the available resources are exhausted.  For
1094   detailed description, refer to the relevant manual page ("help
1095   approximate_model_check from" the VIS shell).
1096
1097** approximate_model_check is faster than model_check for some of the
1098   VIS 1.2 distribution examples. However, significant improvements
1099   over the exact computation can be seen for even larger examples
1100   such as s15850. The current version of the code does not perform
1101   any refinements.  The refinement techniques similar to the "machine
1102   by machine" and "frame by frame" may be implemented in future
1103   version. Furthermore, more aggressive reduction of the initial
1104   states can be performed while proving whether the ACTL formula is
1105   positive. The reduction of the initial states are made for each
1106   level of the lattice of approximations in this version.
1107
1108** The current version includes two distinct "grouping method". More
1109   experiments are required to determine better grouping method(s).
1110
1111** The current version only supports ACTL formulae.
1112
1113* Residue Based Verification
1114
1115** VIS 1.2 includes a new command "res_verify" for combinational
1116   verification based on residue arithmetic. Residue-based
1117   verification is especially suited to multipliers and other
1118   arithmetic circuits. See below, however, for a discussion of the
1119   application of "res_verify" to other circuits. This command is only
1120   available if VIS has been linked with the cu library (default).
1121
1122** The command res_verify takes two circuits (specification and
1123   implementation) whose equivalence is to be established, and an
1124   order for the outputs. The order for the outputs allows res_verify
1125   to interpret the output vectors as integers. Based on this
1126   interpretation, res_verify applies the Chinese remainder theorem to
1127   the equivalence verification: the specification and the
1128   implementation are equivalent if, for a suitable set of relatively
1129   prime numbers, the residues of their outputs are equivalent. The
1130   residues are computed by composing the two circuits into a function
1131   representing the residue computation.
1132
1133** res_verify allows the user to specify what pairs of outputs of the
1134   circuits should be compared directly by building their BDDs,
1135   instead of computing residues for them. The -d <n> option controls
1136   this feature; n pairs of outputs, starting from the least
1137   significant bits of the output vectors, are verified directly if -d
1138   n is specified.
1139
1140** As a special case, the user can specify -d all. This causes
1141   res_verify to directly verify all the output pairs, effectively
1142   foregoing residue verification. This can be useful for
1143   non-arithmetic circuits that are not suited to residue
1144   verification. In this case res_verify works similarly to
1145   comb_verify, with a significant exception: res_verify verifies one
1146   output at the time. This often translates into reduced memory
1147   requirements and CPU times.
1148
1149** res_verify can be applied to pairs of sequential circuits with the
1150   same state encoding. Several options and VIS variables control the
1151   detailed behavior of the command. Refer to the on-line
1152   documentation for the details (help res_verify).
1153
1154
1155* Extended CTL Syntax
1156
1157** Users can now write CTL fomulae using vector notation. Vector
1158   variables have the form of var[i:j] and each bit can be written as
1159   either var<i> or var[i]. For instance, the following formulae are
1160   valid.
1161
1162   counter[3:0] = 10       
1163   counter[3:0] = b1010
1164   counter[3:0] = {1,2,10}
1165
1166   The formula in the last line is true if counter has one of the listed
1167   values.
1168
1169** Macros can be defined and used in CTL formulae to stand for subformulae.
1170   For instance:
1171
1172     \define VALID_INPUT (a[3:0]=0 -> b=1)
1173
1174   defines the macro VALID_INPUT, which can be later used in a formula
1175   like this:
1176
1177     AG(start=1 * \VALID_INPUT -> AF(res[7:0]=b10101010));
1178
1179** The CTL parser allows users to write the following formulae:
1180
1181     var1 == var2
1182     var1[i:j] == var2[k:l]
1183
1184   The first formula is equivalent to (var1=1) * (var2=1) + (var1=0) *
1185   (var2=0) and currently is allowed only in the boolean domain.  (It
1186   cannot be used for variables of enumerated types.)  The second formula
1187   can be used if the lengths of two vectors match.
1188
1189** AX:n(f) is allowed as a shorthand for AX(AX(...AX(f)...)), where n
1190   is the number of invocations of AX. EX:n(f) is defined similarly.
1191
1192
1193* BDD manipulation
1194
1195** VIS 1.2 incorporates Release 2.1.1 of CUDD and an improved version of
1196   CAL. Improvements specific to CUDD and relevant to VIS are:
1197
1198** All reordering methods preserve variable groups. Variable groups are
1199   created by VIS to keep corresponding present and next state variables
1200   adjacent. In VIS 1.1 only method "sift" retained the variable groups.
1201
1202** CUDD determines the maximum size of the computed table based on the
1203   amount of main memory available. On systems where getrlimit is
1204   available, the datasize limit is used to determine how much memory
1205   is available. CUDD allows the computed table to grow up to one
1206   fourth of that amount. This feature allows VIS to self-calibrate
1207   for optimum performance. The computed table will not necessarily
1208   grow to its maximum value, and VIS is not guaranteed to stay within
1209   the memory bound returned by getrlimit. If the datasize limit is
1210   not set, if getrlimit is not available, or if it is available but
1211   does not know about datasize, then a suitable default value is used
1212   instead. The default value is normally 16MB. This value can be
1213   changed at configuration time. Even a value as low as 16MB gives a
1214   reasonably sized computed table for small-medium runs. However, for
1215   large runs--hundreds of MB--the ability to set the memory limit may
1216   produce much faster execution. The maximum computed table size can
1217   be set also from within VIS with set_bdd_parameters.
1218
1219** CUDD now provides access to the package parameters and statistics
1220   via the commands bdd_print_stats and set_bdd_parameters. The
1221   parameters that can be set control the sizing of CUDD's main data
1222   structures (unique table and computed table) and many aspects of
1223   the variable reordering algorithms. The parameters reported refer
1224   to memory occupation, computed table (cache) performance, and
1225   variable reordering.
1226
1227** It is now possible to impose a limit on the number of variable
1228   swaps performed during reordering.
1229
1230
1231* User Interface
1232
1233** New VIS command "set_bdd_parameters". 
1234
1235   The command "print_bdd_stats" prints two sets of data from the
1236   underlying BDD package, parameters and statistics. The parameters
1237   can be modified as follows. By using the "set" command, set the
1238   value of a variable whose prefix is "BDD." and whose suffix is
1239   exactly the name seen in the output of the command
1240   "print_bdd_stats", for example:
1241
1242     vis> set "BDD.Garbage collection enabled" no
1243
1244   Then, the command "set_bdd_parameters" reprograms the underlying BDD
1245   core based on the values of the variables of this type.
1246
1247** Readline Library.
1248
1249   The Readline library is a GNU package that provides command line
1250   editing, command history, and file name completion capabilities. If
1251   the system where VIS is built has this library and it is installed
1252   so that the linker can use it, the configure script will detect
1253   this situation and the executable will be linked with
1254   libreadline.a.
1255
1256** Variable Interpolation.
1257
1258   The VIS shell now allows variable interpolation. For instance, typing
1259
1260    vis> echo $open_path
1261
1262   causes vis to echo the current value of open_path. Typing
1263
1264    vis> set open_path $open_path:/some/path
1265
1266   will append /some/path to open_path. Variable interpolation can be
1267   used also to exchange parameters with scripts. This allows reliable
1268   parameter passing even when "source" is called with options.
1269
1270** PAGER
1271
1272   If the PAGER environment variable is set, VIS uses it to choose the
1273   program used to display the help pages. If PAGER is not set, VIS
1274   uses 'more.'
1275
1276** File Buffering.
1277
1278   The output of VIS when run in batch mode is now line buffered on
1279   systems that provide setvbuf. This makes it more convenient to
1280   observe the evolution of long-running jobs.
1281
1282* Portability and Configuration
1283
1284** VIS 1.2 runs on two new platforms: IBM RS6000 running AIX and Intel
1285   Pentium running Windows95 with Gnu-Win32. The Gnu-Win32 environment
1286   (http://www.cygnus.com/misc/gnu-win32/) is a freely available GNU
1287   environment for Windows 95 and Windows NT.
1288
1289** This release of VIS has been tested with some native compilers
1290   (Ultrix, Solaris, Digital Unix). In particular, when building with
1291   the native compiler on a DEC Alpha running Digital Unix, the option
1292   is provided to compile with 32 bit pointers. Please see the README
1293   file for specific instructions on how to compile with the different
1294   native compilers.
1295
1296** The GLU library now provides portable functions for random number
1297   generation and sorting that help make results reproducible across
1298   different platforms.
1299
1300** The GLU library now provides a function to read the available
1301   memory (based on getrlimit). This function is currently used by the
1302   CUDD package to choose the optimal size of data structures. For
1303   systems without getrlimit a suitable default is provided and can be
1304   changed at configuration time.
1305
1306
1307Version 1.1
1308
1309* Introduction
1310
1311** Improvements over 1.0
1312
1313*** multiple BDD packages
1314*** more synthesis capability
1315*** hierarchy restructuring
1316*** new methods for partitioning
1317*** automatic reduction during model checking
1318*** support for multi-phase clocking and transparent latches
1319*** support for invoking standard scripts
1320*** support for graphically viewing simulation output
1321
1322  These significantly improve VIS's performance in terms of computer
1323  time, memory usage, and ability to complete on larger designs.
1324  Further, additional capability for synthesis is provided.
1325
1326  One particular example of the improved performance of VIS 1.1 is the
1327  first (to our knowledge) reported exact state space traversal of
1328  benchmark s5378. It was run with the cu BDD package on an Alpha
1329  300MHz (using 32 bit pointers). The datasize limit was set at
1330  1GB. The process grew to about 440MB. Dynamic reordering was enabled
1331  all the time and occurred more than 50 times. The orginal ISCAS89
1332  circuit was used, which has 179 latches.
1333
1334*** Multiple BDD packages
1335
1336    We have added the capability to run VIS with three different BDD
1337    packages, cu - from University of Colorado, cal - from UC Berkeley
1338    and cmu - from Carnegie Mellon University. Further details are in
1339    the section "BDD Packages" below.
1340
1341*** Synthesis
1342
1343    VIS synthesis is represented by a number of commands, write_blif,
1344    read_blif, collapse_child, and decompose_child. These allow the
1345    user to manipulate the hierarchy and to write blif files to SIS
1346    and then later read in an optimized file. Each of these commands
1347    can be executed on sub-nodes or sub-trees of the
1348    hierarchy. Details about these commands are in the section
1349    "Collapsing and decomposing a hierarchy" and "Reading and writing
1350    blif files" below.
1351
1352*** Partitioning
1353
1354    Partitioning in VIS is used in a number of places: simulation,
1355    model checking, computing the set of reached states, etc.  Recall
1356    that the VIS data structure is simply a set of tables with outputs
1357    (signals) which can be inputs to other tables. There are also
1358    primary input signals and inputs from latches. Some signals are
1359    primary outputs and/or inputs to latches. A partition is simply a
1360    subset of nodes (signals) which are to be preserved, the remaining
1361    are to be eliminated. Of course, primary outputs and inputs to
1362    latches cannot be eliminated. We provide some new partitioning
1363    methods as described below (in the section "Creating partitions of
1364    the network").
1365
1366    In many cases, a formula to be model checked does not depend on
1367    all of the signals in the design. In such cases, the design can be
1368    reduced to include only signals in the transitive fan-in of the
1369    latches mentioned in the CTL formula plus the fairness
1370    constraints. This reduction can result in vastly more efficient
1371    model checking.
1372
1373*** Multi-phase clocking
1374
1375    One question that is asked frequently is how does VIS support
1376    multi-phase clocking and transparent latches in Verilog. We
1377    provide this capability in our Verilog compiler "vl2mv" and detail
1378    this in a document that describes exactly the steps to be
1379    taken. This document is in the vis-1.1/doc directory and is called
1380    two_phase.ps.
1381
1382*** Standard scripts
1383
1384    Standard scripts have been provided which should help the new user
1385    select certain options that we have determined to be good choices
1386    on a variety of examples. The scripts are divided into two
1387    categories: simple - which are recommended for small/medium
1388    examples, and robust - recommended for large examples where
1389    completion rather than compute time is the most important
1390    concern. The 10 scripts provided are summarized below in the
1391    section "Standard scripts".
1392
1393*** xsimv
1394
1395    Finally, we have included "xsimv", which provides a graphical
1396    method for viewing simulation output. This is detailed in the
1397    section "Using Xsimv".
1398
1399* Multiple BDD packages
1400
1401  We have added the capability to run VIS with three different BDD
1402  packages, cu - from University of Colorado, cal - from UC Berkeley
1403  and cmu - from Carnegie Mellon University. The commands for these
1404  respectively are vis-cu, vis-cal, and vis-cmu. The cmu package is
1405  the same as in VIS 1.0. The cu package is very strong in having a
1406  fast dynamic variable reordering capability. In addition, cu has
1407  been upgraded for the DEC alpha machines so that it uses 32 bit
1408  pointers, instead of 64 bit pointers; hence it realizes a factor of
1409  2 in memory savings on such machines. The other two packages remain
1410  to be upgraded for 32 bit pointers on the DEC alphas.  The cal
1411  package uses the BFS BDD technique and is particularly good at
1412  avoiding paging on large designs. For most problems, we recommend
1413  the cu package.
1414
1415* Reading and writing BLIF files
1416
1417  The "write_blif" command in vis-1.0 only wrote out the combinational
1418  part of an hnode (a node of the hierarchy).  Now this functionality
1419  is performed by the "write_blif -c" command. Other options have been
1420  added as well. The options are:
1421
1422  (1) write_blif -l
1423
1424      writes out the latches of the hnode as well.  Additionally, all
1425      latch IOs are made into POs in the blif file that is
1426      created. This ensures that the these nodes do not get optimized
1427      away by SIS, so that mv-latches can be re-inserted by the
1428      read_blif command in VIS.
1429
1430  (2) write_blif -c
1431
1432      same as "write_blif" of vis-1.0
1433
1434  (3) write_blif
1435
1436      writes out latches of the hnode, but does not make latch IOs
1437      into POs in the blif file. The .blif and .enc files that are
1438      generated by this command currently cannot be guaranteed to read
1439      back into VIS correctly using the read_blif command.
1440
1441  (4) write_blif -R
1442
1443      recursively writes out the entire hnode hierarchy rooted at the
1444      current hnode, to a blif file. This command opens up a direct
1445      path from Verilog to pure blif files and hence to synthesis in
1446      the SIS framework.  For this command to work, 1) all variables
1447      in the hnode hierarchy rooted at the current hnode must be
1448      binary, 2) all tables should be deterministic, and 3) there must
1449      be a unique initial state.
1450
1451* Collapsing and decomposing a hierarchy
1452
1453  If the user travels (via "cd" commands) to a particular node in the
1454  hierarchy and does a "write_blif", only the logic in the *current*
1455  node gets written out. The user might want to collapse some of the
1456  child nodes together and do synthesis in the "collapsed" node. The
1457  "collapse_child" command does just that. The usage is:
1458
1459      collapse_child <child_name>
1460
1461  and the effect is that the child node is absorbed by the parent. By
1462  successive invocations of this command, multiple nodes can be
1463  collapsed into a single node.
1464
1465  "decompose_child" is a command that effects the inverse operation of
1466  collapse_child. The user can specify components of the current node
1467  to be grouped as a separate newly created child node. The user must
1468  also specify the name of the new child. Successive invocations of
1469  "decompose_child" can be used to effect multiple
1470  decompositions. "decompose_child" provides the infra-structure for
1471  implementing and testing FSM decomposition algorithms (to appear
1472  later).
1473
1474  Together, collapse_child and decompose_child provide powerful
1475  primitives that can be used to restructure the design hierarchy.
1476
1477* Creating a flattened network for verification
1478
1479  The important change to note is the "-b" option in the
1480  "flatten_hierarchy" command.  By default this option is off,
1481  implying that the system is not checked for complete and
1482  deterministic specification. However, if the given design does not
1483  meet this criteria, model checking may produce wrong results. (Note:
1484  In VIS nondeterminism is handled by providing pseudo-inputs.
1485  Internally all the tables are deterministic and completely
1486  specified.)  Invoking this "-b" option forces the necessary
1487  checking. However this can be computationally expensive.  The best
1488  strategy is to invoke "flatten_hierarchy" with "-b" option the first
1489  time and if the check passes, use it without "-b" option in
1490  subsequent runs.
1491
1492* Creating partitions of the network
1493
1494  Three new methods for creating partitions for the "build_partition_mdds"
1495  command have been added.
1496
1497      - partial
1498
1499        This can be used to perform partitioning while forcing a
1500        user-specified set of signals (nodes) in the partition. The
1501        set of nodes to be included can either be supplied in a file,
1502        or on the command line.
1503
1504      - boundary
1505
1506        In this method, all nodes that are sub-circuit IOs are
1507        included in the partition.
1508
1509      - frontier
1510
1511        In this method (the default method), the user specifies a
1512        parameter "partition_threshold" which is used to include an
1513        intermediate variable whenever the BDD size for a node in the
1514        network increases beyond the threshold value. This method is
1515        very useful when it is not possible to create the next state
1516        functions in terms of primary inputs because of large BDD
1517        sizes. This method encompasses both "in_out" and "total"
1518        partitioning methods (corresponds to very large and 0 value of
1519        "partition_threshold", respectively). The parameter can be set
1520        by invoking the following from the VIS commandline: "set
1521        partition_threshold <integer>".
1522
1523* Reachability computation
1524
1525  A few new options to reachability computation have been added
1526  (command: compute_reach).
1527
1528
1529        -d depthValue
1530
1531           Used to perform reachability up to a certain number of
1532           steps.
1533
1534        -r threshold_value
1535
1536           Invokes dynamic reordering of variables ONCE, after the
1537           size of the reached state set crosses the threshold_value.
1538
1539* CTL Syntax
1540
1541  For Verilog compatibility, && and || are supported in addition to *
1542  (Boolean AND) and + (Boolean OR) respectively.
1543
1544* Model checking
1545
1546  The mc command, by default, now reduces the model FSM with respect
1547  to the union of all the formulas in the CTL file and uses the
1548  reachability don't cares (thus reachablilty is done first before any
1549  model checking). Also, -d 0 is the default now, i.e. no error trace
1550  is computed. The -r option has been modified and a new capability
1551  for sharing sub-formulas has been added.
1552
1553  -r
1554
1555    (This option has been modified). If this option is used, each
1556    formula is model checked individually on an FSM reduced with
1557    respect to the formula.
1558
1559  -c
1560
1561    This disables the default that sub-formulas of the formulas given
1562    in the CTL file are shared. The sharing of sub-formulas makes sure
1563    that a sub-formula in the set of all sub-formulas of the formulas
1564    in the CTL file is evaluated only once. If both -r (formula
1565    dependent FSM reduction) or "-D 1" (use reachability don't cares)
1566    are enabled, this facility is automatically disabled.  (Note that
1567    currently if the same sub-formula occurs more than once within a
1568    single formula, it may be checked twice.)
1569
1570* Standard scripts
1571
1572  There are 10 standard scripts provided (in the "share" directory),
1573  divided into two categories, simple and robust. The simple scripts
1574  work best on small/medium size examples. The robust scripts are
1575  recommended for large problems where the objective is to complete
1576  the computation without too much concern for computation time. Below
1577  are the scripts with their required arguments.  All scripts assume
1578  that a BLIV-MV file has already been read in.
1579
1580        script_generic.simple
1581        script_compute_reach.simple     
1582        script_model_check.simple foo.ctl
1583        script_fair_model_check.simple foo.fair foo.ctl
1584        script_lang_empty_check.simple foo.fair
1585
1586        script_generic.robust
1587        script_compute_reach.robust
1588        script_model_check.robust foo.ctl
1589        script_fair_model_check.robust foo.fair foo.ctl
1590        script_lang_empty_check.robust foo.fair
1591
1592  In all cases, "script_generic" is a preample to the other scripts.
1593  Generally, we recommend trying a "simple" script first, since it
1594  should be the fastest.
1595
1596* Using "xsimv"
1597
1598  Before invoking xsimv, please modify the first line of the file
1599  "xsimv" and put the complete path name for "expectk".
1600
1601  xsimv is invoked by the command
1602
1603        xsimv <sim-file>
1604
1605  where <sim-file> is a file produced by the vis command
1606
1607        simulate -n <num> -o <sim-file>
1608
1609  When xsimv executes, it comes up with a window with 4 buttons in it,
1610  GO, ReDraw, Save and Quit. At the same time it produces a file,
1611  "strk.simv", with the signal names in it. For example
1612
1613    sensor.rand_choice
1614    timer.rand_choice
1615    car_present
1616    farm_light
1617    hwy_light
1618    timer.state
1619
1620  If only a subset of these names are required the user can edit this
1621  file and comment out a line using "#". For example,
1622
1623    #sensor.rand_choice
1624    #timer.rand_choice
1625    car_present
1626    farm_light
1627    hwy_light
1628    timer.state
1629
1630  will cause the first two signals' simulation to be not displayed.
1631
1632  Pushing GO or ReDraw then produces a new window with the simulation
1633  results shown where time increases from left to right.  The signal
1634  value names not commented out are shown vertically, one for each
1635  row. The "edit strk.simv" and REDRAW sequence can be iterated.
1636
1637Version 1.0
1638
1639* Initial release
Note: See TracBrowser for help on using the repository browser.