bdd.java

一种将c高级语言转化给VHDL的编译器

	return l;
      if (l.isOne() || r.isOne()) 
	return ONE;
      if (l.isZero())
	return r;
      if (r.isZero()) 
	return l;
      break;
    case XOR:
      if (l == r) 
	return ZERO;
      if (l.isZero()) 
	return r;
      if (r.isZero())
	return l;
      break;
    case NAND:
      if (l.isZero() || r.isZero()) 
	return ONE;
      break;
    case NOR:
      if (l.isOne() || r.isOne()) 
	return ZERO;
      break;
    case IMPL:
      if (l.isZero()) 
	return ONE;
      if (l.isOne()) 
	return r;
      if (r.isOne()) 
	return l;
      break;
    }

    if (l.isConst() && r.isConst()) {
      res = (oprres[op][l.getRoot()<<1 | r.getRoot()] == 1 ? ONE : ZERO);
    } else {

      //int q_hash = applyHash(l,r,op);
      //System.err.println(" apply hash "+q_hash);
      entry = applycache.lookup(applyHash(l,r,op));

      //System.err.println(" Found "+entry.toApplyCache());
      
      if (entry.a == l && entry.b == r 
	  && ((Integer)entry.c).intValue() == op) {
	return (BDDNode)entry.res;
      }


      if (l.getLevel() == r.getLevel()) {
	//System.err.println("Level equal");
	bddrefstack.push(apply_rec(l.getLow(),r.getLow(),op));
	bddrefstack.push(apply_rec(l.getHigh(),r.getHigh(),op));
	
	res = makeNode(l.getLevel(), 
		       (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2),
		       (BDDNode)bddrefstack.peek());
      } else if (l.getLevel() < r.getLevel()) {
	//System.err.println("Level l less than r");
	bddrefstack.push(apply_rec(l.getLow(), r, op));
	bddrefstack.push(apply_rec(l.getHigh(), r, op));
	
	/*
	      System.err.println("Stack");
      Iterator stack_iter = bddrefstack.iterator();
    // Iterate on refstack
      while(stack_iter.hasNext()) {
	BDDNode node = (BDDNode) stack_iter.next();
	System.err.println("\t "+node);
      }
	*/
	//System.err.println(" peek()  "+ (BDDNode)bddrefstack.peek());
	//System.err.println(" trick() "+ (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2));
      


	res = makeNode(l.getLevel(), 
		       (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2),
		       (BDDNode)bddrefstack.peek());
      } else {
	//System.err.println("Level l bigger than r");
	bddrefstack.push(apply_rec(l, r.getLow(), op));
	bddrefstack.push(apply_rec(l, r.getHigh(), op));
	
	res = makeNode(r.getLevel(), 
		       (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2),
		       (BDDNode)bddrefstack.peek());
      }
      bddrefstack.pop();
      bddrefstack.pop();

      entry.a = l;
      entry.b = r;
      entry.c = op_integer[op];
      entry.res = res;
    }
    //System.out.println(" apply rec made "+res);

    return res;
  }

  public BDDNode bdd_restrict(BDDNode r, BDDNode var) {
    BDDNode res;
    int[] varset;

    if (r == null || r.getLow() == null) {
      new Exception().printStackTrace();
      System.out.println("Illegal BDD "+r);
      System.exit(-1);
    }

    if (var == null || var.getLow() == null) {
      new Exception().printStackTrace();
      System.out.println("Illegal BDD "+var);
      System.exit(-1);
    }
    
    // check op number ??

    if (var.getRoot() < 2) {
      return r;
    }
    
    varset = set2sintp(var);
    /*
    for (int i=0; i < varset.length; i++) {
      System.out.println(" varset ["+i+"] "+varset[i]);
    }
    */
    // size can change...

    //reset refstack -- uh, how do I have a stack that 
    // I am not pointing to the top?

    miscid = (var.getRoot() << 2) | CACHEID_RESTRICT;

    res = restrict_rec(r, varset, 0, varset.length);
    checkreorder(res);

    return res;
  }

  

  BDDNode restrict_rec(BDDNode r, int[] lvl, int current, int num) {
    BDDCacheData entry;
    BDDNode res;
    int level;
    
    if (r.getRoot() < 2 || num == 0) 
      return r;
    
    entry = misccache.lookup(restrHash(r,miscid));
    if (entry.a == r && ((Integer)entry.c).intValue() == miscid) 
      return (BDDNode)entry.res;

    level = Math.abs(lvl[current]) - 1;
    
    if (r.getLevel() == level) {
      if (lvl[current] > 0) 
	res = restrict_rec(r.getHigh(), lvl, current + 1, num - 1);
      else
	res = restrict_rec(r.getLow(), lvl, current + 1, num - 1);
    } else if (r.getLevel() < level) {
      bddrefstack.push(restrict_rec(r.getLow(), lvl, current, num));
      bddrefstack.push(restrict_rec(r.getHigh(), lvl, current, num));
      
      res = makeNode(r.getLevel(), 
		       (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2),
		       (BDDNode)bddrefstack.peek());
      bddrefstack.pop();
      bddrefstack.pop();
    } else {
      res = restrict_rec(r, lvl, current + 1, num - 1);
    }

    
    entry.a = r;
    entry.c = new Integer(miscid);
    entry.res = res;
      
    return res;
  }
   

  public BDDNode bdd_simplify(BDDNode f, BDDNode d) {
    BDDNode res;

   if (f == null || f.getLow() == null) {
      new Exception().printStackTrace();
      System.out.println("Illegal BDD "+f);
      System.exit(-1);
    }

    if (d == null || d.getLow() == null) {
      new Exception().printStackTrace();
      System.out.println("Illegal BDD "+d);
      System.exit(-1);
    }
    
    //reset refstack -- uh, how do I have a stack that 
    // I am not pointing to the top?
    
    res = simplify_rec(f,d);
    checkreorder(res);
    
    return res;
  }

  
  BDDNode simplify_rec(BDDNode f, BDDNode d) {
    BDDCacheData entry;
    BDDNode res;

    if (d.isZero()) 
      return ZERO;
    if (d.isOne())
      return f;
    if (f.isZero() || f.isOne())
      return f;

    entry = applycache.lookup(applyHash(f,d,SIMPLIFY));

    //System.err.println(" Found "+entry.toApplyCache());
    
    if (entry.a == f && entry.b == d 
	&& ((Integer)entry.c).intValue() == SIMPLIFY) {
      return (BDDNode)entry.res;
    }

    if (f.getLevel() == d.getLevel()) 
      if (d.getLow().isZero())
	res = simplify_rec(f.getHigh(), d.getHigh());
      else if (d.getHigh().isZero())
	res = simplify_rec(f.getLow(), d.getLow());
      else {
	bddrefstack.push(simplify_rec(f.getLow(), d.getLow()));
	bddrefstack.push(simplify_rec(f.getHigh(), f.getHigh()));

	res = makeNode(f.getLevel(), 
		       (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2),
		       (BDDNode)bddrefstack.peek());
	bddrefstack.pop();
	bddrefstack.pop();
      }
    else if (f.getLevel() < d.getLevel()) {
      bddrefstack.push(simplify_rec(f.getLow(), d ));
      bddrefstack.push(simplify_rec(f.getHigh(), d));
      
      res = makeNode(f.getLevel(), 
		     (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2),
		     (BDDNode)bddrefstack.peek());
      bddrefstack.pop();
      bddrefstack.pop();
    } else {
      bddrefstack.push(simplify_rec(f, d.getLow()));
      bddrefstack.push(simplify_rec(f, d.getHigh()));
      
      res = makeNode(d.getLevel(), 
		     (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2),
		     (BDDNode)bddrefstack.peek());
      bddrefstack.pop();
      bddrefstack.pop();
    }
      
    entry.a = f;
    entry.b = d;
    entry.c = op_integer[SIMPLIFY];
    entry.res = res;
    
    return res;
  }


  int[] set2sintp(BDDNode r) {
    BDDNode n;
    int num;
    int result[];

    if (r.getRoot() < 2) {
      System.out.println(" This is a error in set2sintp -- what??");
      System.exit(-1);
    }

    n = r;
    num = 0;

    while (n.getRoot() > 1) {
      if (n.getHigh().getRoot() >= 1) {
	n = n.getHigh();
      } else {
	n = n.getLow();
      }
      num++;
    }

    result = new int[num];
    n = r;
    num = 0;
    
    while (n.getRoot() > 1) {
      if (n.getHigh().getRoot() >= 1) {
	result[num++] = n.getLevel() + 1;
	n = n.getHigh();
      } else {
	result[num++] = -(n.getLevel() + 1);
	n = n.getLow();
      }
    }

    return result;
  }
	     
   
    
  void bdd_operator_reset() {
    applycache.reset();
    //itecache.reset();
    //quantcache.reset();
    //appexcache.reset();
    //replacecache.reset();
    misccache.reset();
  }

  void bdd_reorder_auto() {
    System.err.println(" NO auto reording ... ");
  }
						

  void bdd_noderesize() {
    BDDNode newnodes[];
    BDDNode next_node;
    int oldsize = bddnodesize;
    int n;

    if (bddnodesize >= bddmaxnodesize && bddmaxnodesize > 0) {
      System.err.println("No more nodes can be created ...??");
      System.exit(-1);
    }

    bddnodesize = bddnodesize << 1;
    
    if (bddnodesize > oldsize + maxnodeincrease)
      bddnodesize = oldsize + maxnodeincrease;
   
    if (bddnodesize > bddmaxnodesize  &&  bddmaxnodesize > 0)
      bddnodesize = bddmaxnodesize;

    /*
    if (resize_handler != NULL)
      resize_handler(oldsize, bddnodesize);
    */

    newnodes = new BDDNode[bddnodesize];

    // copy mess over 
    for (n = 0 ; n < oldsize ; n++) {
      bdd_nodes[n].setHash(null); // Nulls now?
      newnodes[n] = bdd_nodes[n];
    }
    
    bdd_nodes = newnodes;
    next_node = new BDDNode(oldsize);
    for (n = oldsize; n < bddnodesize - 1; n++)   {
      bdd_nodes[n] = next_node;
      next_node = new BDDNode(n+1);
      bdd_nodes[n].setNext(next_node);
    }
    bdd_nodes[bddnodesize-1] = next_node;
    bdd_nodes[bddnodesize-1].setNext(bddfreepos);

    bddfreepos = bdd_nodes[oldsize];
  }


  void bdd_clrvarblocks() {
    // System.err.println(" No bdd_clrvarblocks ");
  }

  public int getVar(BDDNode node) {  
    //System.out.println(" size  "+bddlevel2var.length+" level "+node.getLevel());
    if (node.getLevel() > 0) 
      return bddlevel2var[node.getLevel()].getRoot();  
    else 
      return -1;
  }

  public String toString() {
    StringBuffer sbuf = new StringBuffer();

    for (int i = 0; i < bddnodesize; i++) {
      sbuf.append(bdd_nodes[i]);
      sbuf.append("\n");
    }    
    // print caches
    // print mapping tables?

    return sbuf.toString();
  }

  public String toDot(BDDNode r) {
    StringBuffer sbuf = new StringBuffer();
    
    sbuf.append("digraph G {\n");
    if (r.isZero() || !r.isConst()) {
      sbuf.append("0 [shape=box, label=\"0\", ");
      sbuf.append("style=filled, shape=box, height=0.3, width=0.3];\n");
    }
    if (r.isOne() || !r.isConst()) {
      sbuf.append("1 [shape=box, label=\"1\", ");
      sbuf.append("style=filled, shape=box, height=0.3, width=0.3];\n");
    }

    sbuf.append(r.toDot(bddlevel2var));
    sbuf.append("}\n");
    r.clearMark();
    
    return sbuf.toString();
  }
   

    
  

  public static void main( String[] args ) {
    int i;
    BDD my_bdd = new BDD(10,100);
    //BDD my_bdd = new BDD(30000,100000);

    my_bdd.setVarNum(100);

    //System.out.println("my_bdd\n"+my_bdd);

    //BDDNode r[] = new BDDNode[10000];
    //BDDNode a[] = new BDDNode[10000];

    BDDNode b = my_bdd.bdd_ithvar(0);
    BDDNode c = my_bdd.bdd_ithvar(1);
    BDDNode a = my_bdd.bdd_ithvar(2);
    BDDNode d = my_bdd.bdd_ithvar(3);
    BDDNode e = my_bdd.bdd_ithvar(4);
    BDDNode f = my_bdd.bdd_ithvar(5);
    
    /*
    for(i=0; i<10000; i++) {
      //my_bdd.setVarNum(4+i);
      a[i] = my_bdd.bdd_ithvar(i);
    }
    */

    // add varblock ??

    BDDNode tmp1, tmp2, tmp3, tmp4, tmp5, tmp6, tmp7;

    tmp1 = my_bdd.bdd_not(b).incRefCount();
    tmp2 = my_bdd.bdd_not(b).incRefCount();
    tmp3 = my_bdd.bdd_not(tmp2).incRefCount();
    tmp2.decRefCount();
    tmp4 = my_bdd.bdd_apply(a,tmp1,AND).incRefCount();
    tmp1.decRefCount();
    tmp5 = my_bdd.bdd_apply(a,tmp3,AND).incRefCount();
    tmp3.decRefCount();
    tmp1 = my_bdd.bdd_apply(tmp4,c,OR).incRefCount();
    tmp4.decRefCount();
    tmp4 = my_bdd.bdd_apply(tmp1,c,OR).incRefCount();
    tmp1.decRefCount();
    tmp1 = my_bdd.bdd_apply(tmp4,c,OR).incRefCount();
    tmp4.decRefCount();

    d = my_bdd.bdd_apply(tmp1,tmp5,OR).incRefCount();
    tmp1.decRefCount();
    tmp5.decRefCount();

    tmp1 = my_bdd.bdd_apply(a,b,XOR).incRefCount();
    e = my_bdd.bdd_apply(tmp1,c,XOR).incRefCount();
    tmp1.decRefCount();

    tmp1 = my_bdd.bdd_apply(a,b,AND).incRefCount();
    tmp2 = my_bdd.bdd_apply(b,c,AND).incRefCount();
    f = my_bdd.bdd_apply(tmp1,tmp2,OR).incRefCount();
    tmp1.decRefCount();
    tmp2.decRefCount();
    tmp1 = my_bdd.bdd_apply(a,c,AND).incRefCount();
    f = my_bdd.bdd_apply(f,tmp1,OR).incRefCount();
    tmp1.decRefCount();

    System.out.println("sum a b c\n"+my_bdd.toDot(f));
    System.out.println("carry a b c\n"+my_bdd.toDot(e));

      /*
      r[i] = my_bdd.bdd_apply(my_bdd.bdd_apply(my_bdd.bdd_apply(my_bdd.bdd_apply(my_bdd.bdd_apply(a[i],my_bdd.bdd_not(b),AND),c,OR),c,OR),c,OR),my_bdd.bdd_apply(a[i],my_bdd.bdd_not(my_bdd.bdd_not(b)),AND),OR).incRefCount();
      */
      //System.out.println(" r["+i+"] "+r[i].getRoot());
    //r = my_bdd.bdd_apply(a,b,AND);

    
    System.out.println("my_bdd\n"+my_bdd.toDot(d));
    
    d = my_bdd.bdd_restrict(d,e);
    System.out.println("my_bdd\n"+my_bdd.toDot(d));
    
    d = a;
    d = my_bdd.bdd_restrict(d,e);
    System.out.println("my_bdd\n"+my_bdd.toDot(d));
  

  }

}