/**CHeaderFile***************************************************************** FileName [Aig.h] PackageName [Aig] Synopsis [Binary AND/INVERTER graph] Description [External functions and data strucures of the binary AND/INVERTER graph package] SeeAlso [AigInt.h] Author [Mohammad Awedh] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] Revision [$Id: aig.h,v 1.1.1.1 2008-11-14 20:40:11 hhkim Exp $] ******************************************************************************/ #ifndef _AIG #define _AIG #ifdef __cplusplus extern "C" { #endif #include #include #include #include "st.h" #include "util.h" #include "array.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #ifndef TRUE #define TRUE 1 #endif #ifndef FALSE #define FALSE 0 #endif #define AigInvertBit 0x1 /* This bit is set to indicate inverted edge*/ #define AigArrayMaxSize (1 << 27) /* Maximum size of the node array */ #define ZERO_NODE_INDEX 0 /* Reserve this index for constant Zero node*/ #define Aig_Zero (ZERO_NODE_INDEX) /* Constatnt Zero node */ #define Aig_One (Aig_Not(Aig_Zero)) /* Constatnt One node */ #define Aig_NULL 2 /* Bing */ #define AigNodeSize 8 /* Array is used to implement the Aig graph. Each node occupies AigNodeSize array elements. */ #define AigFirstNodeIndex AigNodeSize /* The first node index. */ #define Aig_HashTableSize 481931 #define AigValue 0 /* Index of the decision level. */ #define AigFlags 1 /* Index of flag for this node.*/ #define AigLeft 2 /* Index of the left child */ #define AigRight 3 /* Index of the right child */ #define AigNFanout 4 /* Index of number of fanout.*/ #define AigFanout 5 /* Index of fanout pointer for this node.*/ #define AigCanonical 6 /* Index of canonical node for this node.*/ #define AigNext 7 /* Index of dummy for this node.*/ /* Bing */ #define AigClass 8 /** * If AIG nodes are identified as equivalent node, then they are merged * into one of them. This mask bit is used identified the representative * of those equivalent nodes. **/ #define CanonicalBitMask 0x00020000 #define ResetCanonicalBitMask ~0x00020000L /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef char nameType_t; typedef long AigEdge_t; typedef struct AigManagerStruct Aig_Manager_t; typedef struct AigTimeFrameStruct AigTimeFrame_t; /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [And/Inverter graph manager.] Description [] ******************************************************************************/ struct AigManagerStruct { AigEdge_t *NodesArray; /* contains pointers to nodes of type Aig_Node_t */ long nodesArraySize; /* contains the current number of nodes */ long maxNodesArraySize; /* Nodes Array maximum size */ AigEdge_t *HashTable; /* Hash table */ st_table *SymbolTable; /* Symbol table to store variables and their indices */ char **nameList; /* This table contains the name of each node. nodeID is used to access the node's name. */ array_t *mVarList; /* List of mVarId of each variable */ array_t *bVarList; /* List of bVardId (Aig_t) of the binary value encoding for multi-valued variables. */ int allocatedFlags; st_table *id2aig; struct AigTimeFrameStruct *timeframe; struct AigTimeFrameStruct *timeframeWOI; char *dummy; /* Bing: for interpolation */ AigEdge_t ** HashTableArray; st_table ** SymbolTableArray; int NumOfTable; int cls; /* one is C1, 2 is C2 or for multiCut it is the timeframe; */ AigEdge_t InitState, IPState; int IP,test2LevelMini; }; /**Struct********************************************************************** Synopsis [A struct to save unrolled system] ******************************************************************************/ struct AigTimeFrameStruct { int nInputs; /* the number of inputs */ int nOutputs; /* the number of outputs */ int nLatches; /* the number of latchs */ int nInternals; /* the numebr of internal nodes */ int currentTimeframe; /* the number of unrolled timeframe */ AigEdge_t **inputs; /* the array to save input of each unrolled timeframe */ AigEdge_t **outputs; /* the array to save output of each unrolled timeframe */ AigEdge_t **latchInputs; /* the array to save latch input of each unrolled timeframe */ AigEdge_t **internals; /* the array to save internal node of each unrolled timeframe */ /* we need this array to build property */ /* based on internal node, there might be */ /* the way to improve this. */ AigEdge_t *oriLatchInputs; /* the array to save latch input of original system */ AigEdge_t *oribLatchInputs; /* the array to save latch input of original system */ AigEdge_t *oriInputs; /* the array to save input of original system */ AigEdge_t *oribInputs; /* the array to save input of original system */ st_table *li2index; /* It maps the latch input aig to index which can identify i'th latch input through latchInputs[i][index] */ st_table *o2index; /* It maps the output aig to index which can identify i'th latch input through outputs[i][index] */ st_table *i2index; /* It maps the input aig to index which can identify i'th latch input through inputs[i][index] */ st_table *pi2index; /* It maps the input aig to index which can identify i'th latch input through inputs[i][index] */ array_t *latchArr; array_t *inputArr; array_t *outputArr; array_t *iindexArray; array_t *assertedArray; int nbInputs; /* the number of input bits */ int nbLatches; /* the number of latche bits */ AigEdge_t **binputs; /* the array to save input bit of each unrolled timeframe */ AigEdge_t **blatchInputs; /* the array to save latch input bit of each unrolled timeframe */ st_table *bli2index; /* It maps the latch input bit of aig to index which can identify i'th latch input through blatchInputs[i][index] */ st_table *bpi2index; /* It maps the input bit of aig to index which can identify i'th latch input through binputs[i][index] */ /* Bing */ st_table *libli2eq; st_table *idx2name; st_table *MultiLatchTable; /* stores var corresponding to multiple latches */ }; /**Struct********************************************************************** Synopsis [A struct to save transition relation of AIG ] ******************************************************************************/ typedef struct AigTransitionStruct AigTransition_t; struct AigTransitionStruct { Aig_Manager_t *manager; int nInputs; int nLatches; AigEdge_t objective; AigEdge_t *inputs; AigEdge_t *cstates; AigEdge_t *nstates; AigEdge_t *initials; AigEdge_t *n2c; AigEdge_t *c2n; AigEdge_t *cobj; int csize; int istates; AigEdge_t *tstates; AigEdge_t *coiStates; /* to identified the next states variables in froniter set **/ int *vinputs; /** to save the value of primary inputs **/ int *vtstates; /** to save the value of tstates variable during lifting **/ int objValue; int latestBlockingClause; int iteration; int avgLits; int sum; int period; int interval; int nBlocked; int method; int interface; int inclusionInitial; int constrain; int verbose; int reductionUsingUnsat; int disableLifting; }; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Macro*********************************************************************** Synopsis [Performs the 'Not' Logical operator] Description [This macro inverts the edge going to a node which corresponds to NOT operator] SideEffects [none] SeeAlso [] ******************************************************************************/ /* Bing */ #define Aig_Class(node) (\ bm->NodesArray[Aig_NonInvertedEdge(node)+AigClass]\ ) #define Aig_Not(node) ( \ (AigEdge_t) ((node) ^ (AigInvertBit)) \ ) /**Macro*********************************************************************** Synopsis [Returns the non inverted edge.] Description [This macro returns the non inverted edge. It clears the least significant bit of the edge if it is set.] SideEffects [none] SeeAlso [] ******************************************************************************/ #define Aig_NonInvertedEdge(edge) ( \ (edge) & ~(AigInvertBit) \ ) /**Macro*********************************************************************** Synopsis [Returns true if the edge is inverted.] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define Aig_IsInverted(edge) ( \ (edge) & (AigInvertBit) \ ) /**Macro*********************************************************************** Synopsis [Return right child of aig node] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define rightChild(node)(\ (bm->NodesArray[Aig_NonInvertedEdge(node)+AigRight])\ ) /**Macro*********************************************************************** Synopsis [Return left child of aig node] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define leftChild(node)(\ (bm->NodesArray[Aig_NonInvertedEdge(node)+AigLeft])\ ) /**Macro*********************************************************************** Synopsis [] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define fanout(node)(\ bm->NodesArray[Aig_NonInvertedEdge(node)+AigFanout]\ ) /**Macro*********************************************************************** Synopsis [] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define nFanout(node)(\ bm->NodesArray[Aig_NonInvertedEdge(node)+AigNFanout]\ ) /**Macro*********************************************************************** Synopsis [] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define flags(node)(\ bm->NodesArray[Aig_NonInvertedEdge(node)+AigFlags]\ ) /**Macro*********************************************************************** Synopsis [] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define canonical(node)(\ bm->NodesArray[Aig_NonInvertedEdge(node)+AigCanonical]\ ) /**Macro*********************************************************************** Synopsis [return next of aig] Description [This is used to build hash table for structural hashing] SideEffects [none] SeeAlso [] ******************************************************************************/ #define aig_next(node)(\ bm->NodesArray[Aig_NonInvertedEdge(node)+AigNext]\ ) /**Macro*********************************************************************** Synopsis [return value of aig node] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define aig_value(node)(\ (bm->NodesArray[Aig_NonInvertedEdge(node)+AigValue])\ ) /**Macro*********************************************************************** Synopsis [The node ID] Description [Node ID is a unique number for each node and can be found by dividing the edge going to this node by AigNodeSize.] SideEffects [none] SeeAlso [] ******************************************************************************/ /*#define AigNodeID(edge)(\ Aig_NonInvertedEdge(edge)>>3 \ )*/ /* Bing */ #define AigNodeID(edge)(\ Aig_NonInvertedEdge(edge)/AigNodeSize \ ) /**Macro*********************************************************************** Synopsis [Hash function for the hash table.] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #if 1 #if 1 #define HashTableFunction(left, right) \ ( (AigEdge_t) \ ((( (AigEdge_t) (left)) << 3) + \ (( (AigEdge_t) (right)) << 3)) % Aig_HashTableSize \ ) #else #define HashTableFunction(left, right) \ ((AigEdge_t) \ ((((((AigEdge_t) (left)) + (((AigEdge_t) (left)) << 5)) ^ \ (((AigEdge_t) (right)) + (((AigEdge_t) (right)) << 5)) + left ) % Aig_HashTableSize \ ))) #endif #else #define HashTableFunction(left, right) \ ( (AigEdge_t) \ ((( (AigEdge_t) (left)) + (( (AigEdge_t) (left)) << 5)) ^ \ (( (AigEdge_t) (right)) + (( (AigEdge_t) (right)) << 5)) + \ left ) % Aig_HashTableSize \ ) #endif /**Macro*********************************************************************** Synopsis [Traverse fanout of AIG ] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define AigEdgeForEachFanout( \ manager, /* Aig_Manager_t */ \ v, /* AigEdge_t */ \ cur, /* AigEdge_t for fanout */ \ ii, \ iii, \ pfan \ ) \ for(ii=0, iii=nFanout(v), pfan=(AigEdge_t *)fanout(v); \ (ii