This Homework has you implement a BDD package. The classes and their interfaces that you need to implement are defined in the file bddObj.h which is part of the source distribution. You must create the necessary support functions and data types to implement the classes and functions in the in the file bddObj.h and bddObj.cpp. You may modify only these two files and the file main.cpp. Everything should be defined, where possible, using the ITE operator. Also, you are required to use a unique table and a compute table for ITE. This project includes a predefined main, and you can change it to suit your needs. Also included is a Makefile for your convenience.

The ITE function declaration is given below:

BDD Ite(const BDD& g, const BDD& h, unsigned int limit = 0) const;

The function f is this object invoking the method (i.e., the this-object in the method definition). The function g and h have their usual meanings. Please ignore the limit variable that is optional in the CUDD interface.

Part of your grade depends on correctly managing memory. Memory leaks will cause deductions in your final score. You will need to check your work by running it with valgrind, ccmalloc, or similar memory degugging tool. Valgrind is current running on any of the Linux open lab machines.

Variable Ordering

The variable order is the order in which variables are created. The first created variable is the least variable that sits highest in the BDD. The most recent created variable is the greatest variable that sits just above the terminals. Using such an order will match the ordering in CUDD, and it will match the expected (assumed) ordering for the bddToDot function.

Obtaining the Source Distribution

The source is in a GIT repository which need to clone. The repository is located on the CS Open Lab under the egm account: ~egm/public-git/cs686/bdd-package. You must use GIT to clone the repository as well as to get updates and revisions throughout the semester. The GIT clone can be done as:

$ git clone ssh://_YOURID_@schizo.cs.byu.edu/~egm/public-git/cs686/bdd-package
   Cloning into 'bdd-package'...
   remote: Counting objects: 9, done.
   remote: Compressing objects: 100% (8/8), done.
   remote: Total 9 (delta 0), reused 0 (delta 0)
   Receiving objects: 100% (9/9), 8.15 KiB, done.
Please note that <user> should be your user name for the CS system. Also, some versions of GIT do not like the ~-expansion so you might need to include the full path to my home directory (/users/faculty/egm/public-git/cs431/lectures).

Building and Running

This source distribution will not compile and link out of the box as it is configured to use CUDD. You need to edit the Makefile to set any machine specific items that you may have including install location for CUDD. If you do not wish to use CUDD, then simply do not define USE_CUDD as explained in Makefile. You should now be able to issue make to build the bdd-test exectuble. Type the command:

   > make; bdd-test

Using CUDD as an Oracle

1) Download and build the CUDD libraries (make clean; make; make testobj) (ftp://vlsi.colorado.edu/pub/cudd-2.5.0.tar.gz direct link).

2) Create a lib directory in the CUDD source directory.

3) Create symbolic links in the lib directory for the following libraries:

    > ln -s ../obj/libobj.a
    > ln -s ../cudd/libcudd.a
    > ln -s ../mtr/libmtr.a
    > ln -s ../util/libutil.a
    > ln -s ../st/libst.a
    > ln -s ../epd/libepd.a

4) Set the USE_CUDD variable to 1 in the Makefile 5) Set the CUDD variable to the source tree for your installation for CUDD 6) For OSX Mavericks with the latest version of Xcode, you will need to add -stdlib=libstdc++ to the CLFAGS when you try to link against the libraries using g++.

bddToDot and Restrict

Using bddToDot is not mandatory for completing the homework. It is very possible to test your results by traversing your unique table and comparing to expected answers. If you would like to use it however, then please read on. When I made the choice to use C++ and CUDD rather than Java JBDD, I lost the simple functions f.getHigh() and f.getLow(); these are internal to CUDD and not available for public consumption. CUDD also does not have the “basic” cofactor that we discussed in class:

BDD basicCofactor(BDD f, int v, int pos) {
   if (v > f.getVariable()) {
      assert(0);
   }
   if (v == f.getVariable() && pos == 1) {
      return f.getHigh()
   }
   if (v == f.getVariable() && pos == 0) {
      return f.getLow()
   }
   return f;
}

CUDD does provide several versions of the more powerful cofactor that operates not on just a variable but any arbitrary function. One of these more powerful cofactor methods is restrict. The function f.Restrict(g) returns a new function that is f only variables in f are restricted to specific values which are those that make g true. If you call restrict as

BDD x = bddMgr.getVar(2);
f.Restrict(x);

The you get the function f with x set to true, which is a positive cofactor. f.Restrict(~x) is the negative cofactor. The Restrict method devolves into our basic cofactor if you only call it as suggested above (i.e., the answer is always either this.getLow(), this.getHigh(), or this). If you want to use bddToDot, then you need to add back into the interface the restrict function: BDD BDD::Restrict(BDD g) And implement that function in a manner similar to basic cofactor as below:

BDD Restrict(BDD g) {
   if (isOne() || isZero()) return *this; 
   int varIng = g.getVariable();
   int varInf = this.getVariable();
   BDD high = g.getHigh();
   BDD low = g.getLow();
   // Make sure g is a variable or a negated variable
   assert (high == bddMgr.getOne() || high == bddMgr.getZero());
   assert (low == bddMgr.getOne() || low == bddMgr.getZero());
   if (varIng > varInf) {
      assert(0);
   }
   if (varIng == varInf) {
      if (high == bddMgr.getOne())
         return this.getHigh();
      else 
         return this.getLow();
   }
   return *this;
}

The above code is only a template, and you will need to satisfy yourself that it is correct (or otherwise).

Grading

  • 20 points: Ite Implementation
  • 5 points: Using Ite to implement all Boolean connectives where apprioriate
  • 15 points: Tests and documentation (implementation details and how to test your code). Your documentation can be a separate file or the body of your commit comment (see me for help with Git).

Submission

Please submit a patch to the original repository via the Homework 5 link in Learning Suite.

cs-486/homework-5-2016.txt · Last modified: 2017/01/11 19:11 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0