************************************************************************* SMV 2.4b This version of SMV is based on smv 2.4. Many original routines and functions have been rewritten with a few enhencements added. I have added these functionalities for my own research purposes only. THIS IS NOT AN OFFICIAL VERSION OF SMV. I am releasing this source code in the hope that some of the features I added can help out other research efforts. For the CMU official version of SMV, please see http://www.cs.cmu.edu/~modelcheck/ NOTE: All commercial use of SMV needs to be licensed by CMU. Please contact Prof. Edmund Clarke (emc@cs.cmu.edu) for more information. Bwolen Yang School of Computer Science Carnegie Mellon University bwolen@cs.cmu.edu File Created: 7/99 Last Modified: 7/99 ************************************************************************* HISTORY ------- SMV is a model checker originally developed by Ken McMillan and have subsequently being modified by serveral researchers. In summer 1997, I began to hack BDD part of the SMV code (version 2.4) to generate BDD traces for benchmarking purposes. The more I played with the code, the more places I felt like I can improve its overall performance. Subsequently, I have built my entire Ph.D. thesis on this work. For my thesis work and related publications, please see http://www.cs.cmu.edu/~bwolen/publications.html COMPILATION ----------- gmake Create the "smv-2.4b" in the "bin" directory. gmake dep Create the dependence file for the Makefile. This step is useful if you plan to hack this package. gmake tag Create the TAG file for emacs. This step is useful if you plan to hack this package inside of emacs. gmake clean Remove all files created by this "Makefile". PLATFORM TESTED --------------- Linux -- Pentium / PPro. (Note: gcc version 2.8 or above is required.) Solaris -- Ultrasparc OPTIONS ------- Run smv without any flags will give you a list of options along with brief documentation on each option. I have automated a few options for this version of SMV. Recommended initial flags to use: -f (and -i if you have an initial variable ordering file) Performance Debugging --------------------- Add command line flat "-v 1" for initial performance debugging. "-v 2" will output a lot more information without much performance impact. "-v 3" is full verbose mode and may generally slow down the computation. If you have tough problems that you would like me to look at, please send me the model with the output using "-v 1". Memory Setting -------------- If your SMV job is the only main job that will be running on the machine, there is no need to do anything. It will set and adjust automatically. If your SMV job shares the machine with other jobs, then you can (and should) limit your memory usage by either -mem or in your shell, limit your data size. In C-shell, do % limit M e.g., if you want to limit to 900Mb, either use the SMV command line flag -mem 900 or C-shell command % limit 900M Partition Size of Transitions/Invariants: ----------------------------------------- This is set by specifying the "-partSize" flag. For no partitioning (monolitic transition relation): -partSize 0 Default value is currently set to -partSize 100k Note that the performance of model checking can vary greatly depending on the partition size. Some models run a lot faster with larger partition sizes (>= 1M). Others perferred smaller partition sizes (5K). Selecting the wrong size could mean the difference between doable and not doable. My experience has been that one of 0 (no partitioning), 5K, or 1M would work well. I choose the default of 100K as a compromise of all the test cases I have. Complex Time-Invariant Constraints ---------------------------------- If the model has complex invariant conditions, this version of SMV tries to extract macros (equivalent to SMV's "DEFINES") from these invariant. If the above recommended flags fails to complete due to insufficient memory, try setting -macro with to be larger than 1024, but not too much larger (probably no more than 5000). If this still fails (and it is running out of memory), try -noWitnessShortCircuit flag. In general, this flag is not recommended though. Variable Reordering ------------------- This is perhaps the trickest but the most important part of SMV (or any BDD-based tool in general). SMV's current reordering algorithm is quite primitive and slow. I would suggest the following algorthm for using SMV 1. use SMV without reordering and play with flags above to see if you can complete the verification. 2. if failure is still due to insufficient memory, use "-reorder" flag to enable dynamic variable reordering and capture the new order with the "-o" flag (for documentaiton, run smv without any arguments). Note that reordering can take quite a long time. I would recommend you let this run overnight. During reordering, if you get tired of waiting, press "Control-C" to terminate current reordering process and move on. The ordering obtained so far will be recorded. 3. Rerun SMV with the new ordering obtained ("-i" flag) and do not enable dynamic variable reordering. Hopefully, SMV will be able to make more progress than before. If failure is still due to insufficient memory, repeat step 2 and 3. CHANGES TO symbol.c ------------------- In the original SMV, the main routines are all in a file called symbol.c I have broken this file into the following pieces: ctl-compute.c Top level routines. ctl-eval.c Evalute expressions ctl-explain.c Counter-example/witness generation ctl-models.c ctl-models.h Analyze and process the input SMV model. This is also where macro-optimization takes place for models with many time-invariant constriants. ctl-op.c ctl-op.h CTL operators. ctl-trans.c ctl-trans.h Top-level routines for building transition relations. ctl-trans-cp.c Conjunctive partitioning representation top level routines. This is an improved version of Ranjan et al.'s IWLS'95 paper. For descriptions and performance study, please see my thesis in http://www.cs.cmu.edu/~bwolen/publications.html ctl-trans-dp.c Disjunctive partitioning representation top level routines (disjuntion over asynchronous processes). ctl-trans-merge.c ctl-trans-order.c Ordering and merging routines mainly for conjunctive partitioning. OTHER FILES ADDED ----------------- parameters.h Package parameters. bdd-helper.c bdd-helper.h BDD helper routines. smvBdd.c smvBdd.h smvBddAPI.h Modified version of original "bdd.c". Note that now there is a new concept called top-level node that is exported to the outside world. The use of BDDs obeys the "malloc" semantic; i.e., all objects will be kept alived unless explicitly freed. This allows us to support automatic garbage collection. Note that this is very different from the original SMV which has the following semantic 1. BDDs are not kept unless explicitly saved. 2. the check for garbage collection is explicitly called by users of the BDD package. smvMgr.c smvMgr.h Data structure for maintaining global parameters in the system. ORIGINAL SMV FILES ------------------ grammar.y grammar.c grammar.h hash.c hash.h input.c input.lex main.c misc.c node.c node.h symbols.c symbols.h ustring.c ustring.h ACKNOWLEDGEMENT --------------- The features added are the results of numerous discussions with Henry Rowley, Claudson Bornstein, Randy Bryant, Dave O'Hallaron, Yirng-An Chen, Ed Clarke, and Sergey Berezin. NOTE ---- CMU licenses all versions/derivatives of SMV. Please contact Prof. Edmund Clarke (emc@cs.cmu.edu) for more information. TODO ---- Good variable reordering routines would go very far in making this SMV more powerful. Also, there is no cone-of-influence analysis. DISCLAIMER ---------- I provide no guaranttees / warranties about this software. I did not get around to clean up the code as planned. I am releasing this code in a hurry before I leave CMU. There are many "#define"/"#ifdef" regions that allow me to perform various studies. However, these flags do make the code difficult to read. In particular, symbols.c is a gigantic mess. If you intend to continue modify this version of SMV, please keep in mind that all functionalities in symbols.c are replaced by the ctl-*.c files. "symbols.c" is kept around only as a wrapper for most cases. Good luck hacking. Bwolen Yang Carnegie Mellon University bwolen@cs.cmu.edu 7/16/99