/**CHeaderFile***************************************************************** FileName [baig.h] PackageName [baig] Synopsis [Binary AND/INVERTER graph] Description [External functions and data strucures of the binary AND/INVERTER graph package] SeeAlso [baigInt.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: baig.h,v 1.29 2009/04/12 00:14:03 fabio Exp $] ******************************************************************************/ #ifndef _BAIG #define _BAIG #include "st.h" #include "ntk.h" #include "bdd.h" #include "mdd.h" #include "sat.h" #include "ctlsp.h" /*Bing:*/ #include "puresat.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #ifndef TRUE #define TRUE 1 #endif #ifndef FALSE #define FALSE 0 #endif #define bAigInvertBit 0x1 /* This bit is set to indicate inverted edge*/ #define bAigArrayMaxSize (1 << 27) /* Maximum size of the node array */ #define ZERO_NODE_INDEX 0 /* Reserve this index for constant Zero node*/ #define bAig_Zero (ZERO_NODE_INDEX) /* Constatnt Zero node */ #define bAig_One (bAig_Not(bAig_Zero)) /* Constatnt One node */ #define bAig_NULL 2 /*Bing*/ #define bAigNodeSize 12 /*8*/ /* Array is used to implement the bAig graph. Each node occupies bAigNodeSize array elements. */ #define bAigFirstNodeIndex bAigNodeSize /* The first node index. */ #define bAig_HashTableSize 481931 #define bAigValue 0 /* Index of the decision level. */ #define bAigFlags 1 /* Index of flag for this node.*/ #define bAigLeft 2 /* Index of the left child */ #define bAigRight 3 /* Index of the right child */ #define bAigNFanout 4 /* Index of number of fanout.*/ #define bAigFanout 5 /* Index of fanout pointer for this node.*/ #define bAigCanonical 6 /* Index of canonical node for this node.*/ #define bAigNext 7 /* Index of dummy for this node.*/ /*Bing:*/ #define bAigClass 8 /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef char nameType_t; typedef long bAigEdge_t; typedef struct bAigManagerStruct bAig_Manager_t; typedef struct bAigTimeFrameStruct bAigTimeFrame_t; /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [And/Inverter graph manager.] Description [] ******************************************************************************/ struct bAigManagerStruct { bAigEdge_t *NodesArray; /* contains pointers to nodes of type bAig_Node_t */ long nodesArraySize; /* contains the current number of nodes */ long maxNodesArraySize; /* Nodes Array maximum size */ bAigEdge_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 (bAig_t) of the binary value encoding for multi-valued variables. */ int allocatedFlags; int *bddIdArray; bdd_t **bddArray; bdd_t **relArray; st_table *id2aig; struct bAigTimeFrameStruct *timeframe; struct bAigTimeFrameStruct *timeframeWOI; struct satLiteralDBStruct *literals; char *dummy; /* Bing: for interpolation */ bAigEdge_t ** HashTableArray; st_table ** SymbolTableArray; int NumOfTable; int class_; /* one is C1, 2 is C2 or for multiCut it is the timeframe */ IP_Manager_t * ipm; satArray_t * assertArray; bAigEdge_t InitState, IPState; /*RTree_t *root;*/ int IP,test2LevelMini; satArray_t * assertArray2, *EqArray, *CoiAssertArray; }; /**Struct********************************************************************** Synopsis [A struct to save unrolled system] ******************************************************************************/ struct bAigTimeFrameStruct { 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 */ bAigEdge_t **inputs; /* the array to save input of each unrolled timeframe */ bAigEdge_t **outputs; /* the array to save output of each unrolled timeframe */ bAigEdge_t **latchInputs; /* the array to save latch input of each unrolled timeframe */ bAigEdge_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. */ bAigEdge_t *oriLatchInputs; /* the array to save latch input of original system */ bAigEdge_t *oribLatchInputs; /* the array to save latch input of original system */ bAigEdge_t *oriInputs; /* the array to save input of original system */ bAigEdge_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 */ bAigEdge_t **binputs; /* the array to save input bit of each unrolled timeframe */ bAigEdge_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 bAigTransitionStruct bAigTransition_t; struct bAigTransitionStruct { Ntk_Network_t *network; bAig_Manager_t *manager; satManager_t *allsat; /** to save the sat manager for allsat process **/ satManager_t *lifting; /** to save the sat manager for lifting process **/ int nInputs; int nLatches; bAigEdge_t objective; bAigEdge_t *inputs; bAigEdge_t *cstates; bAigEdge_t *nstates; bAigEdge_t *initials; bAigEdge_t *n2c; bAigEdge_t *c2n; bAigEdge_t *cobj; int csize; int istates; bAigEdge_t *tstates; bAigEdge_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; struct satArrayStruct *unassigned; struct satArrayStruct *tVariables; struct satArrayStruct *auxObj; struct satArrayStruct *objArr; /** to save the next state variable used to build objective */ struct satArrayStruct *reached; struct satArrayStruct *frontier; struct satArrayStruct *originalFrontier; 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 [Returns the class of a node] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ /*Bing:*/ #define bAig_Class(node) (\ manager->NodesArray[bAig_NonInvertedEdge(node)+bAigClass]\ ) /**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 [] ******************************************************************************/ #define bAig_Not(node) ( \ (bAigEdge_t) ((node) ^ (bAigInvertBit)) \ ) /**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 bAig_NonInvertedEdge(edge) ( \ (edge) & ~(bAigInvertBit) \ ) /**Macro*********************************************************************** Synopsis [Returns true if the edge is inverted.] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define bAig_IsInverted(edge) ( \ (edge) & (bAigInvertBit) \ ) /**Macro*********************************************************************** Synopsis [Return right child of aig node] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define rightChild(node)(\ (manager->NodesArray[bAig_NonInvertedEdge(node)+bAigRight])\ ) /**Macro*********************************************************************** Synopsis [Return left child of aig node] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define leftChild(node)(\ (manager->NodesArray[bAig_NonInvertedEdge(node)+bAigLeft])\ ) /**Macro*********************************************************************** Synopsis [] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define fanout(node)(\ manager->NodesArray[bAig_NonInvertedEdge(node)+bAigFanout]\ ) /**Macro*********************************************************************** Synopsis [] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define nFanout(node)(\ manager->NodesArray[bAig_NonInvertedEdge(node)+bAigNFanout]\ ) /**Macro*********************************************************************** Synopsis [] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define flags(node)(\ manager->NodesArray[bAig_NonInvertedEdge(node)+bAigFlags]\ ) /**Macro*********************************************************************** Synopsis [] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define canonical(node)(\ manager->NodesArray[bAig_NonInvertedEdge(node)+bAigCanonical]\ ) /**Macro*********************************************************************** Synopsis [return next of aig] Description [This is used to build hash table for structural hashing] SideEffects [none] SeeAlso [] ******************************************************************************/ #define next(node)(\ manager->NodesArray[bAig_NonInvertedEdge(node)+bAigNext]\ ) /**Macro*********************************************************************** Synopsis [return value of aig node] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define aig_value(node)(\ (manager->NodesArray[bAig_NonInvertedEdge(node)+bAigValue])\ ) /**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 bAigNodeSize.] SideEffects [none] SeeAlso [] ******************************************************************************/ /*#define bAigNodeID(edge)(\ bAig_NonInvertedEdge(edge)>>3 \ )*/ /*Bing:*/ #define bAigNodeID(edge)(\ bAig_NonInvertedEdge(edge)/bAigNodeSize \ ) /**Macro*********************************************************************** Synopsis [Hash function for the hash table.] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define HashTableFunction(left, right) \ ( (bAigEdge_t)\ ((( (bAigEdge_t) (left)) << 3) + \ (( (bAigEdge_t) (right)) << 3)) % bAig_HashTableSize \ ) /**Macro*********************************************************************** Synopsis [Traverse fanout of AIG ] Description [] SideEffects [none] SeeAlso [] ******************************************************************************/ #define bAigEdgeForEachFanout( \ manager, /* bAig_Manager_t */ \ v, /* bAigEdge_t */ \ cur, /* bAigEdge_t for fanout */ \ ii, \ iii, \ pfan \ ) \ for(ii=0, iii=nFanout(v), pfan=(bAigEdge_t *)fanout(v); \ (ii