VCEGAR 1.1 BINARY INSTALLATION ****************************** 1. Download and install the Cadence SMV model checker. The website for obtaining SMV is: http://www.kenmcmil.com/smv.html. Make sure that Cadence SMV executable named "smv" is included in your path variable and is working as expected. 2. Download and install the zChaff SAT solver and unsat core extractor (zcore) which comes as part of the zChaff SAT solver. The website is: http://www.princeton.edu/~chaff/. Suppose you download zChaff 2004.11.15. Then the steps you need to perform (for generating zcore) are as follows: a. Uncomment "#define VERIFY_ON" in zchaff_solver.cpp (line 48). b. In the main routine of zverify_df.cpp replace "_dump_core = false" with "_dump_core = true". You need to do this only at one place (line 771). c. make all d. cp zverify_df zcore If you get compilation error during "make all" in get_mem_usage function of zverify_df.cpp, just comment the code inside get_mem_usage(). It is not really needed. Make sure that zchaff and zcore are available in your path variable. Once again make sure that zChaff and zcore are working as expected on some small examples. If you have trouble with any of the above steps let us know. 3. Include the vcegar binary in your path variable. 4. You are ready to go! Report problems to {hjain, kroening} AT cs DOT cmu DOT edu ----------------------------------------------------------------------- UPGRADING VCEGAR from 1.0 to 1.1 ******************************** If you already have a previous version of VCEGAR installed, then you don't have to install zChaff/zcore or Cadence SMV (smv) again. You can just replace the old vcegar binary with the new one. ----------------------------------------------------------------------- List of changes from VCEGAR 1.0 to VCEGAR 1.1 ********************************************** 1. MiniSat-p_v1.14 is used for abstraction computation, simulation of counterexamples, and simulation of abstract transitions. This improves the performance of VCEGAR significantly on some examples. You do not need to install MiniSat separately. 2. zChaff/zcore is used for one particular step that is related to discovery of new predicates. This is why you still need to have zChaff/zcore available. 3. The default option for predicate clustering (--partition) is now 6 (earlier it was 2). This option speeds up the abstraction computation which was a bottleneck for some examples. 4. Instead of providing the property to check using a separate file you can write the property in the Verilog file itself (see USAGE file for exactly how). When running vcegar give the --claim option to specify which property to check. -----------------------------------------------------------------------