Skip to content

A
abc
Commit 6e774ef5 by Alan Mishchenko
Options

Cleaing AIG manager by removing pointers to HAIG.

parent a50a3815
Showing with 2 additions and 1137 deletions
abclib.dsp
......@@ -3283,10 +3283,6 @@ SOURCE=.\src\aig\saig\saigDup.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigHaig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigInd.c
# End Source File
# Begin Source File
......
src/aig/aig/aig.h
......@@ -66,7 +66,7 @@ typedef enum {
} Aig_Type_t;
// the AIG node
struct Aig_Obj_t_ // 9 words
struct Aig_Obj_t_ // 8 words
{
union {
Aig_Obj_t * pNext; // strashing table
......@@ -74,7 +74,6 @@ struct Aig_Obj_t_ // 9 words
};
Aig_Obj_t * pFanin0; // fanin
Aig_Obj_t * pFanin1; // fanin
Aig_Obj_t * pHaig; // pointer to the HAIG node
unsigned int Type : 3; // object type
unsigned int fPhase : 1; // value under 000...0 pattern
unsigned int fMarkA : 1; // multipurpose mask
......@@ -156,7 +155,6 @@ struct Aig_Man_t_
Vec_Ptr_t * vSeqModelVec; // vector of counter-examples (for sequential miters)
Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots;
Aig_Man_t * pManHaig;
int fCreatePios;
Vec_Int_t * vEquPairs;
Vec_Vec_t * vClockDoms;
......@@ -326,7 +324,6 @@ static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) {
static inline void Aig_ObjSetEquiv( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEqu ) { assert(p->pEquivs); p->pEquivs[pObj->Id] = pEqu; }
static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; }
static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr; }
static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); }
static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{
if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
......
src/aig/aig/aigDup.c
......@@ -49,7 +49,6 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
Aig_Obj_t * pObj, * pObjNew;
int i;
assert( p->pManTime == NULL );
assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
......@@ -61,11 +60,9 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachCi( p, pObj, i )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
......@@ -74,30 +71,21 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
if ( Aig_ObjIsBuf(pObj) )
{
pObjNew = Aig_ObjChild0Copy(pObj);
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// add the POs
Aig_ManForEachCo( p, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// pass the HAIG manager
if ( p->pManHaig != NULL )
{
pNew->pManHaig = p->pManHaig;
p->pManHaig = NULL;
}
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupSimple(): The check has failed.\n" );
......@@ -120,7 +108,6 @@ Aig_Man_t * Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints )
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i, Entry;
assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
assert( p->nAsserts == 0 || p->nConstrs == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
......@@ -175,7 +162,6 @@ Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular((Aig_Obj_t *)pObj->pData)->pHaig = pObj->pHaig;
return (Aig_Obj_t *)pObj->pData;
}
......@@ -200,7 +186,6 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
Aig_Obj_t * pObj, * pObjNew;
int i;
assert( p->pManTime == NULL );
assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
......@@ -212,11 +197,9 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachCi( p, pObj, i )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
......@@ -231,17 +214,10 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
Aig_ManForEachCo( p, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// pass the HAIG manager
if ( p->pManHaig != NULL )
{
pNew->pManHaig = p->pManHaig;
p->pManHaig = NULL;
}
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupSimple(): The check has failed.\n" );
......@@ -337,7 +313,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
}
else
assert( 0 );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
......@@ -347,12 +322,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
// pass the HAIG manager
if ( p->pManHaig != NULL )
{
pNew->pManHaig = p->pManHaig;
p->pManHaig = NULL;
}
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupOrdered(): The check has failed.\n" );
......@@ -376,7 +345,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
Aig_Obj_t * pObj, * pObjNew;
int i;
assert( p->pManTime == NULL );
assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
......@@ -388,7 +356,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachCi( p, pObj, i )
{
if ( i == iInput )
......@@ -396,7 +363,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
else
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
}
pObj->pData = pObjNew;
......@@ -406,31 +372,22 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
if ( Aig_ObjIsBuf(pObj) )
{
pObjNew = Aig_ObjChild0Copy(pObj);
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// add the POs
Aig_ManForEachCo( p, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
// assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
Aig_ManCleanup( pNew );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// pass the HAIG manager
if ( p->pManHaig != NULL )
{
pNew->pManHaig = p->pManHaig;
p->pManHaig = NULL;
}
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupSimple(): The check has failed.\n" );
......@@ -539,7 +496,6 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
}
else
assert( 0 );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
Aig_ManCleanup( pNew );
......@@ -576,10 +532,6 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
if ( p->pManHaig != NULL )
Aig_Regular(pObjNew)->pHaig = Aig_NotCond( pObj->pHaig, Aig_IsComplement(pObjNew) );
else if ( pObj->pHaig )
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
if ( pEquivNew )
{
assert( Aig_Regular(pEquivNew)->Id < Aig_Regular(pObjNew)->Id );
......@@ -624,14 +576,12 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
Aig_ManCleanData( p );
// duplicate internal nodes
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjIsCi(pObj) )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->Level = pObj->Level;
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsCo(pObj) )
......@@ -639,7 +589,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
}
......@@ -650,12 +599,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
// pass the HAIG manager
if ( p->pManHaig != NULL )
{
pNew->pManHaig = p->pManHaig;
p->pManHaig = NULL;
}
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupDfs(): The check has failed.\n" );
......@@ -720,8 +663,6 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin1(pObj) ) )
return NULL;
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
if ( pObj->pHaig )
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
if ( pEquivNew )
{
if ( pNew->pEquivs )
......@@ -771,14 +712,12 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
Aig_ManCleanData( p );
// duplicate internal nodes
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Vec_PtrForEachEntry( Aig_Obj_t *, vPios, pObj, i )
{
if ( Aig_ObjIsCi(pObj) )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->Level = pObj->Level;
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsCo(pObj) )
......@@ -786,7 +725,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) );
// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
}
......@@ -841,11 +779,9 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
}
// create the PIs
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachCi( p, pObj, i )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
......@@ -854,7 +790,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
Vec_VecForEachEntry( Aig_Obj_t *, 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 );
......@@ -862,7 +797,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
Aig_ManForEachCo( p, pObj, i )
{
pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
......
src/aig/aig/aigMan.c
......@@ -100,7 +100,6 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
{
pObjNew = Aig_ObjCreateCi( pNew );
pObjNew->Level = pObj->Level;
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
return pNew;
......@@ -127,7 +126,6 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
return (Aig_Obj_t *)(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 (Aig_Obj_t *)(pObj->pData = pObjNew);
}
......@@ -361,27 +359,6 @@ int Aig_ManCoCleanup( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Performs one iteration of AIG rewriting.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManHaigCounter( Aig_Man_t * pAig )
{
Aig_Obj_t * pObj;
int Counter, i;
Counter = 0;
Aig_ManForEachNode( pAig, pObj, i )
Counter += (pObj->pHaig != NULL);
return Counter;
}
/**Function*************************************************************
Synopsis [Stops the AIG manager.]
Description []
......
src/aig/aig/aigObj.c
......@@ -49,12 +49,6 @@ Aig_Obj_t * Aig_ObjCreateCi( Aig_Man_t * p )
pObj->Type = AIG_OBJ_CI;
Vec_PtrPush( p->vCis, pObj );
p->nObjs[AIG_OBJ_CI]++;
if ( p->pManHaig && p->fCreatePios )
{
p->pManHaig->nRegs++;
pObj->pHaig = Aig_ObjCreateCi( p->pManHaig );
// printf( "Creating PI HAIG node %d equivalent to PI %d.\n", pObj->pHaig->Id, pObj->Id );
}
return pObj;
}
......@@ -77,11 +71,6 @@ Aig_Obj_t * Aig_ObjCreateCo( Aig_Man_t * p, Aig_Obj_t * pDriver )
Vec_PtrPush( p->vCos, pObj );
Aig_ObjConnect( p, pObj, pDriver, NULL );
p->nObjs[AIG_OBJ_CO]++;
if ( p->pManHaig && p->fCreatePios )
{
pObj->pHaig = Aig_ObjCreateCo( p->pManHaig, Aig_ObjHaig( pDriver ) );
// printf( "Creating PO HAIG node %d equivalent to PO %d.\n", pObj->pHaig->Id, pObj->Id );
}
return pObj;
}
......@@ -111,14 +100,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 );
assert( !Aig_IsComplement(pObj->pHaig) );
// printf( "Creating HAIG node %d equivalent to node %d.\n", pObj->pHaig->Id, pObj->Id );
}
// create the power counter
if ( p->vProbs )
{
......@@ -384,14 +365,6 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
}
return;
}
if ( fHaig )
{
if ( pObj->pHaig == NULL )
printf( " HAIG node not given" );
else
printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") );
return;
}
// there are choices
if ( p->pEquivs && p->pEquivs[pObj->Id] )
{
......@@ -511,19 +484,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
printf( "Aig_ObjReplace(): Internal error!\n" );
exit(1);
}
// map the HAIG nodes
if ( p->pManHaig != NULL )
{
// printf( "Setting HAIG node %d equivalent to HAIG node %d (over = %d).\n",
// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
assert( pObjNewR->pHaig != NULL );
assert( !Aig_IsComplement(pObjNewR->pHaig) );
assert( p->pManHaig->vEquPairs != NULL );
Vec_IntPush( p->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
Vec_IntPush( p->pManHaig->vEquPairs, pObjOld->pHaig->Id );
}
else
pObjOld->pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
// recursively delete the old node - but leave the object there
pObjNewR->nRefs++;
Aig_ObjDelete_rec( p, pObjOld, 0 );
......
src/aig/aig/aigPart.c
......@@ -1493,8 +1493,6 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
// make sure the nodes of pThis point to pPrev
Aig_ManForEachObj( pPrev, pObj, i )
pObj->fMarkB = 1;
Aig_ManForEachObj( pThis, pObj, i )
assert( pObj->pHaig == NULL || (!Aig_IsComplement(pObj->pHaig) && pObj->pHaig->fMarkB) );
Aig_ManForEachObj( pPrev, pObj, i )
pObj->fMarkB = 0;
// remap nodes of pThis on top of pNew using pPrev
......@@ -1506,13 +1504,7 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
pObj->pData = Aig_ManCo(pNew, i);
// go through the nodes in the topological order
Aig_ManForEachNode( pThis, pObj, i )
{
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
if ( pObj->pHaig == NULL )
continue;
// pObj->pData and pObj->pHaig->pData are equivalent
Aig_ObjSetRepr_( pNew, Aig_Regular((Aig_Obj_t *)pObj->pData), Aig_Regular((Aig_Obj_t *)pObj->pHaig->pData) );
}
// set the inputs of POs as equivalent
Aig_ManForEachCo( pThis, pObj, i )
{
......
src/aig/saig/module.make
......@@ -7,7 +7,6 @@ SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigConstr2.c \
src/aig/saig/saigDual.c \
src/aig/saig/saigDup.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigInd.c \
src/aig/saig/saigIoa.c \
src/aig/saig/saigIso.c \
......
src/aig/saig/saigHaig.c deleted 100644 → 0
/**CFile****************************************************************
FileName [saigHaig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Experiments with history AIG recording.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "sat/bsat/satSolver.h"
#include "sat/cnf/cnf.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;//, * pMiter;
Aig_Obj_t * pPo;
// skip nodes without representative
pObjRepr = pObj->pHaig;
if ( pObjRepr == NULL )
return;
// assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = (Aig_Obj_t *)pObj->pData;
// get the new node of the representative
pObjReprNew = (Aig_Obj_t *)pObjRepr->pData;
// if this is the same node, no need to add constraints
assert( pObjNew != NULL && pObjReprNew != NULL );
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
return;
// these are different nodes - perform speculative reduction
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
// set the new node
pObj->pData = pObjNew2;
// add the constraint
if ( pObj->fMarkA )
return;
// pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
// pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
// assert( Aig_ObjPhaseReal(pMiter) == 1 );
// Aig_ObjCreateCo( pFrames, pMiter );
if ( Aig_ObjPhaseReal(pObjNew) != Aig_ObjPhaseReal(pObjReprNew) )
pObjReprNew = Aig_Not(pObjReprNew);
pPo = Aig_ObjCreateCo( pFrames, pObjNew );
Aig_ObjCreateCo( pFrames, pObjReprNew );
// remember the node corresponding to this PO
pPo->pData = pObj;
}
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f, nAssumptions = 0;
assert( nFrames == 1 || nFrames == 2 );
assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 );
// start AIG manager for timeframes
pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames );
pFrames->pName = Abc_UtilStrsav( pHaig->pName );
pFrames->pSpec = Abc_UtilStrsav( pHaig->pSpec );
// map the constant node
Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames );
// create variables for register outputs
Saig_ManForEachLo( pHaig, pObj, i )
pObj->pData = Aig_ObjCreateCi( pFrames );
// add timeframes
Aig_ManSetCioIds( pHaig );
for ( f = 0; f < nFrames; f++ )
{
// create primary inputs
Saig_ManForEachPi( pHaig, pObj, i )
pObj->pData = Aig_ObjCreateCi( pFrames );
// create internal nodes
Aig_ManForEachNode( pHaig, pObj, i )
{
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_ManHaigSpeculate( pFrames, pObj );
}
if ( f == nFrames - 2 )
nAssumptions = Aig_ManCoNum(pFrames);
if ( f == nFrames - 1 )
break;
// save register inputs
Saig_ManForEachLi( pHaig, pObj, i )
pObj->pData = Aig_ObjChild0Copy(pObj);
// transfer to register outputs
Saig_ManForEachLiLo( pHaig, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData;
}
Aig_ManCleanup( pFrames );
pFrames->nAsserts = Aig_ManCoNum(pFrames) - nAssumptions;
Aig_ManSetRegNum( pFrames, 0 );
return pFrames;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
{
Aig_Obj_t * pObj1, * pObj2;
int Id1, Id2, i, Counter = 0;
Aig_ManForEachObj( pHaig, pObj1, i )
pObj1->pHaig = NULL;
Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
{
Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
pObj1 = Aig_ManObj( pHaig, Id1 );
pObj2 = Aig_ManObj( pHaig, Id2 );
assert( pObj1 != pObj2 );
assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) );
if ( Aig_ObjIsCi(pObj1) )
{
Counter += (int)(pObj2->pHaig != NULL);
pObj2->pHaig = pObj1;
}
else if ( Aig_ObjIsCi(pObj2) )
{
Counter += (int)(pObj1->pHaig != NULL);
pObj1->pHaig = pObj2;
}
else if ( pObj1->Id < pObj2->Id )
{
Counter += (int)(pObj2->pHaig != NULL);
pObj2->pHaig = pObj1;
}
else
{
Counter += (int)(pObj1->pHaig != NULL);
pObj1->pHaig = pObj2;
}
}
// printf( "Overwrites %d out of %d.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, clock_t clkSynth )
{
int nBTLimit = 0;
Aig_Man_t * pFrames, * pTemp;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj1, * pObj2;
int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
clock_t clk = clock(), clkVerif;
nOvers = Aig_ManMapHaigNodes( pHaig );
// create time frames with speculative reduction and convert them into CNF
clk = clock();
pFrames = Aig_ManHaigFrames( pHaig, nFrames );
Aig_ManCleanMarkA( pHaig );
printf( "Frames: " );
Aig_ManPrintStats( pFrames );
pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
Aig_ManStop( pTemp );
printf( "Frames synt:" );
Aig_ManPrintStats( pFrames );
printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n",
Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );
// pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) - pFrames->nAsserts );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
// Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
// Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
// create the SAT solver to be used for this problem
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
return 0;
}
if ( nFrames == 2 )
{
// add clauses for the first frame
Aig_ManForEachCo( pFrames, pObj1, i )
{
if ( i >= Aig_ManCoNum(pFrames) - pFrames->nAsserts )
break;
pObj2 = Aig_ManCo( pFrames, ++i );
assert( pObj1->fPhase == pObj2->fPhase );
Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
return 0;
}
Lits[0]++;
Lits[1]--;
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
return 0;
}
}
if ( !sat_solver_simplify(pSat) )
{
sat_solver_delete( pSat );
return 0;
}
}
ABC_PRT( "Preparation", clock() - clk );
// check in the second timeframe
clk = clock();
Counter = 0;
printf( "Started solving ...\r" );
Aig_ManForEachCo( pFrames, pObj1, i )
{
if ( i < Aig_ManCoNum(pFrames) - pFrames->nAsserts )
continue;
pObj2 = Aig_ManCo( pFrames, ++i );
assert( pObj1->fPhase == pObj2->fPhase );
Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue1 == l_False )
{
Lits[0] = lit_neg( Lits[0] );
Lits[1] = lit_neg( Lits[1] );
// RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
// assert( RetValue );
}
Lits[0]++;
Lits[1]--;
RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue2 == l_False )
{
Lits[0] = lit_neg( Lits[0] );
Lits[1] = lit_neg( Lits[1] );
// RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
// assert( RetValue );
}
if ( RetValue1 != l_False || RetValue2 != l_False )
Counter++;
if ( i % 50 == 1 )
printf( "Solving assertion %6d out of %6d.\r",
(i - (Aig_ManCoNum(pFrames) - pFrames->nAsserts))/2,
pFrames->nAsserts/2 );
// if ( nClasses == 1000 )
// break;
}
printf( " \r" );
ABC_PRT( "Solving ", clock() - clk );
clkVerif = clock() - clk;
if ( Counter )
printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
else
printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
// print the statistic into a file
{
FILE * pTable;
Aig_Man_t * pTemp, * pHaig2;
pHaig2 = pAig->pManHaig;
pAig->pManHaig = NULL;
pTemp = Aig_ManDupDfs( pAig );
pAig->pManHaig = pHaig2;
Aig_ManSeqCleanup( pTemp );
pTable = fopen( "stats.txt", "a+" );
fprintf( pTable, "%s ", p->pName );
fprintf( pTable, "%d ", Saig_ManPiNum(p) );
fprintf( pTable, "%d ", Saig_ManPoNum(p) );
fprintf( pTable, "%d ", Saig_ManRegNum(p) );
fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
fprintf( pTable, "\n" );
fclose( pTable );
pTable = fopen( "stats2.txt", "a+" );
fprintf( pTable, "%s ", p->pName );
fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
fprintf( pTable, "%d ", pCnf->nVars );
fprintf( pTable, "%d ", pCnf->nClauses );
fprintf( pTable, "%d ", pCnf->nLiterals );
fprintf( pTable, "%d ", Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2 );
fprintf( pTable, "%d ", pFrames->nAsserts/2 );
fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
fprintf( pTable, "\n" );
fclose( pTable );
Aig_ManStop( pTemp );
}
// clean up
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
{
int nBTLimit = 0;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj1, * pObj2;
int i, RetValue1, RetValue2, Counter, Lits[2];
clock_t clk = clock();
int Delta;
int Id1, Id2;
assert( nFrames == 1 || nFrames == 2 );
clk = clock();
pCnf = Cnf_DeriveSimple( pHaig, Aig_ManCoNum(pHaig) );
// Aig_ManForEachObj( pHaig, pObj, i )
// printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
// printf( "\n" );
// create the SAT solver to be used for this problem
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
//Sat_SolverWriteDimacs( pSat, "1.cnf", NULL, NULL, 0 );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
return -1;
}
if ( nFrames == 2 )
{
Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
{
Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
pObj1 = Aig_ManObj( pHaig, Id1 );
pObj2 = Aig_ManObj( pHaig, Id2 );
if ( pObj1->fPhase ^ pObj2->fPhase )
{
Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 0 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
return 0;
}
Lits[0]++;
Lits[1]++;
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
return 0;
}
}
else
{
Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
return 0;
}
Lits[0]++;
Lits[1]--;
if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
{
sat_solver_delete( pSat );
return 0;
}
}
}
if ( !sat_solver_simplify(pSat) )
{
sat_solver_delete( pSat );
return 0;
}
}
ABC_PRT( "Preparation", clock() - clk );
// check in the second timeframe
clk = clock();
Counter = 0;
Delta = (nFrames == 2)? pCnf->nVars : 0;
Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
{
Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
pObj1 = Aig_ManObj( pHaig, Id1 );
pObj2 = Aig_ManObj( pHaig, Id2 );
if ( pObj1->fPhase ^ pObj2->fPhase )
{
Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 );
RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Lits[0]++;
Lits[1]++;
RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue1 != l_False || RetValue2 != l_False )
Counter++;
}
else
{
Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 );
RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Lits[0]++;
Lits[1]--;
RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue1 != l_False || RetValue2 != l_False )
Counter++;
}
if ( i % 50 == 1 )
printf( "Solving assertion %6d out of %6d.\r", i/2, Vec_IntSize(pHaig->vEquPairs)/2 );
// if ( i / 2 > 1000 )
// break;
}
ABC_PRT( "Solving ", clock() - clk );
if ( Counter )
printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
else
printf( "Verification is successful for all %d classes.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig )
{
Vec_Ptr_t * vTemp;
Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter;
int Id1, Id2, i;
// remove regular POs
Aig_ManSetCioIds( pHaig );
vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) );
Aig_ManForEachCo( pHaig, pObj, i )
{
if ( Saig_ObjIsPo(pHaig, pObj) )
{
Aig_ObjDisconnect( pHaig, pObj );
Vec_PtrWriteEntry( pHaig->vObjs, pObj->Id, NULL );
}
else
{
Vec_PtrPush( vTemp, pObj );
}
}
Vec_PtrShrink( pHaig->vCos, 0 );
pHaig->nObjs[AIG_OBJ_CO] = Vec_PtrSize( vTemp );
// add new POs
Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
{
Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
pObj1 = Aig_ManObj( pHaig, Id1 );
pObj2 = Aig_ManObj( pHaig, Id2 );
assert( pObj1 != pObj2 );
assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) );
pMiter = Aig_Exor( pHaig, pObj1, pObj2 );
pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) );
assert( Aig_ObjPhaseReal(pMiter) == 0 );
Aig_ObjCreateCo( pHaig, pMiter );
}
printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
// add the registers
Vec_PtrForEachEntry( Aig_Obj_t *, vTemp, pObj, i )
Vec_PtrPush( pHaig->vCos, pObj );
Vec_PtrFree( vTemp );
assert( pHaig->nObjs[AIG_OBJ_CO] == Vec_PtrSize(pHaig->vCos) );
Aig_ManCleanup( pHaig );
Aig_ManSetRegNum( pHaig, pHaig->nRegs );
// return pHaig;
printf( "HAIG: " );
Aig_ManPrintStats( pHaig );
printf( "HAIG is written into file \"haig.blif\".\n" );
Saig_ManDumpBlif( pHaig, "haig.blif" );
Vec_IntFree( pHaig->vEquPairs );
Aig_ManStop( pHaig );
return NULL;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
{
int fSeqHaig = (int)( Aig_ManRegNum(p) > 0 );
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Aig_Man_t * pNew, * pTemp;
Aig_Obj_t * pObj;
int i, k, nStepsReal;
clock_t clk = clock(), clkSynth;
Dar_ManDefaultRwrParams( pParsRwr );
clk = clock();
// duplicate this manager
pNew = Aig_ManDupSimple( p );
// create its history AIG
pNew->pManHaig = Aig_ManDupSimple( pNew );
Aig_ManForEachObj( pNew, pObj, i )
pObj->pHaig = (Aig_Obj_t *)pObj->pData;
// remove structural hashing table
Aig_TableClear( pNew->pManHaig );
pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 );
ABC_PRT( "HAIG setup time", clock() - clk );
clk = clock();
if ( fSeqHaig )
{
if ( fRetimingOnly )
{
// perform retiming
nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs );
pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
Aig_ManStop( pTemp );
printf( "Performed %d retiming moves.\n", nStepsReal );
}
else
{
for ( k = 0; k < nIters; k++ )
{
// perform balancing
pNew = Dar_ManBalance( pTemp = pNew, 0 );
Aig_ManStop( pTemp );
// perform rewriting
Dar_ManRewrite( pNew, pParsRwr );
pNew = Aig_ManDupDfs( pTemp = pNew );
Aig_ManStop( pTemp );
// perform retiming
nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs );
pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
Aig_ManStop( pTemp );
printf( "Performed %d retiming moves.\n", nStepsReal );
}
}
}
else
{
for ( k = 0; k < nIters; k++ )
{
// perform balancing
pNew = Dar_ManBalance( pTemp = pNew, 0 );
Aig_ManStop( pTemp );
// perform rewriting
Dar_ManRewrite( pNew, pParsRwr );
pNew = Aig_ManDupDfs( pTemp = pNew );
Aig_ManStop( pTemp );
}
}
ABC_PRT( "Synthesis time ", clock() - clk );
clkSynth = clock() - clk;
// use the haig for verification
// Aig_ManAntiCleanup( pNew->pManHaig );
Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
//Aig_ManShow( pNew->pManHaig, 0, NULL );
printf( "AIG before: " );
Aig_ManPrintStats( p );
printf( "AIG after: " );
Aig_ManPrintStats( pNew );
printf( "HAIG: " );
Aig_ManPrintStats( pNew->pManHaig );
if ( fUseCnf )
{
if ( !Aig_ManHaigVerify2( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
printf( "Constructing SAT solver has failed.\n" );
}
else
{
if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
printf( "Constructing SAT solver has failed.\n" );
}
Saig_ManHaigDump( pNew->pManHaig );
pNew->pManHaig = NULL;
return pNew;
/*
// cleanup
Vec_IntFree( pNew->pManHaig->vEquPairs );
Aig_ManStop( pNew->pManHaig );
pNew->pManHaig = NULL;
return pNew;
*/
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/base/abc/abc.h
......@@ -215,7 +215,6 @@ struct Abc_Ntk_t_
void * pExcare; // the EXDC network (if given)
void * pData; // misc
Abc_Ntk_t * pCopy; // copy of this network
void * pHaig; // history AIG
float * pLutTimes; // arrivals/requireds/slacks using LUT-delay model
Vec_Ptr_t * vOnehots; // names of one-hot-encoded registers
Vec_Int_t * vObjPerm; // permutation saved
......
src/base/abc/abcAig.c
......@@ -344,9 +344,6 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
// add the node to the list of updated nodes
if ( pMan->vAddedCells )
Vec_PtrPush( pMan->vAddedCells, pAnd );
// create HAIG
// if ( pAnd->pNtk->pHaig )
// pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) );
return pAnd;
}
......@@ -387,9 +384,6 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
// add the node to the list of updated nodes
// if ( pMan->vAddedCells )
// Vec_PtrPush( pMan->vAddedCells, pAnd );
// create HAIG
// if ( pAnd->pNtk->pHaig )
// pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) );
return pAnd;
}
......@@ -858,9 +852,6 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
Vec_PtrPush( pMan->vStackReplaceOld, pOld );
Vec_PtrPush( pMan->vStackReplaceNew, pNew );
assert( !Abc_ObjIsComplement(pOld) );
// create HAIG
// if ( pOld->pNtk->pHaig )
// Hop_ObjCreateChoice( pOld->pEquiv, Abc_ObjRegular(pNew)->pEquiv );
// process the replacements
while ( Vec_PtrSize(pMan->vStackReplaceOld) )
{
......
src/base/abc/abcNtk.c
......@@ -1070,9 +1070,6 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// int LargePiece = (4 << ABC_NUM_STEPS);
if ( pNtk == NULL )
return;
// free the HAIG
// if ( pNtk->pHaig )
// Abc_NtkHaigStop( pNtk );
// free EXDC Ntk
if ( pNtk->pExdc )
Abc_NtkDelete( pNtk->pExdc );
......
src/base/abci/abcBalance.c
......@@ -277,9 +277,6 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
// if ( Abc_ObjRegular(pNodeOld->pCopy) == Abc_AigConst1(pNtkNew) )
// printf( "Constant node\n" );
// assert( pNodeOld->Level >= Abc_ObjRegular(pNodeOld->pCopy)->Level );
// update HAIG
// if ( Abc_ObjRegular(pNodeOld->pCopy)->pNtk->pHaig )
// Hop_ObjCreateChoice( pNodeOld->pEquiv, Abc_ObjRegular(pNodeOld->pCopy)->pEquiv );
return pNodeOld->pCopy;
}
......
src/base/abci/abcHaig.c
......@@ -31,129 +31,6 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#if 0
/**Function*************************************************************
Synopsis [Start history AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkHaigStart( Abc_Ntk_t * pNtk )
{
Hop_Man_t * p;
Abc_Obj_t * pObj, * pTemp;
int i;
assert( Abc_NtkIsStrash(pNtk) );
// check if the package is already started
if ( pNtk->pHaig )
{
Abc_NtkHaigStop( pNtk );
assert( pNtk->pHaig == NULL );
printf( "Warning: Previous history AIG was removed.\n" );
}
// make sure the data is clean
Abc_NtkForEachObj( pNtk, pObj, i )
assert( pObj->pEquiv == NULL );
// start the HOP package
p = Hop_ManStart();
p->vObjs = Vec_PtrAlloc( 4096 );
Vec_PtrPush( p->vObjs, Hop_ManConst1(p) );
// map the constant node
Abc_AigConst1(pNtk)->pEquiv = Hop_ManConst1(p);
// map the CIs
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pEquiv = Hop_ObjCreatePi(p);
// map the internal nodes
Abc_NtkForEachNode( pNtk, pObj, i )
pObj->pEquiv = Hop_And( p, Abc_ObjChild0Equiv(pObj), Abc_ObjChild1Equiv(pObj) );
// map the choice nodes
if ( Abc_NtkGetChoiceNum( pNtk ) )
{
// print warning about choice nodes
printf( "Warning: The choice nodes in the original AIG are converted into HAIG.\n" );
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( !Abc_AigNodeIsChoice( pObj ) )
continue;
for ( pTemp = pObj->pData; pTemp; pTemp = pTemp->pData )
Hop_ObjCreateChoice( pObj->pEquiv, pTemp->pEquiv );
}
}
// make sure everything is okay
if ( !Hop_ManCheck(p) )
{
printf( "Abc_NtkHaigStart: Check for History AIG has failed.\n" );
Hop_ManStop(p);
return 0;
}
pNtk->pHaig = p;
return 1;
}
/**Function*************************************************************
Synopsis [Stops history AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkHaigStop( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i;
assert( Abc_NtkIsStrash(pNtk) );
if ( pNtk->pHaig == NULL )
{
printf( "Warning: History AIG is not allocated.\n" );
return 1;
}
Abc_NtkForEachObj( pNtk, pObj, i )
pObj->pEquiv = NULL;
Hop_ManStop( pNtk->pHaig );
pNtk->pHaig = NULL;
return 1;
}
/**Function*************************************************************
Synopsis [Transfers the HAIG to the new network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
{
Abc_Obj_t * pObj;
int i;
if ( pNtkOld->pHaig == NULL )
return;
// transfer the package
assert( pNtkNew->pHaig == NULL );
pNtkNew->pHaig = pNtkOld->pHaig;
pNtkOld->pHaig = NULL;
// transfer constant pointer
Abc_AigConst1(pNtkOld)->pCopy->pEquiv = Abc_AigConst1(pNtkOld)->pEquiv;
// transfer the CI pointers
Abc_NtkForEachCi( pNtkOld, pObj, i )
pObj->pCopy->pEquiv = pObj->pEquiv;
}
#endif
/**Function*************************************************************
......@@ -642,64 +519,6 @@ int Abc_NtkHaigResetReprs( Hop_Man_t * p )
return nFanouts;
}
#if 0
/**Function*************************************************************
Synopsis [Stops history AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
{
Hop_Man_t * pMan, * pManTemp;
Abc_Ntk_t * pNtkAig;
Abc_Obj_t * pObj;
int i;
// check if HAIG is available
assert( Abc_NtkIsStrash(pNtk) );
if ( pNtk->pHaig == NULL )
{
printf( "Warning: History AIG is not available.\n" );
return NULL;
}
// convert HOP package into AIG with choices
// print HAIG stats
// Hop_ManPrintStats( pMan ); // USES DATA!!!
// add the POs
Abc_NtkForEachCo( pNtk, pObj, i )
Hop_ObjCreatePo( pNtk->pHaig, Abc_ObjChild0Equiv(pObj) );
// clean the old network
Abc_NtkForEachObj( pNtk, pObj, i )
pObj->pEquiv = NULL;
pMan = pNtk->pHaig;
pNtk->pHaig = 0;
// iteratively reconstruct the HOP manager to create choice nodes
while ( Abc_NtkHaigResetReprs( pMan ) )
{
pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
Hop_ManStop( pManTemp );
}
// traverse in the topological order and create new AIG
pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
Hop_ManStop( pMan );
// free HAIG
return pNtkAig;
}
#endif
/**Function*************************************************************
Synopsis [Transform HOP manager into the one without loops.]
......
src/base/abci/abcPart.c
......@@ -1000,7 +1000,6 @@ Hop_Man_t * Abc_NtkPartStartHop( Abc_Ntk_t * pNtk )
Abc_Ntk_t * Abc_NtkPartStitchChoices( Abc_Ntk_t * pNtk, Vec_Ptr_t * vParts )
{
extern Abc_Ntk_t * Abc_NtkHopRemoveLoops( Abc_Ntk_t * pNtk, Hop_Man_t * pMan );
Hop_Man_t * pMan;
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew, * pNtkTemp;
......
src/base/abci/module.make
......@@ -21,7 +21,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcFraig.c \
src/base/abci/abcFxu.c \
src/base/abci/abcGen.c \
src/base/abci/abcHaig.c \
src/base/abci/abcHaig.c \
src/base/abci/abcIf.c \
src/base/abci/abcIfif.c \
src/base/abci/abcIfMux.c \
......
src/opt/dar/darBalance.c
......@@ -532,19 +532,6 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
// make sure the balanced node is not assigned
// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
assert( pObjOld->pData == NULL );
if ( pNew->pManHaig != NULL )
{
Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
// printf( "Balancing HAIG node %d equivalent to HAIG node %d (over = %d).\n",
// pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
assert( pObjNewR->pHaig != NULL );
assert( !Aig_IsComplement(pObjNewR->pHaig) );
assert( pNew->pManHaig->vEquPairs != NULL );
Vec_IntPush( pNew->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
Vec_IntPush( pNew->pManHaig->vEquPairs, pObjOld->pHaig->Id );
}
else
Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
return (Aig_Obj_t *)(pObjOld->pData = pObjNew);
}
......@@ -574,12 +561,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pNew->nConstrs = p->nConstrs;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
// pass the HAIG manager
if ( p->pManHaig != NULL )
{
pNew->pManHaig = p->pManHaig; p->pManHaig = NULL;
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(pNew->pManHaig);
}
// map the PI nodes
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
......@@ -598,7 +579,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
// copy the PI
pObjNew = Aig_ObjCreateCi(pNew);
pObj->pData = pObjNew;
pObjNew->pHaig = pObj->pHaig;
// set the arrival time of the new PI
arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
pObjNew->Level = (int)arrTime;
......@@ -614,7 +594,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime );
// create PO
pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
pObjNew->pHaig = pObj->pHaig;
}
else
assert( 0 );
......@@ -629,7 +608,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pObjNew = Aig_ObjCreateCi(pNew);
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
pObjNew->pHaig = pObj->pHaig;
}
Aig_ManForEachCo( p, pObj, i )
{
......@@ -637,7 +615,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
pObjNew->pHaig = pObj->pHaig;
}
}
Vec_VecFree( vStore );
......
src/opt/dar/darScript.c
......@@ -134,27 +134,6 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
/**Function*************************************************************
Synopsis [Performs one iteration of AIG rewriting.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManHaigPrintStats( Aig_Man_t * pAig )
{
Aig_Obj_t * pObj;
int Counter, i;
Counter = 0;
Aig_ManForEachNode( pAig, pObj, i )
Counter += (pObj->pHaig != NULL);
printf( "Total nodes = %6d. Equiv nodes = %6d.\n", Aig_ManNodeNum(pAig), Counter );
}
/**Function*************************************************************
Synopsis [Reproduces script "compress".]
Description []
......@@ -352,34 +331,20 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
{
Vec_Ptr_t * vAigs;
Aig_Obj_t * pObj;
int i;
vAigs = Vec_PtrAlloc( 3 );
pAig = Aig_ManDupDfs(pAig);
Vec_PtrPush( vAigs, pAig );
Aig_ManForEachObj( pAig, pObj, i )
pObj->pHaig = pObj;
pAig = Dar_ManCompress(pAig, fBalance, fUpdateLevel, fPower, fVerbose);
Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );
Aig_ManForEachObj( pAig, pObj, i )
{
pObj->pNext = pObj->pHaig;
pObj->pHaig = pObj;
}
pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose);
Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );
pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 );
Aig_ManForEachObj( pAig, pObj, i )
pObj->pHaig = pObj->pNext;
return vAigs;
}
......
src/proof/fra/fraLcr.c
......@@ -273,7 +273,6 @@ Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
Fra_LcrManDup_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 (Aig_Obj_t *)(pObj->pData = pObjNew);
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment