************************************************************************* BDD Trace Driver (Ver. 0.9) Bwolen Yang School of Computer Science Carnegie Mellon University bwolen@cs.cmu.edu Created: 3/98 Last Modified: 11/98 ************************************************************************* Note ---- The next version of trace driver (Version 1.0) will have significantly changes in the interface to BDD packages. These changes are made to make this package more portable and also allow integration of BDD-trace generator to differnt tools. Originally, I planned to have this new new version (1.0) ready by Feb, 1999. Unfortunately, I have been pre-occupied trying to finish my thesis. Sorry for any inconvenience this may have caused. I have decided to release Version 0.9 to allow people to test the BDD traces used in the FMCAD'98 BDD performance study. If you are interested in porting your BDD package to the trace interface, please contact me (bwolen@cs.cmu.edu) to get the version 1.0 interface. Description ----------- "BDD Trace Driver" is a platform for executing BDD trace files. A trace file contains traces of calls to a BDD package; i.e., a record of how a BDD package is used. The "BDD Trace Driver" can then be used "replay" these traces to study or benchmark different BDD packages. (For the description of the trace file format, please see the file "README.trace".) Currently, this package is setup for BDD operations used in model checking. The supported operations are relational product (a.k.a. AndExist/AndAbstract), existential/universal quantification, composition (simultaneously replacing a set of variables with a set of functions), restrict, (Coudert's restrict algorithm for simplifying a BDD using Don't-Care space.) basic Boolean operations (and/or/not.... etc) At the end of execution, the statistics on this execution are reported. The performance (memory/time), gathered by the trace driver, is based on the BDD package's resource usage. This measurement excludes resource usage in setting up this package, parsing input files, and post-processing the statistics. The time usage reported is CPU time in seconds. The memory usage reported is the maximum heap usage in MBytes. (The maximum heap usage provides a good approximation to a BDD package's peak memory usage.) Other statistics collected by each BDD packages are reported after this. For the description of the statistics, please see the file "README.statistics". Software Requirement -------------------- gmake/gcc/flex/bison gcc/flex/bison can be easily replaced. To do so, please modify the definition of CC/LEX/YACC in Makefile.helper. Note: An ANSI C-compiler is required for CC. Installation ------------ Adding a new BDD package to this system is straightforward. Based on our experience in integrating CUDD (from University of Colorado) and CAL (from UC Berkeley), we expect this integration process to be especially easy for people who are familiar with the BDD package. The following is the definition for a list of symbols referred to in this section: foo: name of the new BDD package to integrate. fooIncludePath: path for interface header file. fooAPI.h: interface header file. FooManagerType: type of BDD manager in C. FooBddNodeType: type of BDD node in C. FooFnMapType: type of variables-to-functions map in C. libPath1, libPath2,...: paths for library files. libFoo1.a, libFoo2.a, ...: BDD libraries name. foo-driver: target executable name. FOO_PACKAGE: 's cpp symbol to be used in the trace driver. The steps to integrate into this package are: 1. Check to ensure that the BDD package collects and exports the statistics described in the file "README.statistics". This step may require modifications to the BDD package. 2. For the file "bddAPI.h", within the region /*---------------------------------------- * insert definition of new package below *---------------------------------------*/ /*---------------------------------------- * insert definition for new package above *---------------------------------------*/ insert the following: #elif defined(FOO_PACKAGE) # include typedef FooManagerType BddMgrType; typedef FooBddNodeType BddPtrType; typedef FooFnMapType BddFnMapType; 3. Write a fooPort.c interface file supplying all the functions described in the file "bddAPI.h". A template file port-template and port files for various BDD packages can be found in the "sample-port-files" directory. Please see the file "sample-port-files/README" for more detail. This package also comes with several examples "port" files: abcdPort.c: Interface to ABCD package by Armin Biere. ABCD can be obtained from http://iseran.ira.uka.de/~armin/abcd/ cuddPort.c: Interface to CUDD package from University of Colorado. CUDD can be obtained from http://vlsi.colorado.edu/~fabio/ ehvPort.c: Interface to EHV package by Geert Jansen. EHV can be obtained from ftp://ftp.ics.ele.tue.nl/pub/users/geert/bdd.tar.gz ppbfPort.c: Interface to parallel PBF package by Bwolen Yang (only combinational circuit ops is supported.) PPBF can be obtained from http://www.cs.cmu.edu/~bwolen/software/ NOTE: The port file of CAL package (UC Berkeley) is not included at the request of its author (Rajeev Ranjan). This is due to the fact that the CAL package used for the FMCAD BDD study is developed internally and have not been publicly released yet. For the latest public version of CAL pacakge, see http://www-cad.eecs.berkeley.edu/Research/cal_bdd/ Writing this interface file is mostly straightforward. Please note the following: a. If your BDD packages (like CUDD or SMV's BDD package) require the user to explicitly SAVE the BDDs returned from BDD operations, then for each BDD operation, be sure to save the result BDD before returning it. In contrast, other BDD packages (like CAL) saves the result before returning it. In this case, nothing special needs to be done. To compare the difference, please see how the function bdd_and() is written in cuddPort.c and calPort.c. b. The representation for a set of variables used by this trace package is a product (i.e. Boolean AND) of all the variables involved (which is the same as CUDD and SMV's BDD package). Set of variables is used in operations like existential/universal quantifications where the set represents the quantifying variables. If the new BDD package also represents variable set as a product, then nothing special need to be done. However, for BDD packages that do not use this product representation (e.g., CAL), you may be able to use package's support_var() routine to obtain the membership of the set. (support_var() returns the support variables in a BDD.) Please see bdd_exists() and lookup_association() in calPort.c for example. 4. Add the following rule for foo-driver to the Makefile foo-driver: @gmake-f Makefile.helper \ "TARGET = $@" \ "PACKAGE = FOO_PACKAGE" \ "PORTFILE = fooPort.c" \ "INCLUDE = -IfooIncludePath" \ "BDDLIBPATHS = -LlibPath1 -LlibPath2 ..." \ "BDDLIBS = -lfoo1 -lfoo2 ..." where TARGET: Name of executable. ($@ means same as the target of this rule, i.e., foo-driver). PACKAGE: Name (internal cpp symbol) of this package used in "bddAPI.h". PORTFILE: Name of the interface file that is written for this new BDD package. INCLUDE: The directory contains a BDD package's own interface header file can be found. BDDLIBPATHS: paths for 's BDD libraries. BDDLIBS: 's BDD libraries. Compilation ----------- gmake foo-driver Create an executable foo-driver 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". Execution --------- Synopsis: foo-driver [options] Options: Documentation of options can be obtained from the manual pages in the file "bdd-trace-driver.1" or by simply execute the driver without any arguments: foo-driver Testing ------- There are some small sample traces in the directory sample-traces/ The traces files have the file name extension of *.trace. A set of sample outputs (*.out) are also provided for references. Note that for equality operations, if the results are annotated in the trace, the trace driver will always check for the correctness of the results. For details about the trace format, please see the file "README.trace". Files ----- CHAGES List of changes to this package. (This will start with the official release of 1.0.) Makefile The main make file. This is where rules for making new packages is inserted. Makefile.helper Internal core make file. README This file. README.trace Description of trace file format. README.statistics Description of the useful BDD statistics to collect. bdd-trace-driver.1 Manual page for this package. bddAPI.h Interface header file. dd-ops.c dd-ops.h Information associated with each operation. driver.c driver.h The main C source file and its header file for this BDD trace driver. generic.h Generic header definitions. grammar.y Grammar for yacc or bison. myassert.h My version of assert. myhash.c myhash.h Generic hashing library. obj/ Object file directory scanner.l File for lexical scanner. (for lex or flex). sample-port-files This directory contains a template for port file "port-template" and port files for variables BDD pacakges. sample-traces/ This directory contains sample trace files and sample outputs. util.c util.h Useful utility functions for general software development. BUGS ---- For some systems (like Linux), the memory usage reported by this package can be completely wrong. This is because maximum heap growth is tracked using sbrk(0) and thus, incorrect results can be reported on systems where the heap can shrink (like Linux). Fortunately, this measurement methodology works for the following systems: SGI/Irix, SunOS, Solaris (SunOS 5), and Alpha/OSF. (For Alpha/OSF, this package explicitly turned off the heap shrinking feature.) Acknowledgement --------------- This package is based on the front end of ACV (arithmetic circuit verifier). ACV is written by Yirng-An Chen (yachen@cs.cmu.edu) from Carnegie Mellon University. Lawyerese --------- If you will be using one of the included files and/or any part of any included file in another system, it is your responsibility and duty to ensure this notice appears with the included file and/or its parts and in the documentation for your system. /* * Copyright (c) 1998 Carnegie Mellon University. * All Rights Reserved. * * Permission to use, copy, modify, and distribute this software and * its documentation is hereby granted (including for commercial or * for-profit use), provided that both the copyright notice and this * permission notice appear in all copies of the software, derivative * works, or modified versions, and any portions thereof, and that * both notices appear in supporting documentation, and that credit * is given to Carnegie Mellon University in all publications reporting * on direct or indirect use of this code or its derivatives. * * THIS IMPLEMENTATION MAY HAVE BUGS, SOME OF WHICH MAY HAVE SERIOUS * CONSEQUENCES. CARNEGIE MELLON PROVIDES THIS SOFTWARE IN ITS "AS IS" * CONDITION, AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, * BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY * AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL * CARNEGIE MELLON UNIVERSITY BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED * TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. * * Carnegie Mellon encourages (but does not require) users of this * software to return any improvements or extensions that they make, * and to grant Carnegie Mellon the rights to redistribute these * changes without encumbrance. */