abc/src/bool/kit/cloud.h - third_party/vtr-verilog-to-routing - Git at Google

 /**CFile****************************************************************

   FileName    [cloud.h]

   PackageName [Fast application-specific BDD package.]

   Synopsis    [Interface of the package.]

   Author      [Alan Mishchenko <alanmi@ece.pdx.edu>]

   Affiliation [ECE Department. Portland State University, Portland, Oregon.]

   Date        [Ver. 1.0. Started - June 10, 2002.]

   Revision    [$Id: cloud.h,v 1.0 2002/06/10 03:00:00 alanmi Exp $]

 ***********************************************************************/

 #ifndef ABC__aig__kit__cloud_h
 #define ABC__aig__kit__cloud_h


 #include <stdio.h>
 #include <stdlib.h>
 #include <assert.h>

 #include "misc/util/abc_global.h"


 ABC_NAMESPACE_HEADER_START


 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
 #endif

 ////////////////////////////////////////////////////////////////////////
 //  n |  2^n ||  n |    2^n ||  n |        2^n ||  n |           2^n  //
 //====================================================================//
 //  1 |    2 ||  9 |    512 || 17 |    131,072 || 25 |    33,554,432  //
 //  2 |    4 || 10 |  1,024 || 18 |    262,144 || 26 |    67,108,864  //
 //  3 |    8 || 11 |  2,048 || 19 |    524,288 || 27 |   134,217,728  //
 //  4 |   16 || 12 |  4,096 || 20 |  1,048,576 || 28 |   268,435,456  //
 //  5 |   32 || 13 |  8,192 || 21 |  2,097,152 || 29 |   536,870,912  //
 //  6 |   64 || 14 | 16,384 || 22 |  4,194,304 || 30 | 1,073,741,824  //
 //  7 |  128 || 15 | 32,768 || 23 |  8,388,608 || 31 | 2,147,483,648  //
 //  8 |  256 || 16 | 65,536 || 24 | 16,777,216 || 32 | 4,294,967,296  //
 ////////////////////////////////////////////////////////////////////////

 // data structure typedefs
 typedef struct cloudManager       CloudManager;
 typedef unsigned                  CloudVar;
 typedef unsigned                  CloudSign;
 typedef struct cloudNode          CloudNode;
 typedef struct cloudCacheEntry1   CloudCacheEntry1;
 typedef struct cloudCacheEntry2   CloudCacheEntry2;
 typedef struct cloudCacheEntry3   CloudCacheEntry3;

 // operation codes used to set up the cache
 typedef enum {
     CLOUD_OPER_AND,
     CLOUD_OPER_XOR,
     CLOUD_OPER_BDIFF,
     CLOUD_OPER_LEQ
 } CloudOper;

 /*
 // the number of operators using cache
 static int CacheOperNum = 4;

 // the ratio of cache size to the unique table size for each operator
 static int CacheLogRatioDefault[4] = {
     4, // CLOUD_OPER_AND,
     8, // CLOUD_OPER_XOR,
     8, // CLOUD_OPER_BDIFF,
     8  // CLOUD_OPER_LEQ
 };

 // the ratio of cache size to the unique table size for each operator
 static int CacheSize[4] = {
     2, // CLOUD_OPER_AND,
     2, // CLOUD_OPER_XOR,
     2, // CLOUD_OPER_BDIFF,
     2  // CLOUD_OPER_LEQ
 };
 */

 // data structure definitions
 struct cloudManager            // the fast bdd manager
 {
     // variables
     int nVars;                 // the number of variables allocated
     // bits
     int bitsNode;              // the number of bits used for the node
     int bitsCache[4];          // default: bitsNode - CacheSizeRatio[i]
     // shifts
     int shiftUnique;           // 8*sizeof(unsigned) - (bitsNode + 1)
     int shiftCache[4];         // 8*sizeof(unsigned) -  bitsCache[i]
     // nodes
     int nNodesAlloc;           // 2 ^ (bitsNode + 1)
     int nNodesLimit;           // 2 ^  bitsNode
     int nNodesCur;             // the current number of nodes (including const1 and vars)
     // signature
     CloudSign nSignCur;

     // statistics
     int nMemUsed;              // memory usage in bytes
     // cache stats
     int nUniqueHits;           // hits in the unique table
     int nUniqueMisses;         // misses in the unique table
     int nCacheHits;            // hits in the caches
     int nCacheMisses;          // misses in the caches
     // the number of steps through the hash table
     int nUniqueSteps;

     // tables
     CloudNode * tUnique;       // the unique table to store BDD nodes

     // special nodes
     CloudNode * pNodeStart;    // the pointer to the first node
     CloudNode * pNodeEnd;      // the pointer to the first node out of the table

     // constants and variables
     CloudNode *  one;          // the one function
     CloudNode *  zero;         // the zero function
     CloudNode ** vars;         // the elementary variables

     // temporary storage for nodes
     CloudNode ** ppNodes;

     // caches
     CloudCacheEntry2 * tCaches[20];    // caches
 };

 struct cloudNode   // representation of the node in the unique table
 {
     CloudSign   s;         // signature
     CloudVar    v;         // variable
     CloudNode * e;         // negative cofactor
     CloudNode * t;         // positive cofactor
 };
 struct cloudCacheEntry1  // one-argument cache
 {
     CloudSign   s;         // signature
     CloudNode * a;         // argument 1
     CloudNode * r;         // result
 };
 struct cloudCacheEntry2  // the two-argument cache
 {
     CloudSign   s;         // signature
     CloudNode * a;
     CloudNode * b;
     CloudNode * r;
 };
 struct cloudCacheEntry3  // the three-argument cache
 {
     CloudSign   s;         // signature
     CloudNode * a;
     CloudNode * b;
     CloudNode * c;
     CloudNode * r;
 };


 // parameters
 #define CLOUD_NODE_BITS              23

 #define CLOUD_CONST_INDEX            ((unsigned)0x0fffffff)
 #define CLOUD_MARK_ON                ((unsigned)0x10000000)
 #define CLOUD_MARK_OFF               ((unsigned)0xefffffff)

 // hash functions a la Buddy
 #define cloudHashBuddy2(x,y,s)       ((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1))
 #define cloudHashBuddy3(x,y,z,s)     (cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1))
 // hash functions a la Cudd
 #define DD_P1                           12582917
 #define DD_P2                         4256249
 #define DD_P3                         741457
 #define DD_P4                         1618033999
 #define cloudHashCudd2(f,g,s)        ((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2) >> (s))
 #define cloudHashCudd3(f,g,h,s)      (((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2 + (unsigned)(ABC_PTRUINT_T)(h)) * DD_P3) >> (s))

 // node complementation (using node)
 #define Cloud_Regular(p)             ((CloudNode*)(((ABC_PTRUINT_T)(p)) & ~01))   // get the regular node (w/o bubble)
 #define Cloud_Not(p)                 ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^  01))   // complement the node
 #define Cloud_NotCond(p,c)           ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ (c)))   // complement the node conditionally
 #define Cloud_IsComplement(p)        ((int)(((ABC_PTRUINT_T)(p)) & 01))           // check if complemented
 // checking constants (using node)
 #define Cloud_IsConstant(p)          (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
 #define cloudIsConstant(p)           (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)

 // retrieving values from the node (using node structure)
 #define Cloud_V(p)                   ((Cloud_Regular(p))->v)
 #define Cloud_E(p)                   ((Cloud_Regular(p))->e)
 #define Cloud_T(p)                   ((Cloud_Regular(p))->t)
 // retrieving values from the regular node (using node structure)
 #define cloudV(p)                    ((p)->v)
 #define cloudE(p)                    ((p)->e)
 #define cloudT(p)                    ((p)->t)
 // marking/unmarking (using node structure)
 #define cloudNodeMark(p)             ((p)->v       |= CLOUD_MARK_ON)
 #define cloudNodeUnmark(p)           ((p)->v       &= CLOUD_MARK_OFF)
 #define cloudNodeIsMarked(p)         ((int)((p)->v &  CLOUD_MARK_ON))

 // cache lookups and inserts (using node)
 #define cloudCacheLookup1(p,sign,f)     (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0))
 #define cloudCacheLookup2(p,sign,f,g)   (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0))
 #define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0))
 // cache inserts
 #define cloudCacheInsert1(p,sign,f,r)     (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r)))
 #define cloudCacheInsert2(p,sign,f,g,r)   (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r)))
 #define cloudCacheInsert3(p,sign,f,g,h,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r)))

 //#define CLOUD_ASSERT(p)              (assert((p) >= (dd->pNodeStart-1) && (p) < dd->pNodeEnd))
 #define CLOUD_ASSERT(p)            assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc)

 ////////////////////////////////////////////////////////////////////////
 ///                       FUNCTION DECLARATIONS                      ///
 ////////////////////////////////////////////////////////////////////////
 // starting/stopping
 extern CloudManager * Cloud_Init( int nVars, int nBits );
 extern void           Cloud_Quit( CloudManager * dd );
 extern void           Cloud_Restart( CloudManager * dd );
 extern void           Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int size );
 extern CloudNode *    Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e );
 // support and node count
 extern CloudNode *    Cloud_Support( CloudManager * dd, CloudNode * n );
 extern int            Cloud_SupportSize( CloudManager * dd, CloudNode * n );
 extern int            Cloud_DagSize( CloudManager * dd, CloudNode * n );
 extern int            Cloud_DagCollect( CloudManager * dd, CloudNode * n );
 extern int            Cloud_SharingSize( CloudManager * dd, CloudNode * * pn, int nn );
 // cubes
 extern CloudNode *    Cloud_GetOneCube( CloudManager * dd, CloudNode * n );
 extern void           Cloud_bddPrint( CloudManager * dd, CloudNode * Func );
 extern void           Cloud_bddPrintCube( CloudManager * dd, CloudNode * Cube );
 // operations
 extern CloudNode *    Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g );
 extern CloudNode *    Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g );
 // stats
 extern void           Cloud_PrintInfo( CloudManager * dd );
 extern void           Cloud_PrintHashTable( CloudManager * dd );


 ABC_NAMESPACE_HEADER_END


 #endif

 ////////////////////////////////////////////////////////////////////////
 ///                            END OF FILE                           ///
 ////////////////////////////////////////////////////////////////////////
	/CFile**************************************************************

	FileName [cloud.h]

	PackageName [Fast application-specific BDD package.]

	Synopsis [Interface of the package.]

	Author [Alan Mishchenko <alanmi@ece.pdx.edu>]

	Affiliation [ECE Department. Portland State University, Portland, Oregon.]

	Date [Ver. 1.0. Started - June 10, 2002.]

	Revision [$Id: cloud.h,v 1.0 2002/06/10 03:00:00 alanmi Exp $]

	***********************************************************************/

	#ifndef ABC__aig__kit__cloud_h
	#define ABC__aig__kit__cloud_h


	#include <stdio.h>
	#include <stdlib.h>
	#include <assert.h>

	#include "misc/util/abc_global.h"



	ABC_NAMESPACE_HEADER_START


	#ifdef _WIN32
	#define inline __inline // compatible with MS VS 6.0
	#endif

	////////////////////////////////////////////////////////////////////////
	// n \| 2^n \|\| n \| 2^n \|\| n \| 2^n \|\| n \| 2^n //
	//====================================================================//
	// 1 \| 2 \|\| 9 \| 512 \|\| 17 \| 131,072 \|\| 25 \| 33,554,432 //
	// 2 \| 4 \|\| 10 \| 1,024 \|\| 18 \| 262,144 \|\| 26 \| 67,108,864 //
	// 3 \| 8 \|\| 11 \| 2,048 \|\| 19 \| 524,288 \|\| 27 \| 134,217,728 //
	// 4 \| 16 \|\| 12 \| 4,096 \|\| 20 \| 1,048,576 \|\| 28 \| 268,435,456 //
	// 5 \| 32 \|\| 13 \| 8,192 \|\| 21 \| 2,097,152 \|\| 29 \| 536,870,912 //
	// 6 \| 64 \|\| 14 \| 16,384 \|\| 22 \| 4,194,304 \|\| 30 \| 1,073,741,824 //
	// 7 \| 128 \|\| 15 \| 32,768 \|\| 23 \| 8,388,608 \|\| 31 \| 2,147,483,648 //
	// 8 \| 256 \|\| 16 \| 65,536 \|\| 24 \| 16,777,216 \|\| 32 \| 4,294,967,296 //
	////////////////////////////////////////////////////////////////////////

	// data structure typedefs
	typedef struct cloudManager CloudManager;
	typedef unsigned CloudVar;
	typedef unsigned CloudSign;
	typedef struct cloudNode CloudNode;
	typedef struct cloudCacheEntry1 CloudCacheEntry1;
	typedef struct cloudCacheEntry2 CloudCacheEntry2;
	typedef struct cloudCacheEntry3 CloudCacheEntry3;

	// operation codes used to set up the cache
	typedef enum {
	CLOUD_OPER_AND,
	CLOUD_OPER_XOR,
	CLOUD_OPER_BDIFF,
	CLOUD_OPER_LEQ
	} CloudOper;

	/*
	// the number of operators using cache
	static int CacheOperNum = 4;

	// the ratio of cache size to the unique table size for each operator
	static int CacheLogRatioDefault[4] = {
	4, // CLOUD_OPER_AND,
	8, // CLOUD_OPER_XOR,
	8, // CLOUD_OPER_BDIFF,
	8 // CLOUD_OPER_LEQ
	};

	// the ratio of cache size to the unique table size for each operator
	static int CacheSize[4] = {
	2, // CLOUD_OPER_AND,
	2, // CLOUD_OPER_XOR,
	2, // CLOUD_OPER_BDIFF,
	2 // CLOUD_OPER_LEQ
	};
	*/

	// data structure definitions
	struct cloudManager // the fast bdd manager
	{
	// variables
	int nVars; // the number of variables allocated
	// bits
	int bitsNode; // the number of bits used for the node
	int bitsCache[4]; // default: bitsNode - CacheSizeRatio[i]
	// shifts
	int shiftUnique; // 8*sizeof(unsigned) - (bitsNode + 1)
	int shiftCache[4]; // 8*sizeof(unsigned) - bitsCache[i]
	// nodes
	int nNodesAlloc; // 2 ^ (bitsNode + 1)
	int nNodesLimit; // 2 ^ bitsNode
	int nNodesCur; // the current number of nodes (including const1 and vars)
	// signature
	CloudSign nSignCur;

	// statistics
	int nMemUsed; // memory usage in bytes
	// cache stats
	int nUniqueHits; // hits in the unique table
	int nUniqueMisses; // misses in the unique table
	int nCacheHits; // hits in the caches
	int nCacheMisses; // misses in the caches
	// the number of steps through the hash table
	int nUniqueSteps;

	// tables
	CloudNode * tUnique; // the unique table to store BDD nodes

	// special nodes
	CloudNode * pNodeStart; // the pointer to the first node
	CloudNode * pNodeEnd; // the pointer to the first node out of the table

	// constants and variables
	CloudNode * one; // the one function
	CloudNode * zero; // the zero function
	CloudNode ** vars; // the elementary variables

	// temporary storage for nodes
	CloudNode ** ppNodes;

	// caches
	CloudCacheEntry2 * tCaches[20]; // caches
	};

	struct cloudNode // representation of the node in the unique table
	{
	CloudSign s; // signature
	CloudVar v; // variable
	CloudNode * e; // negative cofactor
	CloudNode * t; // positive cofactor
	};
	struct cloudCacheEntry1 // one-argument cache
	{
	CloudSign s; // signature
	CloudNode * a; // argument 1
	CloudNode * r; // result
	};
	struct cloudCacheEntry2 // the two-argument cache
	{
	CloudSign s; // signature
	CloudNode * a;
	CloudNode * b;
	CloudNode * r;
	};
	struct cloudCacheEntry3 // the three-argument cache
	{
	CloudSign s; // signature
	CloudNode * a;
	CloudNode * b;
	CloudNode * c;
	CloudNode * r;
	};


	// parameters
	#define CLOUD_NODE_BITS 23

	#define CLOUD_CONST_INDEX ((unsigned)0x0fffffff)
	#define CLOUD_MARK_ON ((unsigned)0x10000000)
	#define CLOUD_MARK_OFF ((unsigned)0xefffffff)

	// hash functions a la Buddy
	#define cloudHashBuddy2(x,y,s) ((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1))
	#define cloudHashBuddy3(x,y,z,s) (cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1))
	// hash functions a la Cudd
	#define DD_P1 12582917
	#define DD_P2 4256249
	#define DD_P3 741457
	#define DD_P4 1618033999
	#define cloudHashCudd2(f,g,s) ((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2) >> (s))
	#define cloudHashCudd3(f,g,h,s) (((((unsigned)(ABC_PTRUINT_T)(f) * DD_P1 + (unsigned)(ABC_PTRUINT_T)(g)) * DD_P2 + (unsigned)(ABC_PTRUINT_T)(h)) * DD_P3) >> (s))

	// node complementation (using node)
	#define Cloud_Regular(p) ((CloudNode*)(((ABC_PTRUINT_T)(p)) & ~01)) // get the regular node (w/o bubble)
	#define Cloud_Not(p) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ 01)) // complement the node
	#define Cloud_NotCond(p,c) ((CloudNode*)(((ABC_PTRUINT_T)(p)) ^ (c))) // complement the node conditionally
	#define Cloud_IsComplement(p) ((int)(((ABC_PTRUINT_T)(p)) & 01)) // check if complemented
	// checking constants (using node)
	#define Cloud_IsConstant(p) (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
	#define cloudIsConstant(p) (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)

	// retrieving values from the node (using node structure)
	#define Cloud_V(p) ((Cloud_Regular(p))->v)
	#define Cloud_E(p) ((Cloud_Regular(p))->e)
	#define Cloud_T(p) ((Cloud_Regular(p))->t)
	// retrieving values from the regular node (using node structure)
	#define cloudV(p) ((p)->v)
	#define cloudE(p) ((p)->e)
	#define cloudT(p) ((p)->t)
	// marking/unmarking (using node structure)
	#define cloudNodeMark(p) ((p)->v \|= CLOUD_MARK_ON)
	#define cloudNodeUnmark(p) ((p)->v &= CLOUD_MARK_OFF)
	#define cloudNodeIsMarked(p) ((int)((p)->v & CLOUD_MARK_ON))

	// cache lookups and inserts (using node)
	#define cloudCacheLookup1(p,sign,f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0))
	#define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0))
	#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0))
	// cache inserts
	#define cloudCacheInsert1(p,sign,f,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r)))
	#define cloudCacheInsert2(p,sign,f,g,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r)))
	#define cloudCacheInsert3(p,sign,f,g,h,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r)))

	//#define CLOUD_ASSERT(p) (assert((p) >= (dd->pNodeStart-1) && (p) < dd->pNodeEnd))
	#define CLOUD_ASSERT(p) assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc)

	////////////////////////////////////////////////////////////////////////
	/// FUNCTION DECLARATIONS ///
	////////////////////////////////////////////////////////////////////////
	// starting/stopping
	extern CloudManager * Cloud_Init( int nVars, int nBits );
	extern void Cloud_Quit( CloudManager * dd );
	extern void Cloud_Restart( CloudManager * dd );
	extern void Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int size );
	extern CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e );
	// support and node count
	extern CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n );
	extern int Cloud_SupportSize( CloudManager * dd, CloudNode * n );
	extern int Cloud_DagSize( CloudManager * dd, CloudNode * n );
	extern int Cloud_DagCollect( CloudManager * dd, CloudNode * n );
	extern int Cloud_SharingSize( CloudManager * dd, CloudNode * * pn, int nn );
	// cubes
	extern CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * n );
	extern void Cloud_bddPrint( CloudManager * dd, CloudNode * Func );
	extern void Cloud_bddPrintCube( CloudManager * dd, CloudNode * Cube );
	// operations
	extern CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g );
	extern CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g );
	// stats
	extern void Cloud_PrintInfo( CloudManager * dd );
	extern void Cloud_PrintHashTable( CloudManager * dd );



	ABC_NAMESPACE_HEADER_END



	#endif

	////////////////////////////////////////////////////////////////////////
	/// END OF FILE ///
	////////////////////////////////////////////////////////////////////////