bdd.java

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

/*
 *
 LA-CC 05-135 Trident 0.7.1

Copyright Notice
Copyright 2006 (c) the Regents of the University of California.

This Software was produced under a U.S. Government contract
(W-7405-ENG-36) by Los Alamos National Laboratory, which is operated
by the University of California for the U.S. Department of Energy. The
U.S. Government is licensed to use, reproduce, and distribute this
Software. Permission is granted to the public to copy and use this
Software without charge, provided that this Notice and any statement
of authorship are reproduced on all copies. Neither the Government nor
the University makes any warranty, express or implied, or assumes any
liability or responsibility for the user of this Software.

 
 */ 

package fp.util.bdd;

import java.util.HashMap;
import java.util.Stack;
import java.util.Iterator;

public class BDD {
  static final int MAXVAR = 0x1FFFFF;

  BDDNode bdd_nodes[];

  BDDNode ZERO, ONE;
  
  int bddnodesize;
  int bddmaxnodesize;

  int bddvarnum;
  BDDNode bddfreepos;
  int bddfreenum;

  BDDNode bddvarset[];
  BDDNode bddlevel2var[];
  BDDNode bddvar2level[];
  
  Stack bddrefstack;

  BDDCache applycache;
  //BDDCache itecache;
  //BDDCache quantcache;
  //BDDCache appexcache;
  //BDDCache replacecache;
  BDDCache misccache;

  static final int CACHEID_RESTRICT = 0x1;

  int miscid;
  int cachesize;
  int maxnodeincrease;
  int bddproduced = 0;

  boolean bdd_try_reordering = false;
  int bdd_reorder_method = 0;

  static int gbcollectnum;
  static int minfreenodes = 20;

  static int DEFAULTMAXNODEINC = 50000;
  
  BDDPairs bdd_pairs;

  public static final int AND  = 0;
  public static final int XOR  = 1;
  public static final int OR   = 2;
  public static final int NAND = 3;

  public static final int NOR  = 4;
  public static final int IMPL = 5;
  public static final int BIML = 6;
  public static final int DIFF = 7;

  public static final int LESS = 8;
  public static final int IIMP = 9;
  public static final int NOT  = 10;
  public static final int SIMPLIFY = 11;

  static String op_name[] = {
    "AND",  "XOR",  "OR",   "NAND", 
    "NOR", "IMPL",  "BIML", "DIFF", 
    "LESS", "IIMP", "NOT" };

  static Integer op_integer[] = {
    new Integer(AND),  new Integer(XOR),  new Integer(OR), 
    new Integer(NAND), new Integer(NOR),  new Integer(IMPL),
    new Integer(BIML), new Integer(DIFF), new Integer(LESS),
    new Integer(IIMP), new Integer(NOT), new Integer(SIMPLIFY),
  };


  static int oprres[][] = {
    {0,0,0,1},  /* and                       ( & )         */
    {0,1,1,0},  /* xor                       ( ^ )         */
    {0,1,1,1},  /* or                        ( | )         */
    {1,1,1,0},  /* nand                                    */
    {1,0,0,0},  /* nor                                     */
    {1,1,0,1},  /* implication               ( >> )        */
    {1,0,0,1},  /* bi-implication                          */
    {0,0,1,0},  /* difference /greater than  ( - ) ( > )   */
    {0,1,0,0},  /* less than                 ( < )         */
    {1,0,1,1},  /* inverse implication       ( << )        */
    {1,1,0,0}   /* not                       ( ! )         */
  };

  public BDD(int nodesize, int cs) {
    //hash = new Hashmap(nodesize); 
    
    bddnodesize = nodesize;

    bdd_nodes = new BDDNode[nodesize];

    BDDNode next_node = new BDDNode(2);
    for (int i = 2; i < nodesize - 1; i++) {
      bdd_nodes[i] = next_node;
      next_node = new BDDNode(i+1);
      bdd_nodes[i].setNext(next_node);
    }
    bdd_nodes[nodesize-1] = next_node;
    bdd_nodes[nodesize-1].setNext(null);
    
    ZERO = bdd_nodes[0] = BDDNode.ZERO;
    ONE = bdd_nodes[1] = BDDNode.ONE;
    
    ZERO.setRoot(0); ONE.setRoot(1);
    ZERO.setMaxRefCount();
    ONE.setMaxRefCount();
    ZERO.setLow(ZERO); ZERO.setHigh(ZERO);
    ONE.setLow(ONE); ONE.setHigh(ONE);
    ONE.setNext(bdd_nodes[2]);
    ZERO.setNext(ONE);

    bdd_operator_init(cs);

    // bdd operator cache init

    bddfreepos = bdd_nodes[2];
    bddfreenum = nodesize - 2;
    bddvarnum = 0;
    gbcollectnum = 0;
    cachesize = cs;
    
    bdd_reorder_method = 0;
    bdd_try_reordering = false;
    maxnodeincrease = DEFAULTMAXNODEINC;

    // Other Init
    //bdd_fddinit();
    bdd_clrvarblocks();

    // bdd pairs init
    bdd_pairs = new BDDPairs(this);
    //bdd_reorder_init();

  }

