summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aig.h33
-rw-r--r--src/aig/aig/aigCheck.c16
-rw-r--r--src/aig/aig/aigDfs.c37
-rw-r--r--src/aig/aig/aigMan.c196
-rw-r--r--src/aig/aig/aigObj.c17
-rw-r--r--src/aig/aig/aigOper.c98
-rw-r--r--src/aig/aig/aigRetF.c12
-rw-r--r--src/aig/aig/aigSeq.c502
-rw-r--r--src/aig/aig/aigShow.c12
-rw-r--r--src/aig/aig/aigTable.c34
-rw-r--r--src/aig/aig/module.make1
-rw-r--r--src/aig/dar/darBalance.c456
-rw-r--r--src/aig/dar/darScript.c8
-rw-r--r--src/aig/fra/fraCore.c1
-rw-r--r--src/aig/fra/fraInd.c1
-rw-r--r--src/aig/fra/fraLcr.c1
-rw-r--r--src/aig/hop/hopTruth.c8
17 files changed, 521 insertions, 912 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 8a61a530..f58ba409 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -47,7 +47,6 @@ extern "C" {
typedef struct Aig_Man_t_ Aig_Man_t;
typedef struct Aig_Obj_t_ Aig_Obj_t;
-typedef struct Aig_Box_t_ Aig_Box_t;
typedef struct Aig_MmFixed_t_ Aig_MmFixed_t;
typedef struct Aig_MmFlex_t_ Aig_MmFlex_t;
typedef struct Aig_MmStep_t_ Aig_MmStep_t;
@@ -61,9 +60,7 @@ typedef enum {
AIG_OBJ_BUF, // 4: buffer node
AIG_OBJ_AND, // 5: AND node
AIG_OBJ_EXOR, // 6: EXOR node
- AIG_OBJ_LATCH, // 7: latch
- AIG_OBJ_BOX, // 8: latch
- AIG_OBJ_VOID // 9: unused object
+ AIG_OBJ_VOID // 7: unused object
} Aig_Type_t;
// the AIG node
@@ -73,11 +70,11 @@ struct Aig_Obj_t_ // 8 words
Aig_Obj_t * pFanin0; // fanin
Aig_Obj_t * pFanin1; // fanin
Aig_Obj_t * pHaig; // pointer to the HAIG node
- unsigned int Type : 4; // object type
+ unsigned int Type : 3; // object type
unsigned int fPhase : 1; // value under 000...0 pattern
unsigned int fMarkA : 1; // multipurpose mask
unsigned int fMarkB : 1; // multipurpose mask
- unsigned int nRefs : 25; // reference count
+ unsigned int nRefs : 26; // reference count
unsigned Level : 24; // the level of this node
unsigned nCuts : 8; // the number of cuts
int TravId; // unique ID of last traversal involving the node
@@ -89,16 +86,6 @@ struct Aig_Obj_t_ // 8 words
};
};
-// the AIG box
-struct Aig_Box_t_
-{
- int nInputs; // the number of box inputs (POs)
- int i1Input; // the first PO of the interval
- int nOutputs; // the number of box outputs (PIs)
- int i1Output; // the first PI of the interval
- float ** pTable; // the delay table of the box
-};
-
// the AIG manager
struct Aig_Man_t_
{
@@ -154,7 +141,6 @@ struct Aig_Man_t_
Vec_Ptr_t * vMapped;
Vec_Int_t * vFlopNums;
void * pSeqModel;
- Aig_Man_t * pManHaig;
Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots;
// timing statistics
@@ -265,7 +251,6 @@ static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nO
static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; }
static inline int Aig_ManAndNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]; }
static inline int Aig_ManExorNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_EXOR]; }
-static inline int Aig_ManLatchNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_LATCH]; }
static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; }
@@ -289,10 +274,9 @@ static inline int Aig_ObjIsPo( Aig_Obj_t * pObj ) { return pObj-
static inline int Aig_ObjIsBuf( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_BUF; }
static inline int Aig_ObjIsAnd( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND; }
static inline int Aig_ObjIsExor( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_EXOR; }
-static inline int Aig_ObjIsLatch( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_LATCH; }
static inline int Aig_ObjIsNode( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1; }
-static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR || pObj->Type == AIG_OBJ_LATCH; }
+static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; }
static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; }
@@ -405,6 +389,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
// iterator over all nodes
#define Aig_ManForEachNode( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
+// iterator over all nodes
+#define Aig_ManForEachExor( p, pObj, i ) \
+ Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
// iterator over the nodes whose IDs are stored in the array
#define Aig_ManForEachNodeVec( p, vIds, pObj, i ) \
for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
@@ -458,6 +445,7 @@ extern Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLea
extern void Aig_ManCutStop( Aig_ManCut_t * p );
/*=== aigDfs.c ==========================================================*/
extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p );
+extern Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p );
@@ -514,7 +502,6 @@ extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_O
extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i );
extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
extern Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
-extern Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne );
extern Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
extern Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
extern Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 );
@@ -564,9 +551,7 @@ extern Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
extern int Aig_ManSeqCleanup( Aig_Man_t * p );
extern int Aig_ManCountMergeRegs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
-extern void Aig_ManComputeSccs( Aig_Man_t * p );
-/*=== aigSeq.c ========================================================*/
-extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
+extern void Aig_ManComputeSccs( Aig_Man_t * p );
/*=== aigShow.c ========================================================*/
extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
/*=== aigTable.c ========================================================*/
diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c
index 8c53e635..bddc9288 100644
--- a/src/aig/aig/aigCheck.c
+++ b/src/aig/aig/aigCheck.c
@@ -90,23 +90,23 @@ int Aig_ManCheck( Aig_Man_t * p )
}
// count the total number of nodes
if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) +
- Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
+ Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) )
{
printf( "Aig_ManCheck: The number of created nodes is wrong.\n" );
- printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",
- 1, Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManBufNum(p), Aig_ManAndNum(p), Aig_ManExorNum(p), Aig_ManLatchNum(p),
- 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) );
+ printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Total = %d.\n",
+ 1, Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManBufNum(p), Aig_ManAndNum(p), Aig_ManExorNum(p),
+ 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) );
printf( "Created = %d. Deleted = %d. Existing = %d.\n",
p->nCreated, p->nDeleted, p->nCreated - p->nDeleted );
return 0;
}
// count the number of nodes in the table
- if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
+ if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) )
{
printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
- printf( "Entries = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",
- Aig_TableCountEntries(p), Aig_ManAndNum(p), Aig_ManExorNum(p), Aig_ManLatchNum(p),
- Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) );
+ printf( "Entries = %d. And = %d. Xor = %d. Total = %d.\n",
+ Aig_TableCountEntries(p), Aig_ManAndNum(p), Aig_ManExorNum(p),
+ Aig_ManAndNum(p) + Aig_ManExorNum(p) );
return 0;
}
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 5681f689..aebe6c95 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -78,11 +78,6 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
Aig_ManForEachPi( p, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
- // if there are latches, mark them
- if ( Aig_ManLatchNum(p) > 0 )
- Aig_ManForEachObj( p, pObj, i )
- if ( Aig_ObjIsLatch(pObj) )
- Aig_ObjSetTravIdCurrent( p, pObj );
// go through the nodes
vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
Aig_ManForEachObj( p, pObj, i )
@@ -93,6 +88,32 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
/**Function*************************************************************
+ Synopsis [Levelizes the nodes
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ Vec_Vec_t * vLevels;
+ int nLevels, i;
+ nLevels = Aig_ManLevelNum( p );
+ vLevels = Vec_VecStart( nLevels + 1 );
+ Aig_ManForEachNode( p, pObj, i )
+ {
+ assert( (int)pObj->Level <= nLevels );
+ Vec_VecPush( vLevels, pObj->Level, pObj );
+ }
+ return vLevels;
+}
+
+/**Function*************************************************************
+
Synopsis [Collects internal nodes in the DFS order.]
Description []
@@ -130,7 +151,6 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
Vec_Ptr_t * vNodes;
// Aig_Obj_t * pObj;
int i;
- assert( Aig_ManLatchNum(p) == 0 );
Aig_ManIncrementTravId( p );
// mark constant and PIs
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
@@ -245,11 +265,6 @@ Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
// mark POs
Aig_ManForEachPo( p, pObj, i )
Aig_ObjSetTravIdCurrent( p, pObj );
- // if there are latches, mark them
- if ( Aig_ManLatchNum(p) > 0 )
- Aig_ManForEachObj( p, pObj, i )
- if ( Aig_ObjIsLatch(pObj) )
- Aig_ObjSetTravIdCurrent( p, pObj );
// go through the nodes
vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
Aig_ManForEachObj( p, pObj, i )
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 665401c3..95bacf8a 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -102,6 +102,8 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
return pNew;
}
+//#if 0
+
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
@@ -122,7 +124,7 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
if ( Aig_ObjIsBuf(pObj) )
return pObj->pData = Aig_ObjChild0Copy(pObj);
Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
- pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
return pObj->pData = pObjNew;
}
@@ -148,7 +150,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
- pNew->pManHaig = p->pManHaig;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// create the PIs
@@ -164,7 +165,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
}
else if ( Aig_ObjIsNode(pObj) )
{
- pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
}
else if ( Aig_ObjIsPi(pObj) )
{
@@ -187,6 +188,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
}
else
{
+/*
+
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachObj( p, pObj, i )
@@ -207,13 +210,73 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
pObj->pData = pObjNew;
}
}
+*/
+ Vec_Vec_t * vLevels;
+ int k;
+
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+ Aig_ManForEachPi( p, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePi( pNew );
+ pObjNew->pHaig = pObj->pHaig;
+ pObjNew->Level = pObj->Level;
+ pObj->pData = pObjNew;
+ }
+
+ vLevels = Aig_ManLevelize( p );
+ Vec_VecForEachEntry( vLevels, pObj, i, k )
+ {
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ Vec_VecFree( vLevels );
+
+ // add the POs
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ pObjNew->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+
+
+/*
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ pObjNew = Aig_ObjCreatePi( pNew );
+ pObjNew->Level = pObj->Level;
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+// pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ else if ( Aig_ObjIsConst1(pObj) )
+ {
+ pObjNew = Aig_ManConst1(pNew);
+ }
+ else
+ {
+ pObjNew = Aig_ManDup_rec( pNew, p, pObj );
+ }
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ // add the POs
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ pObjNew->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+*/
}
// add the POs
- assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
- // pass the HAIG to the new AIG
- p->pManHaig = NULL;
- Aig_ManForEachObj( p, pObj, i )
- pObj->pHaig = NULL;
+// assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -223,6 +286,117 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
return pNew;
}
+//#endif
+
+#if 0
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager recursively.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pObjNew;
+ if ( pObj->pData )
+ return pObj->pData;
+ Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
+ if ( Aig_ObjIsBuf(pObj) )
+ return pObj->pData = Aig_ObjChild0Copy(pObj);
+ Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ return pObj->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int i;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->nRegs = p->nRegs;
+ pNew->nAsserts = p->nAsserts;
+ if ( p->vFlopNums )
+ pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+ // create the PIs
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+ Aig_ManForEachPi( p, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePi( pNew );
+ pObjNew->pHaig = pObj->pHaig;
+ pObjNew->Level = pObj->Level;
+ pObj->pData = pObjNew;
+ }
+ // duplicate internal nodes
+ if ( fOrdered )
+ {
+ Aig_ManForEachObj( p, pObj, i )
+ if ( Aig_ObjIsBuf(pObj) )
+ {
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ }
+ else if ( Aig_ObjIsNode(pObj) )
+ {
+ pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ }
+ }
+ else
+ {
+ Aig_ManForEachObj( p, pObj, i )
+ if ( !Aig_ObjIsPo(pObj) )
+ {
+ Aig_ManDup_rec( pNew, p, pObj );
+ assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+ }
+ }
+ // add the POs
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ pObjNew->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+/*
+ printf( "PIs : " );
+ Aig_ManForEachPi( p, pObj, i )
+ printf( "%d ", pObj->Id );
+ printf( "\n" );
+ printf( "PIs : " );
+ Aig_ManForEachPo( p, pObj, i )
+ printf( "%d ", pObj->Id );
+ printf( "\n" );
+*/
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDup(): The check has failed.\n" );
+ return pNew;
+}
+
+#endif
+
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
@@ -252,7 +426,7 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
{
assert( !Aig_ObjIsBuf(pObj) );
if ( Aig_ObjIsNode(pObj) )
- pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
}
return pNew;
}
@@ -311,8 +485,6 @@ void Aig_ManStop( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
- if ( p->pManHaig )
- Aig_ManStop( p->pManHaig );
if ( p->vMapped )
Vec_PtrFree( p->vMapped );
// print time
@@ -412,7 +584,7 @@ int Aig_ManHaigCounter( Aig_Man_t * pAig )
void Aig_ManPrintStats( Aig_Man_t * p )
{
int nChoices = Aig_ManCountChoices(p);
- printf( "PI/PO/Lat = %5d/%5d/%5d ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
+ printf( "PI/PO = %5d/%5d ", Aig_ManPiNum(p), Aig_ManPoNum(p) );
printf( "A = %7d. ", Aig_ManAndNum(p) );
printf( "Eq = %7d. ", Aig_ManHaigCounter(p) );
if ( nChoices )
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 734f1277..2f92f720 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -88,7 +88,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
Aig_Obj_t * pObj;
assert( !Aig_IsComplement(pGhost) );
assert( Aig_ObjIsHash(pGhost) );
-// assert( pGhost == &p->Ghost );
+ assert( pGhost == &p->Ghost );
// get memory for the new object
pObj = Aig_ManFetchMemory( p );
pObj->Type = pGhost->Type;
@@ -97,14 +97,6 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
// update node counters of the manager
p->nObjs[Aig_ObjType(pObj)]++;
assert( pObj->pData == NULL );
-/*
- if ( p->pManHaig )
- {
- pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
- pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
- pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
- }
-*/
return pObj;
}
@@ -374,13 +366,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
// make sure object is not pointing to itself
assert( pObjOld != Aig_ObjFanin0(pObjNewR) );
assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
- // map the HAIG nodes
- if ( p->pManHaig != NULL )
- {
- assert( pObjNewR->pHaig != NULL );
- assert( pObjNewR->pHaig->pHaig == NULL );
- pObjNewR->pHaig->pHaig = pObjOld->pHaig;
- }
// recursively delete the old node - but leave the object there
pObjNewR->nRefs++;
Aig_ObjDelete_rec( p, pObjOld, 0 );
diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c
index c19f551e..6e9d37ba 100644
--- a/src/aig/aig/aigOper.c
+++ b/src/aig/aig/aigOper.c
@@ -89,43 +89,6 @@ Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t
/**Function*************************************************************
- Synopsis [Creates the canonical form of the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Obj_t * Aig_CanonPair_rec( Aig_Man_t * p, Aig_Obj_t * pGhost )
-{
- Aig_Obj_t * pResult, * pLat0, * pLat1;
- int fCompl0, fCompl1;
- Aig_Type_t Type;
- assert( Aig_ObjIsNode(pGhost) );
- // consider the case when the pair is canonical
- if ( !Aig_ObjIsLatch(Aig_ObjFanin0(pGhost)) || !Aig_ObjIsLatch(Aig_ObjFanin1(pGhost)) )
- {
- if ( (pResult = Aig_TableLookup( p, pGhost )) )
- return pResult;
- return Aig_ObjCreate( p, pGhost );
- }
- /// remember the latches
- pLat0 = Aig_ObjFanin0(pGhost);
- pLat1 = Aig_ObjFanin1(pGhost);
- // remember type and compls
- Type = Aig_ObjType(pGhost);
- fCompl0 = Aig_ObjFaninC0(pGhost);
- fCompl1 = Aig_ObjFaninC1(pGhost);
- // call recursively
- pResult = Aig_Oper( p, Aig_NotCond(Aig_ObjChild0(pLat0), fCompl0), Aig_NotCond(Aig_ObjChild0(pLat1), fCompl1), Type );
- // build latch on top of this
- return Aig_Latch( p, pResult, (Type == AIG_OBJ_AND)? fCompl0 & fCompl1 : fCompl0 ^ fCompl1 );
-}
-
-/**Function*************************************************************
-
Synopsis [Performs canonicization step.]
Description [The argument nodes can be complemented.]
@@ -138,16 +101,7 @@ Aig_Obj_t * Aig_CanonPair_rec( Aig_Man_t * p, Aig_Obj_t * pGhost )
Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
{
Aig_Obj_t * pGhost, * pResult;
-// Aig_Obj_t * pFan0, * pFan1;
- if ( p->pTable == NULL )
- {
-// pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
- pGhost = Aig_ManGhost(p);
- pGhost->Type = AIG_OBJ_AND;
- pGhost->pFanin0 = p0;
- pGhost->pFanin1 = p1;
- return Aig_ObjCreate( p, pGhost );
- }
+ Aig_Obj_t * pFan0, * pFan1;
// check trivial cases
if ( p0 == p1 )
return p0;
@@ -241,32 +195,12 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
}
}
// check if it can be an EXOR gate
-// if ( Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
-// return Aig_Exor( p, pFan0, pFan1 );
+ if ( p->fCatchExor && Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
+ return Aig_Exor( p, pFan0, pFan1 );
pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
- pResult = Aig_CanonPair_rec( p, pGhost );
- return pResult;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the canonical form of the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne )
-{
- Aig_Obj_t * pGhost, * pResult;
- pGhost = Aig_ObjCreateGhost( p, Aig_NotCond(pObj, fInitOne), NULL, AIG_OBJ_LATCH );
- pResult = Aig_TableLookup( p, pGhost );
- if ( pResult == NULL )
- pResult = Aig_ObjCreate( p, pGhost );
- return Aig_NotCond( pResult, fInitOne );
+ if ( (pResult = Aig_TableLookup( p, pGhost )) )
+ return pResult;
+ return Aig_ObjCreate( p, pGhost );
}
/**Function*************************************************************
@@ -282,8 +216,8 @@ Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne )
***********************************************************************/
Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
{
-/*
Aig_Obj_t * pGhost, * pResult;
+ int fCompl;
// check trivial cases
if ( p0 == p1 )
return Aig_Not(p->pConst1);
@@ -293,13 +227,19 @@ Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
return Aig_NotCond( p1, p0 == p->pConst1 );
if ( Aig_Regular(p1) == p->pConst1 )
return Aig_NotCond( p0, p1 == p->pConst1 );
- // check the table
+ // when there is no special XOR gates
+ if ( !p->fCatchExor )
+ return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
+ // canonicize
+ fCompl = Aig_IsComplement(p0) ^ Aig_IsComplement(p1);
+ p0 = Aig_Regular(p0);
+ p1 = Aig_Regular(p1);
pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_EXOR );
+ // check the table
if ( pResult = Aig_TableLookup( p, pGhost ) )
- return pResult;
- return Aig_ObjCreate( p, pGhost );
-*/
- return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
+ return Aig_NotCond( pResult, fCompl );
+ pResult = Aig_ObjCreate( p, pGhost );
+ return Aig_NotCond( pResult, fCompl );
}
/**Function*************************************************************
@@ -331,7 +271,7 @@ Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
***********************************************************************/
Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 )
{
-/*
+/*
Aig_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
int Count0, Count1;
// consider trivial cases
diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c
index 4318be9d..e52283b1 100644
--- a/src/aig/aig/aigRetF.c
+++ b/src/aig/aig/aigRetF.c
@@ -178,18 +178,6 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
p->nObjs[AIG_OBJ_BUF]++;
Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL );
// create HAIG if defined
-/*
- if ( p->pManHaig )
- {
- // create HAIG latch
- pObjLo->pHaig = Aig_ObjCreatePi( p->pManHaig );
- pObjLi->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( Aig_ObjChild0(pObjLi) ) );
- // create equivalence class
- assert( pObjLo->pHaig != NULL );
- assert( pObjLo->pHaig->pHaig == NULL );
- pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig);
- }
-*/
// mark the change
fChange = 1;
// check the limit
diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c
deleted file mode 100644
index daafeab1..00000000
--- a/src/aig/aig/aigSeq.c
+++ /dev/null
@@ -1,502 +0,0 @@
-/**CFile****************************************************************
-
- FileName [aigSeq.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [AIG package.]
-
- Synopsis [Sequential strashing.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - April 28, 2007.]
-
- Revision [$Id: aigSeq.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Converts combinational AIG manager into a sequential one.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits )
-{
- Aig_Obj_t * pObjLi, * pObjLo, * pLatch;
- int i;
- assert( Vec_PtrSize( p->vBufs ) == 0 );
- // collect the POs to be converted into latches
- for ( i = 0; i < nLatches; i++ )
- {
- // get the corresponding PI/PO pair
- pObjLi = Aig_ManPo( p, Aig_ManPoNum(p) - nLatches + i );
- pObjLo = Aig_ManPi( p, Aig_ManPiNum(p) - nLatches + i );
- // create latch
- pLatch = Aig_Latch( p, Aig_ObjChild0(pObjLi), pInits? pInits[i] : 0 );
- // recycle the old PO object
- Aig_ObjDisconnect( p, pObjLi );
- Vec_PtrWriteEntry( p->vObjs, pObjLi->Id, NULL );
- Aig_ManRecycleMemory( p, pObjLi );
- // convert the corresponding PI to be a buffer and connect it to the latch
- pObjLo->Type = AIG_OBJ_BUF;
- Aig_ObjConnect( p, pObjLo, pLatch, NULL );
- // save the buffer
-// Vec_PtrPush( p->vBufs, pObjLo );
- }
- // shrink the arrays
- Vec_PtrShrink( p->vPis, Aig_ManPiNum(p) - nLatches );
- Vec_PtrShrink( p->vPos, Aig_ManPoNum(p) - nLatches );
- // update the counters of different objects
- p->nObjs[AIG_OBJ_PI] -= nLatches;
- p->nObjs[AIG_OBJ_PO] -= nLatches;
- p->nObjs[AIG_OBJ_BUF] += nLatches;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects internal nodes in the DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManDfsSeq_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
- assert( !Aig_IsComplement(pObj) );
- if ( pObj == NULL )
- return;
- if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
- return;
- Aig_ObjSetTravIdCurrent( p, pObj );
- if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
- return;
- Aig_ManDfsSeq_rec( p, Aig_ObjFanin0(pObj), vNodes );
- Aig_ManDfsSeq_rec( p, Aig_ObjFanin1(pObj), vNodes );
-// if ( (Aig_ObjFanin0(pObj) == NULL || Aig_ObjIsBuf(Aig_ObjFanin0(pObj))) &&
-// (Aig_ObjFanin1(pObj) == NULL || Aig_ObjIsBuf(Aig_ObjFanin1(pObj))) )
- Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects internal nodes in the DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsSeq( Aig_Man_t * p )
-{
- Vec_Ptr_t * vNodes;
- Aig_Obj_t * pObj;
- int i;
- Aig_ManIncrementTravId( p );
- vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
- Aig_ManForEachPo( p, pObj, i )
- Aig_ManDfsSeq_rec( p, Aig_ObjFanin0(pObj), vNodes );
- return vNodes;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects internal nodes in the DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManDfsUnreach_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
- assert( !Aig_IsComplement(pObj) );
- if ( pObj == NULL )
- return;
- if ( Aig_ObjIsTravIdPrevious(p, pObj) || Aig_ObjIsTravIdCurrent(p, pObj) )
- return;
- Aig_ObjSetTravIdPrevious( p, pObj ); // assume unknown
- Aig_ManDfsUnreach_rec( p, Aig_ObjFanin0(pObj), vNodes );
- Aig_ManDfsUnreach_rec( p, Aig_ObjFanin1(pObj), vNodes );
- if ( Aig_ObjIsTravIdPrevious(p, Aig_ObjFanin0(pObj)) &&
- (Aig_ObjFanin1(pObj) == NULL || Aig_ObjIsTravIdPrevious(p, Aig_ObjFanin1(pObj))) )
- Vec_PtrPush( vNodes, pObj );
- else
- Aig_ObjSetTravIdCurrent( p, pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects internal nodes unreachable from PIs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsUnreach( Aig_Man_t * p )
-{
- Vec_Ptr_t * vNodes;
- Aig_Obj_t * pObj, * pFanin;
- int i, k;//, RetValue;
- // collect unreachable nodes
- Aig_ManIncrementTravId( p );
- Aig_ManIncrementTravId( p );
- // mark the constant and PIs
- Aig_ObjSetTravIdPrevious( p, Aig_ManConst1(p) );
- Aig_ManForEachPi( p, pObj, i )
- Aig_ObjSetTravIdCurrent( p, pObj );
- // curr marks visited nodes reachable from PIs
- // prev marks visited nodes unreachable or unknown
-
- // collect the unreachable nodes
- vNodes = Vec_PtrAlloc( 32 );
- Aig_ManForEachPo( p, pObj, i )
- Aig_ManDfsUnreach_rec( p, Aig_ObjFanin0(pObj), vNodes );
-
- // refine resulting nodes
- do
- {
- k = 0;
- Vec_PtrForEachEntry( vNodes, pObj, i )
- {
- assert( Aig_ObjIsTravIdPrevious(p, pObj) );
- if ( Aig_ObjIsLatch(pObj) || Aig_ObjIsBuf(pObj) )
- {
- pFanin = Aig_ObjFanin0(pObj);
- assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
- if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
- {
- Aig_ObjSetTravIdCurrent( p, pObj );
- continue;
- }
- }
- else // AND gate
- {
- assert( Aig_ObjIsNode(pObj) );
- pFanin = Aig_ObjFanin0(pObj);
- assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
- if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
- {
- Aig_ObjSetTravIdCurrent( p, pObj );
- continue;
- }
- pFanin = Aig_ObjFanin1(pObj);
- assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
- if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
- {
- Aig_ObjSetTravIdCurrent( p, pObj );
- continue;
- }
- }
- // write it back
- Vec_PtrWriteEntry( vNodes, k++, pObj );
- }
- Vec_PtrShrink( vNodes, k );
- }
- while ( k < i );
-
-// if ( Vec_PtrSize(vNodes) > 0 )
-// printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) );
- return vNodes;
-
-/*
- // the resulting array contains all unreachable nodes except const 1
- if ( Vec_PtrSize(vNodes) == 0 )
- {
- Vec_PtrFree( vNodes );
- return 0;
- }
- RetValue = Vec_PtrSize(vNodes);
-
- // mark these nodes
- Aig_ManIncrementTravId( p );
- Vec_PtrForEachEntry( vNodes, pObj, i )
- Aig_ObjSetTravIdCurrent( p, pObj );
- Vec_PtrFree( vNodes );
- return RetValue;
-*/
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Removes nodes that do not fanout into POs.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManRemoveUnmarked( Aig_Man_t * p )
-{
- Vec_Ptr_t * vNodes;
- Aig_Obj_t * pObj;
- int i, RetValue;
- // collect unmarked nodes
- vNodes = Vec_PtrAlloc( 100 );
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( Aig_ObjIsTerm(pObj) )
- continue;
- if ( Aig_ObjIsTravIdCurrent(p, pObj) )
- continue;
-//Aig_ObjPrintVerbose( pObj, 0 );
- Aig_ObjDisconnect( p, pObj );
- Vec_PtrPush( vNodes, pObj );
- }
- if ( Vec_PtrSize(vNodes) == 0 )
- {
- Vec_PtrFree( vNodes );
- return 0;
- }
- // remove the dangling objects
- RetValue = Vec_PtrSize(vNodes);
- Vec_PtrForEachEntry( vNodes, pObj, i )
- Aig_ObjDelete( p, pObj );
-// printf( "Removed %d dangling.\n", Vec_PtrSize(vNodes) );
- Vec_PtrFree( vNodes );
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [Rehashes the nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach )
-{
- Aig_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
- int i, RetValue = 0, Counter = 0;//, Counter2 = 0;
-
- // mark the unreachable nodes
- Aig_ManIncrementTravId( p );
- Vec_PtrForEachEntry( vUnreach, pObj, i )
- Aig_ObjSetTravIdCurrent(p, pObj);
-/*
- // count the number of unreachable object connections
- // that is the number of unreachable objects connected to main objects
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( Aig_ObjIsTravIdCurrent(p, pObj) )
- continue;
-
- pFanin0 = Aig_ObjFanin0(pObj);
- if ( pFanin0 == NULL )
- continue;
- if ( Aig_ObjIsTravIdCurrent(p, pFanin0) )
- pFanin0->fMarkA = 1;
-
- pFanin1 = Aig_ObjFanin1(pObj);
- if ( pFanin1 == NULL )
- continue;
- if ( Aig_ObjIsTravIdCurrent(p, pFanin1) )
- pFanin1->fMarkA = 1;
- }
-
- // count the objects
- Aig_ManForEachObj( p, pObj, i )
- Counter2 += pObj->fMarkA, pObj->fMarkA = 0;
- printf( "Connections = %d.\n", Counter2 );
-*/
-
- // go through the nodes while skipping unreachable
- Vec_PtrForEachEntry( vNodes, pObj, i )
- {
- // skip nodes unreachable from the PIs
- if ( Aig_ObjIsTravIdCurrent(p, pObj) )
- continue;
- // process the node
- if ( Aig_ObjIsPo(pObj) )
- {
- if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
- continue;
- pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
- Aig_ObjPatchFanin0( p, pObj, pFanin0 );
- continue;
- }
- if ( Aig_ObjIsLatch(pObj) )
- {
- if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
- continue;
- pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
- pObjNew = Aig_Latch( p, pObjNew, 0 );
- Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
- RetValue = 1;
- Counter++;
- continue;
- }
- if ( Aig_ObjIsNode(pObj) )
- {
- if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) && !Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) )
- continue;
- pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
- pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
- pObjNew = Aig_And( p, pFanin0, pFanin1 );
- Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
- RetValue = 1;
- Counter++;
- continue;
- }
- }
-// printf( "Rehashings = %d.\n", Counter++ );
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [If AIG contains buffers, this procedure removes them.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManRemoveBuffers( Aig_Man_t * p )
-{
- Aig_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
- int i;
- if ( Aig_ManBufNum(p) == 0 )
- return;
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( Aig_ObjIsPo(pObj) )
- {
- if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
- continue;
- pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
- Aig_ObjPatchFanin0( p, pObj, pFanin0 );
- }
- else if ( Aig_ObjIsLatch(pObj) )
- {
- if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
- continue;
- pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
- pObjNew = Aig_Latch( p, pFanin0, 0 );
- Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
- }
- else if ( Aig_ObjIsAnd(pObj) )
- {
- if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) && !Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) )
- continue;
- pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
- pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
- pObjNew = Aig_And( p, pFanin0, pFanin1 );
- Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
- }
- }
- assert( Aig_ManBufNum(p) == 0 );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits )
-{
- Vec_Ptr_t * vNodes, * vUnreach;
-// Aig_Obj_t * pObj, * pFanin;
-// int i;
- int Iter, RetValue = 1;
-
- // create latches out of the additional PI/PO pairs
- Aig_ManSeqStrashConvert( p, nLatches, pInits );
-
- // iteratively rehash the network
- for ( Iter = 0; RetValue; Iter++ )
- {
-// Aig_ManPrintStats( p );
-/*
- Aig_ManForEachObj( p, pObj, i )
- {
- assert( pObj->Type > 0 );
- pFanin = Aig_ObjFanin0(pObj);
- assert( pFanin == NULL || pFanin->Type > 0 );
- pFanin = Aig_ObjFanin1(pObj);
- assert( pFanin == NULL || pFanin->Type > 0 );
- }
-*/
- // mark nodes unreachable from the PIs
- vUnreach = Aig_ManDfsUnreach( p );
- if ( Iter == 0 && Vec_PtrSize(vUnreach) > 0 )
- printf( "Unreachable objects = %d.\n", Vec_PtrSize(vUnreach) );
- // collect nodes reachable from the POs
- vNodes = Aig_ManDfsSeq( p );
- // remove nodes unreachable from the POs
- if ( Iter == 0 )
- Aig_ManRemoveUnmarked( p );
- // continue rehashing as long as there are changes
- RetValue = Aig_ManSeqRehashOne( p, vNodes, vUnreach );
- Vec_PtrFree( vNodes );
- Vec_PtrFree( vUnreach );
- }
-
- // perform the final cleanup
- Aig_ManIncrementTravId( p );
- vNodes = Aig_ManDfsSeq( p );
- Aig_ManRemoveUnmarked( p );
- Vec_PtrFree( vNodes );
- // remove buffers if they are left
-// Aig_ManRemoveBuffers( p );
-
- // clean up
- if ( !Aig_ManCheck( p ) )
- {
- printf( "Aig_ManSeqStrash: The network check has failed.\n" );
- return 0;
- }
- return 1;
-
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/aig/aigShow.c b/src/aig/aig/aigShow.c
index 96b0e37f..8dc67c79 100644
--- a/src/aig/aig/aigShow.c
+++ b/src/aig/aig/aigShow.c
@@ -170,7 +170,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
*/
fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
- fprintf( pFile, ", shape = %s", (Aig_ObjIsLatch(pNode)? "box":"invtriangle") );
+ fprintf( pFile, ", shape = %s", "invtriangle" );
fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" );
}
@@ -237,7 +237,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
*/
fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
- fprintf( pFile, ", shape = %s", (Aig_ObjIsLatch(pNode)? "box":"triangle") );
+ fprintf( pFile, ", shape = %s", "triangle" );
fprintf( pFile, ", color = coral, fillcolor = coral" );
fprintf( pFile, "];\n" );
}
@@ -248,7 +248,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
// generate invisible edges from the square down
fprintf( pFile, "title1 -> title2 [style = invis];\n" );
Aig_ManForEachPo( pMan, pNode, i )
- fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") );
+ fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
// generate edges
Aig_ManForEachObj( pMan, pNode, i )
@@ -256,9 +256,9 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
if ( !Aig_ObjIsNode(pNode) && !Aig_ObjIsPo(pNode) && !Aig_ObjIsBuf(pNode) )
continue;
// generate the edge from this node to the next
- fprintf( pFile, "Node%d%s", pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") );
+ fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " -> " );
- fprintf( pFile, "Node%d%s", Aig_ObjFaninId0(pNode), (Aig_ObjIsLatch(Aig_ObjFanin0(pNode))? "_out":"") );
+ fprintf( pFile, "Node%d", Aig_ObjFaninId0(pNode) );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Aig_ObjFaninC0(pNode)? "dotted" : "bold" );
// if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
@@ -270,7 +270,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
// generate the edge from this node to the next
fprintf( pFile, "Node%d", pNode->Id );
fprintf( pFile, " -> " );
- fprintf( pFile, "Node%d%s", Aig_ObjFaninId1(pNode), (Aig_ObjIsLatch(Aig_ObjFanin1(pNode))? "_out":"") );
+ fprintf( pFile, "Node%d", Aig_ObjFaninId1(pNode) );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Aig_ObjFaninC1(pNode)? "dotted" : "bold" );
// if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index 357b63c3..9cfbf5f2 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -39,15 +39,8 @@ static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize )
static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t ** ppEntry;
- if ( Aig_ObjIsLatch(pObj) )
- {
- assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) == NULL );
- }
- else
- {
- assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) );
- assert( Aig_ObjFanin0(pObj)->Id < Aig_ObjFanin1(pObj)->Id );
- }
+ assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) );
+ assert( Aig_ObjFanin0(pObj)->Id < Aig_ObjFanin1(pObj)->Id );
for ( ppEntry = p->pTable + Aig_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
if ( *ppEntry == pObj )
return ppEntry;
@@ -119,20 +112,11 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
{
Aig_Obj_t * pEntry;
assert( !Aig_IsComplement(pGhost) );
- if ( pGhost->Type == AIG_OBJ_LATCH )
- {
- assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) == NULL );
- if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) )
- return NULL;
- }
- else
- {
- assert( pGhost->Type == AIG_OBJ_AND );
- assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
- assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id );
- if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) )
- return NULL;
- }
+ assert( Aig_ObjIsNode(pGhost) );
+ assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
+ assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id );
+ if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) )
+ return NULL;
for ( pEntry = p->pTable[Aig_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
{
if ( Aig_ObjChild0(pEntry) == Aig_ObjChild0(pGhost) &&
@@ -184,8 +168,6 @@ Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t *
void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t ** ppPlace;
- if ( p->pTable == NULL )
- return;
assert( !Aig_IsComplement(pObj) );
assert( Aig_TableLookup(p, pObj) == NULL );
if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Aig_ManNodeNum(p) )
@@ -209,8 +191,6 @@ void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t ** ppPlace;
- if ( p->pTable == NULL )
- return;
assert( !Aig_IsComplement(pObj) );
ppPlace = Aig_TableFind( p, pObj );
assert( *ppPlace == pObj ); // node should be in the table
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 00a85c26..ddb12e6e 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -16,7 +16,6 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigRet.c \
src/aig/aig/aigRetF.c \
src/aig/aig/aigScl.c \
- src/aig/aig/aigSeq.c \
src/aig/aig/aigShow.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTiming.c \
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 03707481..63f6f232 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -25,151 +25,12 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
-static Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
-static int Dar_BalanceFindLeft( Vec_Ptr_t * vSuper );
-static void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
-static void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj );
-static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel );
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Performs algebraic balancing of the AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
-{
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj, * pDriver, * pObjNew;
- Vec_Vec_t * vStore;
- int i;
- // create the new manager
- pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
- pNew->nRegs = p->nRegs;
- pNew->nAsserts = p->nAsserts;
- if ( p->vFlopNums )
- pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
- // map the PI nodes
- Aig_ManCleanData( p );
- Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- vStore = Vec_VecAlloc( 50 );
- if ( p->pManTime != NULL )
- {
- float arrTime;
- Tim_ManIncrementTravId( p->pManTime );
- Aig_ManSetPioNumbers( p );
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( Aig_ObjIsAnd(pObj) || Aig_ObjIsConst1(pObj) )
- continue;
- if ( Aig_ObjIsPi(pObj) )
- {
- // copy the PI
- pObjNew = Aig_ObjCreatePi(pNew);
- pObj->pData = pObjNew;
- // set the arrival time of the new PI
- arrTime = Tim_ManGetPiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
- pObjNew->Level = (int)arrTime;
- }
- else if ( Aig_ObjIsPo(pObj) )
- {
- // perform balancing
- pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
- pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
- pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
- Aig_ObjCreatePo( pNew, pObjNew );
- // save arrival time of the output
- arrTime = (float)Aig_Regular(pObjNew)->Level;
- Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
- }
- else
- assert( 0 );
- }
- Aig_ManCleanPioNumbers( p );
- pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
- }
- else
- {
- Aig_ManForEachPi( p, pObj, i )
- {
- pObjNew = Aig_ObjCreatePi(pNew);
- pObjNew->Level = pObj->Level;
- pObj->pData = pObjNew;
- }
- Aig_ManForEachPo( p, pObj, i )
- {
- pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
- pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
- pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
- Aig_ObjCreatePo( pNew, pObjNew );
- }
- }
- Vec_VecFree( vStore );
- // remove dangling nodes
- Aig_ManCleanup( pNew );
- // check the resulting AIG
- if ( !Aig_ManCheck(pNew) )
- printf( "Dar_ManBalance(): The check has failed.\n" );
- return pNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns the new node constructed.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
-{
- Aig_Obj_t * pObjNew;
- Vec_Ptr_t * vSuper;
- int i;
- assert( !Aig_IsComplement(pObjOld) );
- assert( !Aig_ObjIsBuf(pObjOld) );
- // return if the result is known
- if ( pObjOld->pData )
- return pObjOld->pData;
- assert( Aig_ObjIsNode(pObjOld) );
- // get the implication supergate
- vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
- // check if supergate contains two nodes in the opposite polarity
- if ( vSuper->nSize == 0 )
- return pObjOld->pData = Aig_ManConst0(pNew);
- if ( Vec_PtrSize(vSuper) < 2 )
- printf( "BUG!\n" );
- // for each old node, derive the new well-balanced node
- for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
- {
- pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
- vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
- }
- // build the supergate
- pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
- // make sure the balanced node is not assigned
-// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
- assert( pObjOld->pData == NULL );
- Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
- return pObjOld->pData = pObjNew;
-}
-
-/**Function*************************************************************
-
Synopsis [Collects the nodes of the supergate.]
Description []
@@ -185,14 +46,26 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
// check if the node is visited
if ( Aig_Regular(pObj)->fMarkB )
{
- // check if the node occurs in the same polarity
- for ( i = 0; i < vSuper->nSize; i++ )
- if ( vSuper->pArray[i] == pObj )
- return 1;
- // check if the node is present in the opposite polarity
- for ( i = 0; i < vSuper->nSize; i++ )
- if ( vSuper->pArray[i] == Aig_Not(pObj) )
- return -1;
+ if ( Aig_ObjIsExor(pRoot) )
+ {
+ assert( !Aig_IsComplement(pObj) );
+ // check if the node occurs in the same polarity
+ Vec_PtrRemove( vSuper, pObj );
+ Aig_Regular(pObj)->fMarkB = 0;
+//printf( " Duplicated EXOR input!!! " );
+ return 1;
+ }
+ else
+ {
+ // check if the node occurs in the same polarity
+ for ( i = 0; i < vSuper->nSize; i++ )
+ if ( vSuper->pArray[i] == pObj )
+ return 1;
+ // check if the node is present in the opposite polarity
+ for ( i = 0; i < vSuper->nSize; i++ )
+ if ( vSuper->pArray[i] == Aig_Not(pObj) )
+ return -1;
+ }
assert( 0 );
return 0;
}
@@ -251,60 +124,6 @@ Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
/**Function*************************************************************
- Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
-{
- int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
- if ( Diff > 0 )
- return -1;
- if ( Diff < 0 )
- return 1;
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Builds implication supergate.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
-{
- Aig_Obj_t * pObj1, * pObj2;
- int LeftBound;
- assert( vSuper->nSize > 1 );
- // sort the new nodes by level in the decreasing order
- Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
- // balance the nodes
- while ( vSuper->nSize > 1 )
- {
- // find the left bound on the node to be paired
- LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
- // find the node that can be shared (if no such node, randomize choice)
- Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
- // pull out the last two nodes
- pObj1 = Vec_PtrPop(vSuper);
- pObj2 = Vec_PtrPop(vSuper);
- Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
- }
- return Vec_PtrEntry(vSuper, 0);
-}
-
-/**Function*************************************************************
-
Synopsis [Finds the left bound on the next candidate to be paired.]
Description [The nodes in the array are in the decreasing order of levels.
@@ -405,6 +224,27 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
/**Function*************************************************************
+ Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
+{
+ int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
+ if ( Diff > 0 )
+ return -1;
+ if ( Diff < 0 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Inserts a new node in the order by levels.]
Description []
@@ -432,6 +272,220 @@ void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj )
}
}
+/**Function*************************************************************
+
+ Synopsis [Builds implication supergate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
+{
+ Aig_Obj_t * pObj1, * pObj2;
+ int LeftBound;
+ assert( vSuper->nSize > 1 );
+ // sort the new nodes by level in the decreasing order
+ Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
+ // balance the nodes
+ while ( vSuper->nSize > 1 )
+ {
+ // find the left bound on the node to be paired
+ LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
+ // find the node that can be shared (if no such node, randomize choice)
+ Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
+ // pull out the last two nodes
+ pObj1 = Vec_PtrPop(vSuper);
+ pObj2 = Vec_PtrPop(vSuper);
+ Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
+ }
+ return Vec_PtrEntry(vSuper, 0);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the new node constructed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
+{
+ Aig_Obj_t * pObjNew;
+ Vec_Ptr_t * vSuper;
+ int i;
+ assert( !Aig_IsComplement(pObjOld) );
+ assert( !Aig_ObjIsBuf(pObjOld) );
+ // return if the result is known
+ if ( pObjOld->pData )
+ return pObjOld->pData;
+ assert( Aig_ObjIsNode(pObjOld) );
+ // get the implication supergate
+ vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
+ // check if supergate contains two nodes in the opposite polarity
+ if ( vSuper->nSize == 0 )
+ return pObjOld->pData = Aig_ManConst0(pNew);
+ if ( Vec_PtrSize(vSuper) < 2 )
+ printf( "BUG!\n" );
+ // for each old node, derive the new well-balanced node
+ for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
+ {
+ pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+ vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
+ }
+ // build the supergate
+ pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
+ // make sure the balanced node is not assigned
+// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
+ assert( pObjOld->pData == NULL );
+ Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
+ return pObjOld->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs algebraic balancing of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pDriver, * pObjNew;
+ Vec_Vec_t * vStore;
+ int i;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->nRegs = p->nRegs;
+ pNew->nAsserts = p->nAsserts;
+ if ( p->vFlopNums )
+ pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+ // map the PI nodes
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ vStore = Vec_VecAlloc( 50 );
+ if ( p->pManTime != NULL )
+ {
+ float arrTime;
+ Tim_ManIncrementTravId( p->pManTime );
+ Aig_ManSetPioNumbers( p );
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
+ continue;
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ // copy the PI
+ pObjNew = Aig_ObjCreatePi(pNew);
+ pObj->pData = pObjNew;
+ // set the arrival time of the new PI
+ arrTime = Tim_ManGetPiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
+ pObjNew->Level = (int)arrTime;
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ // perform balancing
+ pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+ pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+ pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+ Aig_ObjCreatePo( pNew, pObjNew );
+ // save arrival time of the output
+ arrTime = (float)Aig_Regular(pObjNew)->Level;
+ Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
+ }
+ else
+ assert( 0 );
+ }
+ Aig_ManCleanPioNumbers( p );
+ pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+ }
+ else
+ {
+ Aig_ManForEachPi( p, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePi(pNew);
+ pObjNew->Level = pObj->Level;
+ pObj->pData = pObjNew;
+ }
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+ pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+ pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+ Aig_ObjCreatePo( pNew, pObjNew );
+ }
+ }
+ Vec_VecFree( vStore );
+ // remove dangling nodes
+ Aig_ManCleanup( pNew );
+ // check the resulting AIG
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Dar_ManBalance(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts a new node in the order by levels.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_BalancePrintStats( Aig_Man_t * p )
+{
+ Vec_Ptr_t * vSuper;
+ Aig_Obj_t * pObj, * pTemp;
+ int i, k;
+ if ( Aig_ManExorNum(p) == 0 )
+ {
+ printf( "There is no EXOR gates.\n" );
+ return;
+ }
+ Aig_ManForEachExor( p, pObj, i )
+ {
+ Aig_ObjFanin0(pObj)->fMarkA = 1;
+ Aig_ObjFanin1(pObj)->fMarkA = 1;
+ assert( !Aig_ObjFaninC0(pObj) );
+ assert( !Aig_ObjFaninC1(pObj) );
+ }
+ vSuper = Vec_PtrAlloc( 1000 );
+ Aig_ManForEachExor( p, pObj, i )
+ {
+ if ( pObj->fMarkA && pObj->nRefs == 1 )
+ continue;
+ Vec_PtrClear( vSuper );
+ Dar_BalanceCone_rec( pObj, pObj, vSuper );
+ Vec_PtrForEachEntry( vSuper, pTemp, k )
+ pTemp->fMarkB = 0;
+ if ( Vec_PtrSize(vSuper) < 3 )
+ continue;
+ printf( " %d(", Vec_PtrSize(vSuper) );
+ Vec_PtrForEachEntry( vSuper, pTemp, k )
+ printf( " %d", pTemp->Level );
+ printf( " )" );
+ }
+ Vec_PtrFree( vSuper );
+ Aig_ManForEachObj( p, pObj, i )
+ pObj->fMarkA = 0;
+ printf( "\n" );
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index a4ac9082..116b1591 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -201,14 +201,6 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
- // balance
- if ( fBalance )
- {
- pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
- Aig_ManStop( pTemp );
- if ( fVerbose ) Aig_ManPrintStats( pAig );
- }
-
return pAig;
}
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 67940c4f..444157f0 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -371,7 +371,6 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
if ( Aig_ManNodeNum(pManAig) == 0 )
return Aig_ManDup(pManAig, 1);
clk = clock();
- assert( Aig_ManLatchNum(pManAig) == 0 );
p = Fra_ManStart( pManAig, pPars );
p->pManFraig = Fra_ManPrepareComb( p );
p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 18c9ffcc..1ac2adab 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -344,7 +344,6 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
pParams->nIters = 0;
return Aig_ManDup(pManAig, 1);
}
- assert( Aig_ManLatchNum(pManAig) == 0 );
assert( Aig_ManRegNum(pManAig) > 0 );
assert( pParams->nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index a6460ed7..9149aca4 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -516,7 +516,6 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
if ( pnIter ) *pnIter = 0;
return Aig_ManDup(pAig, 1);
}
- assert( Aig_ManLatchNum(pAig) == 0 );
assert( Aig_ManRegNum(pAig) > 0 );
// simulate the AIG
diff --git a/src/aig/hop/hopTruth.c b/src/aig/hop/hopTruth.c
index 9a2161b6..47358715 100644
--- a/src/aig/hop/hopTruth.c
+++ b/src/aig/hop/hopTruth.c
@@ -176,8 +176,10 @@ unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars
// assert( Hop_ManPiNum(p) <= 8 );
if ( fMsbFirst )
{
- Hop_ManForEachPi( p, pObj, i )
+// Hop_ManForEachPi( p, pObj, i )
+ for ( i = 0; i < nVars; i++ )
{
+ pObj = Hop_ManPi( p, i );
if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
else
@@ -186,8 +188,10 @@ unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars
}
else
{
- Hop_ManForEachPi( p, pObj, i )
+// Hop_ManForEachPi( p, pObj, i )
+ for ( i = 0; i < nVars; i++ )
{
+ pObj = Hop_ManPi( p, i );
if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, i);
else
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-12 07:53:45 +0000