  static int PAIR(int a, int b) {
    return ((a + b) * (a + b + 1)/2 + a);
  }

  static long TRIPLE(int a, int b, int c) {
    long p = PAIR(a,b);
    long result = ((p + c) * (p + c + 1) / 2 + p);
    return result;
  }

  int nodeHash(int lvl, BDDNode low, BDDNode high) {
    /*
    int a = lvl;
    int b = low.getRoot();
    int c = high.getRoot();
    System.err.println("a "+a+" b "+b+" c "+c);
    System.err.println("PAIR(a,b) "+PAIR(a,b));
    System.err.println("PAIR(PAIR(a,b),c) "+PAIR(PAIR(a,b),c));
    System.err.println("TRIPLE(a,b,c) % nodesize "+(TRIPLE(a,b,c) % bddnodesize));
    */
    return (int)(TRIPLE(lvl,low.getRoot(),high.getRoot()) % bddnodesize);
  }

  int applyHash(BDDNode l, BDDNode r, int op) {
    /*
    int a = l.getRoot();
    int b = r.getRoot();
    int c = op;
    System.err.println("a "+a+" b "+b+" c "+c);
    System.err.println("PAIR(a,b) "+PAIR(a,b));
    System.err.println("PAIR(PAIR(a,b),c) "+PAIR(PAIR(a,b),c));
    System.err.println("TRIPLE(a,b,c) "+(TRIPLE(a,b,c)));
    System.err.println("TRIPLE(a,b,c) % nodesize "+(TRIPLE(a,b,c) % 0x80000000));
    */
    return (int)(Math.abs(TRIPLE(l.getRoot(), r.getRoot(), op)) % 0x80000000);
  }

  int notHash(BDDNode r) {
    return (r.getRoot());
  }

  int restrHash(BDDNode r, int misc) {
    return (PAIR(r.getRoot(),misc));
  }

  void bdd_operator_init(int cachesize) {
    //System.out.println("Cache Inited!");
    applycache = new BDDCache(cachesize);
    //itecache = new BDDCache(cachesize);
    //quantcache = new BDDCache(cachesize);
    //appexcache = new BDDCache(cachesize);
    //replacecache = new BDDCache(cachesize);
    misccache = new BDDCache(cachesize);
  }



  void bdd_gbc() {
    System.out.println("Garbage Collecting! "+gbcollectnum);

    Iterator stack_iter = bddrefstack.iterator();
    // Iterate on refstack
    while(stack_iter.hasNext()) {
      BDDNode node = (BDDNode) stack_iter.next();
      node.setMark();
    }

    for (int n=0; n<bddnodesize; n++) {
      if (bdd_nodes[n].getRefCount() > 0) 
	bdd_nodes[n].setMark();

      // Should this be ZERO or null
      bdd_nodes[n].setHash(null);
    }
    
    bddfreepos = null;
    bddfreenum = 0;
    
    for (int n=2; n < bddnodesize; n++) {
      BDDNode node = bdd_nodes[n];
      
      if ((node.getMark()) && (node.getLow() != null) ) {
	int hash;
	
	node.unmark();
	hash = nodeHash(node.getLevel(), node.getLow(), node.getHigh());
	node.setNext(bdd_nodes[hash].getHash());
	bdd_nodes[hash].setHash(bdd_nodes[n]);
      } else {
	node.setLow(null);
	node.setNext(bddfreepos);
	bddfreepos = bdd_nodes[n];
	bddfreenum++;
      }
    }

    bdd_operator_reset();
    
    gbcollectnum++;
  }


  BDDNode makeNode(int level, BDDNode low, BDDNode high) {
    BDDNode node;
    int hash;
    BDDNode res;
    
    //System.err.println("Makenode!");

    //System.err.println(" lvl: "+level+" l: "+low.getRoot()+" h: "+high.getRoot());
    //System.err.println(" equal "+(low == high));
    // Check whether children are equal
    if (low == high) 
      return low;
  
    // find existing node
    // This is a problem ...
    hash = nodeHash(level, low, high);
    //System.err.println(" Hash returned "+hash+" nodesize "+bddnodesize);
    res = bdd_nodes[hash].getHash();

    while (res != null) {
      if (res.getLevel() == level
	  && res.getLow() == low
	  && res.getHigh() == high)
	return res;
      res = res.getNext();
    }

    if (bddfreepos == null) {

      //System.err.println(" freepos == null -- will garbage collect!");

      bdd_gbc();

      if ((bddfreenum*100)/bddnodesize <= minfreenodes) {
	// Must always run rehash after noderesize()
	bdd_noderesize();
	bdd_gbc();
	bdd_try_reordering = true;
	hash = nodeHash(level, low, high);
      }

      if (bddfreepos == null) {
	System.err.println("Cannot find free nodes");
	System.exit(-1);
      }
    }
    
    res = bddfreepos;
    bddfreepos = bddfreepos.getNext();
    /*
    if (bddfreepos != null) 
      System.err.println("FreePos now is "+bddfreepos.getRoot());
    else 
      System.err.println("FreePos now is null");
    */
    bddfreenum--;
    bddproduced++;
    
    node = res;
    node.setLevel(level);
    node.setLow(low);
    node.setHigh(high);

    node.setNext(bdd_nodes[hash].getHash());
    bdd_nodes[hash].setHash(res);

    return res;
  }

  public void setVarNum(int num) {
    if ((num < 1) || ( num > MAXVAR)) {
      System.err.println("Number of BDD Vars out of range");
      System.exit(-1);
    }

    if (num < bddvarnum) {
      System.err.println("Number of variables can only be increased.");
      System.exit(-1);
    }

    // nothing to do -- do nothing.
    if (num == bddvarnum) return;

    if (bddvarset == null) {
      // needs real nodes ??
      bddvarset = new BDDNode[num*2];
      bddlevel2var = new BDDNode[num];
      bddvar2level = new BDDNode[num];
    } else {

      // build bigger arrays.
      BDDNode[] new_bddvarset = new BDDNode[num*2];
      BDDNode[] new_bddlevel2var = new BDDNode[num];
      BDDNode[] new_bddvar2level = new BDDNode[num];
      
      // copy old references
      for(int n=0; n<bddvarnum; n++) {
	new_bddvarset[n] = bddvarset[n];
	new_bddvarset[n+bddvarnum] = bddvarset[n+bddvarnum];
	new_bddlevel2var[n] = bddlevel2var[n];
	new_bddvar2level[n] = bddvar2level[n];
      }

      // move new arrays into place
      bddvarset = new_bddvarset;
      bddlevel2var = new_bddlevel2var;
      bddvar2level = new_bddvar2level;
    }

    if (bddrefstack == null) {
      bddrefstack = new Stack();
    }
	
    for( ;bddvarnum < num; bddvarnum++) {
      bddvarset[bddvarnum*2] = 
	(BDDNode)bddrefstack.push(makeNode(bddvarnum,ZERO,ONE));
      bddvarset[bddvarnum*2 + 1] = makeNode(bddvarnum,ONE,ZERO);
      bddrefstack.pop();
      
      bddvarset[bddvarnum*2].setMaxRefCount();
      bddvarset[bddvarnum*2+1].setMaxRefCount();
      bddlevel2var[bddvarnum] = bdd_nodes[bddvarnum];
      bddvar2level[bddvarnum] = bdd_nodes[bddvarnum];
      
    }

    ZERO.setLevel(num);
    ONE.setLevel(num);

    bdd_pairs.resize(bddvarnum);

  }
   
  
  public BDDNode bdd_ithvar(int var) {
    if (var < 0 || var >= bddvarnum) {
      System.err.println("Illegal varnum "+var);
      System.exit(-1);
    }
    return bddvarset[var*2];
  }

  void checkreorder(BDDNode node) {
    node.incRefCount();
    if (bdd_try_reordering)
      bdd_reorder_auto();
    bdd_try_reordering = false;
    
    node.decRefCount();
  }

  public BDDNode bdd_not(BDDNode r) {
    BDDNode res;

    if (r == null || r.getLow() == null) {
      new Exception().printStackTrace();
      System.out.println("Illegal BDD "+r);
      System.exit(-1);
    }
    
    // reset refstack ???
    
    res = not_rec(r);
    checkreorder(res);
    return res;
  }
   
  BDDNode not_rec(BDDNode r) {
    BDDCacheData entry;
    BDDNode res;
    
    if (r.isZero())
      return ONE;
    if (r.isOne())
      return ZERO;
    
    entry = applycache.lookup(notHash(r));

    if (entry.a == r && ((Integer)entry.c).intValue() == NOT) {
      return (BDDNode)entry.res;
    }

    bddrefstack.push(not_rec(r.getLow()));
    bddrefstack.push(not_rec(r.getHigh()));
	
    res = makeNode(r.getLevel(), 
		   (BDDNode)bddrefstack.elementAt(bddrefstack.size() - 2),
		   (BDDNode)bddrefstack.peek());
    
    bddrefstack.pop();
    bddrefstack.pop();

    entry.a = r;
    entry.c = op_integer[NOT];
    entry.res = res;
    
    return res;
  }



  public BDDNode bdd_apply(BDDNode l, BDDNode r, int op) {
    BDDNode res;
    
    if (r == null || r.getLow() == null) {
      new Exception().printStackTrace();
      System.out.println("Illegal BDD "+r);
      System.exit(-1);
    }

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

    return res;
  }
   
  BDDNode apply_rec(BDDNode l, BDDNode r, int op) {
    BDDCacheData entry;
    BDDNode res;

    //System.out.println(" apply_rec "+l.getRoot()+" "+op_name[op]+" "+r.getRoot());
  
    switch(op) {
    case AND:
      if (l == r) 
	return l;
      if (l.isZero() || r.isZero()) 
	return ZERO;
      if (l.isOne())
	return r;
      if (r.isOne())
	return l;
      break;
    case OR:
      if (l == r)