luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc80517

This commit is contained in:
Alan Mishchenko 2008-05-17 08:01:00 -07:00
parent 6da56f1f0f
commit 4d37d4d92f
32 changed files with 1066 additions and 560 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
abc.dsp
View File

@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
@ -3262,6 +3262,10 @@ SOURCE=.\src\aig\saig\saigCone.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigHaig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigInter.c
# End Source File
# Begin Source File

18
src/aig/aig/aig.h
View File

@ -150,6 +150,8 @@ struct Aig_Man_t_
void * pSeqModel;
Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots;
Aig_Man_t * pManHaig;
int fCreatePios;
// timing statistics
int time1;
int time2;
@ -322,7 +324,8 @@ static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj
static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); }
static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; }
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 int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext; }
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_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext; }
static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{
if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
@ -469,11 +472,12 @@ extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t
extern void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
/*=== aigDup.c ==========================================================*/
extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder );
extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide );
extern Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p );
@ -487,15 +491,15 @@ extern void Aig_ManFanoutStart( Aig_Man_t * p );
extern void Aig_ManFanoutStop( Aig_Man_t * p );
/*=== aigFrames.c ==========================================================*/
extern Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap );
/*=== aigHaig.c ==========================================================*/
extern void Aig_ManHaigRecord( Aig_Man_t * p );
/*=== aigMan.c ==========================================================*/
extern Aig_Man_t * Aig_ManStart( int nNodesMax );
extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManStop( Aig_Man_t * p );
extern int Aig_ManCleanup( Aig_Man_t * p );
extern int Aig_ManAntiCleanup( Aig_Man_t * p );
extern int Aig_ManPiCleanup( Aig_Man_t * p );
extern int Aig_ManPoCleanup( Aig_Man_t * p );
extern void Aig_ManPrintStats( Aig_Man_t * p );
extern void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
extern void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs );
@ -517,9 +521,9 @@ extern void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_
extern void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop );
extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel );
extern void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fUpdateLevel );
/*=== aigOper.c =========================================================*/
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 );

143
src/aig/aig/aigDup.c
View File

@ -40,11 +40,13 @@
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
{
Aig_Man_t * pNew;
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 = Aig_UtilStrsav( p->pName );
@ -88,12 +90,109 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
pObj->pData = pObjNew;
}
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 );
// 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_ManDup(): The check has failed.\n" );
printf( "Aig_ManDupSimple(): The check has failed.\n" );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager recursively.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
if ( pObj->pData )
return pObj->pData;
Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
if ( Aig_ObjIsBuf(pObj) )
return 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(pObj->pData)->pHaig = pObj->pHaig;
return pObj->pData;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description [Orders nodes as follows: PIs, ANDs, POs.]
SideEffects [This procedure assumes that buffers are not used during
HAIG recording. This way, each HAIG node is in one-to-one correspondence
with old HAIG node. There is no need to create new nodes, just reassign
the pointers. If it were not the case, we would need to create HAIG nodes
for each new node duplicated. ]
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
{
Aig_Man_t * pNew;
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 = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
pNew->nTruePis = p->nTruePis;
pNew->nTruePos = p->nTruePos;
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
Aig_ManForEachObj( p, pObj, i )
if ( !Aig_ObjIsPo(pObj) )
{
Aig_ManDupSimpleDfs_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) );
// 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" );
return pNew;
}
@ -160,6 +259,12 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( 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" );
@ -255,7 +360,9 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
return 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 ( pObj->pHaig )
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 )
{
@ -313,7 +420,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->Level = pObj->Level;
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsPo(pObj) )
@ -321,7 +428,7 @@ 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_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
}
@ -331,6 +438,12 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
// duplicate the timing manager
if ( p->pManTime )
pNew->pManTime = Tim_ManDup( 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" );
@ -379,7 +492,7 @@ Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder )
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjNew, * pEquivNew = NULL;
if ( pObj->pData )
@ -387,12 +500,12 @@ Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t *
if ( Aig_ObjIsPi(pObj) )
return NULL;
if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
pEquivNew = Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
if ( !Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin0(pObj) ) )
pEquivNew = Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) ) )
return NULL;
if ( Aig_ObjIsBuf(pObj) )
return pObj->pData = Aig_ObjChild0Copy(pObj);
if ( !Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin1(pObj) ) )
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 )
@ -418,7 +531,7 @@ Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t *
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
{
Vec_Ptr_t * vPios;
Aig_Man_t * pNew;
@ -448,7 +561,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
// duplicate internal nodes
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
vPios = Aig_ManOrderPios( p, pOrder );
vPios = Aig_ManOrderPios( p, pGuide );
Vec_PtrForEachEntry( vPios, pObj, i )
{
if ( Aig_ObjIsPi(pObj) )
@ -460,7 +573,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
}
else if ( Aig_ObjIsPo(pObj) )
{
Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin0(pObj) );
Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) );
// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;

271
src/aig/aig/aigHaig.c
View File

@ -1,271 +0,0 @@
/**CFile****************************************************************
FileName [aigHaig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: aigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
#include "satSolver.h"
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Aig_Obj_t * Aig_HaigObjFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f ) { return ppMap[nFrames*pObj->Id + f]; }
static inline void Aig_HaigObjSetFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + f] = pNode; }
static inline Aig_Obj_t * Aig_HaigObjChild0Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Aig_HaigObjChild1Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs speculative reduction for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Aig_ManHaigFramesNode( Aig_Obj_t ** ppMap, int nFrames, Aig_Man_t * pFrames, Aig_Obj_t * pObj, int iFrame )
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
// skip nodes without representative
pObjRepr = pObj->pHaig;
if ( pObjRepr == NULL )
return;
assert( !Aig_IsComplement(pObjRepr) );
assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = Aig_HaigObjFrames( ppMap, nFrames, pObj, iFrame );
// get the new node of the representative
pObjReprNew = Aig_HaigObjFrames( ppMap, nFrames, pObjRepr, iFrame );
// if this is the same node, no need to add constraints
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
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, iFrame, pObjNew2 );
// add the constraint
pMiter = Aig_Exor( pFrames, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
pMiter = Aig_Not( pMiter );
Aig_ObjCreatePo( pFrames, pMiter );
}
/**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, * pObjNew;
Aig_Obj_t ** ppMap;
int i, k, f;
assert( nFrames >= 2 );
assert( Aig_ManRegNum(pHaig) > 0 );
assert( Aig_ManRegNum(pHaig) < Aig_ManPiNum(pHaig) );
// create node mapping
ppMap = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pHaig) * nFrames );
memset( ppMap, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pHaig) * nFrames );
// start the frames
pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames );
pFrames->pName = Aig_UtilStrsav( pHaig->pName );
pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec );
pFrames->nRegs = pHaig->nRegs;
// create PI nodes for the frames
for ( f = 0; f < nFrames; f++ )
Aig_HaigObjSetFrames( ppMap, nFrames, Aig_ManConst1(pHaig), f, Aig_ManConst1(pFrames) );
for ( f = 0; f < nFrames; f++ )
Aig_ManForEachPiSeq( pHaig, pObj, i )
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
// create latches for the first frame
Aig_ManForEachLoSeq( pHaig, pObj, i )
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// mark the asserts
if ( f == nFrames - 1 )
pFrames->nAsserts = Aig_ManPoNum(pFrames);
// constrain latch outputs and internal nodes
Aig_ManForEachObj( pHaig, pObj, i )
{
if ( Aig_ObjIsPi(pObj) && Aig_HaigObjFrames(ppMap, nFrames, pObj, f) == NULL )
{
Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
}
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( pFrames,
Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f),
Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) );
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew );
Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
}
}
/*
// set the constraints on the latch outputs
Aig_ManForEachLoSeq( pHaig, pObj, i )
Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
// add internal nodes of this frame
Aig_ManForEachNode( pHaig, pObj, i )
{
pObjNew = Aig_And( pFrames,
Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f),
Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) );
Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew );
Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
}
*/
// transfer latch inputs to the latch outputs
Aig_ManForEachLiLoSeq( pHaig, pObjLi, pObjLo, k )
{
pObjNew = Aig_HaigObjChild0Frames(ppMap,nFrames,pObjLi,f);
Aig_HaigObjSetFrames( ppMap, nFrames, pObjLo, f+1, pObjNew );
}
}
// remove dangling nodes
Aig_ManCleanup( pFrames );
free( ppMap );
return pFrames;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManHaigVerify( Aig_Man_t * pHaig )
{
int nBTLimit = 0;
Aig_Man_t * pFrames;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj;
int i, Lit, RetValue, Counter;
int clk = clock();
// create time frames with speculative reduction and convert them into CNF
clk = clock();
pFrames = Aig_ManHaigFrames( pHaig, 2 );
pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
// create the SAT solver to be used for this problem
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
printf( "HAIG regs = %d. HAIG nodes = %d. Outputs = %d.\n",
Aig_ManRegNum(pHaig), Aig_ManNodeNum(pHaig), Aig_ManPoNum(pHaig) );
printf( "Frames regs = %d. Frames nodes = %d. Outputs = %d. Assumptions = %d. Asserts = %d.\n",
Aig_ManRegNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManPoNum(pFrames),
pFrames->nAsserts, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
PRT( "Preparation", clock() - clk );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
return -1;
}
// solve each output
clk = clock();
Counter = 0;
Aig_ManForEachPo( pFrames, pObj, i )
{
if ( i < pFrames->nAsserts )
continue;
Lit = toLitCond( pCnf->pVarNums[pObj->Id], pObj->fPhase );
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
Counter++;
}
PRT( "Solving ", clock() - clk );
if ( Counter )
printf( "Verification failed for %d classes.\n", Counter );
else
printf( "Verification is successful.\n" );
// clean up
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManHaigRecord( Aig_Man_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
// start the HAIG
p->pManHaig = Aig_ManDupOrdered( p );
// set the pointers to the HAIG nodes
Aig_ManForEachObj( p, pObj, i )
pObj->pHaig = pObj->pData;
// remove structural hashing table
Aig_TableClear( p->pManHaig );
// perform a sequence of synthesis steps
pNew = Aig_ManRetimeFrontier( p, 10000 );
// use the haig for verification
Aig_ManDumpBlif( pNew->pManHaig, "haig_temp.blif", NULL, NULL );
Aig_ManHaigVerify( pNew->pManHaig );
Aig_ManStop( pNew );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

60
src/aig/aig/aigMan.c
View File

@ -163,7 +163,7 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t *
Aig_ObjCreatePo( pNew, pObj );
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDup(): The check has failed.\n" );
printf( "Aig_ManExtractMiter(): The check has failed.\n" );
return pNew;
}
@ -235,8 +235,7 @@ int Aig_ManCleanup( Aig_Man_t * p )
{
Vec_Ptr_t * vObjs;
Aig_Obj_t * pNode;
int i, nNodesOld;
nNodesOld = Aig_ManNodeNum(p);
int i, nNodesOld = Aig_ManNodeNum(p);
// collect roots of dangling nodes
vObjs = Vec_PtrAlloc( 100 );
Aig_ManForEachObj( p, pNode, i )
@ -249,6 +248,27 @@ int Aig_ManCleanup( Aig_Man_t * p )
return nNodesOld - Aig_ManNodeNum(p);
}
/**Function*************************************************************
Synopsis [Adds POs for the nodes that otherwise would be dangling.]
Description [Returns the number of POs added.]
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManAntiCleanup( Aig_Man_t * p )
{
Aig_Obj_t * pNode;
int i, nNodesOld = Aig_ManPoNum(p);
Aig_ManForEachObj( p, pNode, i )
if ( Aig_ObjIsNode(pNode) && Aig_ObjRefs(pNode) == 0 )
Aig_ObjCreatePo( p, pNode );
return nNodesOld - Aig_ManPoNum(p);
}
/**Function*************************************************************
Synopsis [Removes PIs without fanouts.]
@ -280,6 +300,40 @@ int Aig_ManPiCleanup( Aig_Man_t * p )
return nPisOld - Aig_ManPiNum(p);
}
/**Function*************************************************************
Synopsis [Removes POs with constant input.]
Description [Returns the number of POs removed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManPoCleanup( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i, k = 0, nPosOld = Aig_ManPoNum(p);
Vec_PtrForEachEntry( p->vPos, pObj, i )
{
if ( i >= Aig_ManPoNum(p) - Aig_ManRegNum(p) )
Vec_PtrWriteEntry( p->vPos, k++, pObj );
else if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) || !Aig_ObjFaninC0(pObj) ) // non-const or const1
Vec_PtrWriteEntry( p->vPos, k++, pObj );
else
{
Aig_ObjDisconnect( p, pObj );
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
}
}
Vec_PtrShrink( p->vPos, k );
p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
if ( Aig_ManRegNum(p) )
p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
return nPosOld - Aig_ManPoNum(p);
}
/**Function*************************************************************
Synopsis [Performs one iteration of AIG rewriting.]

339
src/aig/aig/aigObj.c
View File

@ -46,6 +46,12 @@ Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p )
pObj->Type = AIG_OBJ_PI;
Vec_PtrPush( p->vPis, pObj );
p->nObjs[AIG_OBJ_PI]++;
if ( p->pManHaig && p->fCreatePios )
{
p->pManHaig->nRegs++;
pObj->pHaig = Aig_ObjCreatePi( p->pManHaig );
// printf( "Creating PI HAIG node %d equivalent to PI %d.\n", pObj->pHaig->Id, pObj->Id );
}
return pObj;
}
@ -68,6 +74,11 @@ Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver )
Vec_PtrPush( p->vPos, pObj );
Aig_ObjConnect( p, pObj, pDriver, NULL );
p->nObjs[AIG_OBJ_PO]++;
if ( p->pManHaig && p->fCreatePios )
{
pObj->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( pDriver ) );
// printf( "Creating PO HAIG node %d equivalent to PO %d.\n", pObj->pHaig->Id, pObj->Id );
}
return pObj;
}
@ -88,7 +99,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,6 +108,14 @@ 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 );
}
return pObj;
}
@ -137,7 +156,7 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj
pObj->Level = Aig_ObjLevelNew( pObj );
pObj->fPhase = Aig_ObjPhaseReal(pFan0) & Aig_ObjPhaseReal(pFan1);
// add the node to the structural hash table
if ( Aig_ObjIsHash(pObj) )
if ( p->pTable && Aig_ObjIsHash(pObj) )
Aig_TableInsert( p, pObj );
// add the node to the dynamically updated topological order
// if ( p->pOrderData && Aig_ObjIsNode(pObj) )
@ -173,7 +192,7 @@ void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj )
Aig_ObjDeref(Aig_ObjFanin1(pObj));
}
// remove the node from the structural hash table
if ( Aig_ObjIsHash(pObj) )
if ( p->pTable && Aig_ObjIsHash(pObj) )
Aig_TableDelete( p, pObj );
// add the first fanin
pObj->pFanin0 = NULL;
@ -269,160 +288,6 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
Aig_ObjDelete_rec( p, pFaninOld, 1 );
}
/**Function*************************************************************
Synopsis [Replaces node with a buffer fanin by a node without them.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, int fUpdateLevel )
{
Aig_Obj_t * pFanReal0, * pFanReal1, * pResult;
p->nBufFixes++;
if ( Aig_ObjIsPo(pObj) )
{
assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) );
pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
assert( Aig_ObjPhaseReal(Aig_ObjChild0(pObj)) == Aig_ObjPhaseReal(pFanReal0) );
Aig_ObjPatchFanin0( p, pObj, pFanReal0 );
return;
}
assert( Aig_ObjIsNode(pObj) );
assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) || Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) );
// get the real fanins
pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pFanReal1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
// get the new node
if ( Aig_ObjIsNode(pObj) )
pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) );
// else if ( Aig_ObjIsLatch(pObj) )
// pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) );
else
assert( 0 );
// replace the node with buffer by the node without buffer
Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel );
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
{
Aig_Obj_t * pObj;
int nSteps;
assert( p->pFanData );
for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
{
// get the node with a buffer fanin
for ( pObj = Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) );
// replace this node by a node without buffer
Aig_NodeFixBufferFanins( p, pObj, fNodesOnly, fUpdateLevel );
// stop if a cycle occured
if ( nSteps > 1000000 )
{
printf( "Error: A cycle is encountered while propagating buffers.\n" );
break;
}
}
return nSteps;
}
/**Function*************************************************************
Synopsis [Replaces one object by another.]
Description [The new object (pObjNew) should be used instead of the old
object (pObjOld). If the new object is complemented or used, the buffer
is added and the new object remains in the manager; otherwise, the new
object is deleted.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel )
{
Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
Aig_Obj_t * pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
// the object to be replaced cannot be complemented
assert( !Aig_IsComplement(pObjOld) );
// the object to be replaced cannot be a terminal
// assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) );
assert( !Aig_ObjIsPo(pObjOld) );
// the object to be used cannot be a buffer or a PO
assert( !Aig_ObjIsBuf(pObjNewR) && !Aig_ObjIsPo(pObjNewR) );
// the object cannot be the same
assert( pObjOld != pObjNewR );
// make sure object is not pointing to itself
assert( pObjOld != Aig_ObjFanin0(pObjNewR) );
assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
if ( pObjOld == Aig_ObjFanin0(pObjNewR) || pObjOld == Aig_ObjFanin1(pObjNewR) )
{
printf( "Aig_ObjReplace(): Internal error!\n" );
exit(1);
}
// recursively delete the old node - but leave the object there
pObjNewR->nRefs++;
if ( !Aig_ObjIsPi(pObjOld) )
Aig_ObjDelete_rec( p, pObjOld, 0 );
pObjNewR->nRefs--;
// if the new object is complemented or already used, create a buffer
p->nObjs[pObjOld->Type]--;
if ( Aig_IsComplement(pObjNew) || Aig_ObjRefs(pObjNew) > 0 || (fNodesOnly && !Aig_ObjIsNode(pObjNew)) )
{
pObjOld->Type = AIG_OBJ_BUF;
Aig_ObjConnect( p, pObjOld, pObjNew, NULL );
p->nBufReplaces++;
}
else
{
Aig_Obj_t * pFanin0 = pObjNew->pFanin0;
Aig_Obj_t * pFanin1 = pObjNew->pFanin1;
int LevelOld = pObjOld->Level;
pObjOld->Type = pObjNew->Type;
Aig_ObjDisconnect( p, pObjNew );
Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
// update the haig node
pObjOld->pHaig = pObjNew->pHaig;
// delete the new object
Aig_ObjDelete( p, pObjNew );
// update levels
if ( p->pFanData )
{
pObjOld->Level = LevelOld;
Aig_ManUpdateLevel( p, pObjOld );
}
if ( fUpdateLevel )
{
Aig_ObjClearReverseLevel( p, pObjOld );
Aig_ManUpdateReverseLevel( p, pObjOld );
}
}
p->nObjs[pObjOld->Type]++;
// store buffers if fanout is allocated
if ( p->pFanData && Aig_ObjIsBuf(pObjOld) )
{
Vec_PtrPush( p->vBufs, pObjOld );
p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel );
}
pObjOld->pHaig = pHaig;
}
/**Function*************************************************************
Synopsis [Verbose printing of the AIG node.]
@ -498,6 +363,166 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
printf( " class of %d", pObj->Id );
}
/**Function*************************************************************
Synopsis [Replaces node with a buffer fanin by a node without them.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fUpdateLevel )
{
Aig_Obj_t * pFanReal0, * pFanReal1, * pResult;
p->nBufFixes++;
if ( Aig_ObjIsPo(pObj) )
{
assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) );
pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
assert( Aig_ObjPhaseReal(Aig_ObjChild0(pObj)) == Aig_ObjPhaseReal(pFanReal0) );
Aig_ObjPatchFanin0( p, pObj, pFanReal0 );
return;
}
assert( Aig_ObjIsNode(pObj) );
assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) || Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) );
// get the real fanins
pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
pFanReal1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
// get the new node
if ( Aig_ObjIsNode(pObj) )
pResult = Aig_Oper( p, pFanReal0, pFanReal1, Aig_ObjType(pObj) );
// else if ( Aig_ObjIsLatch(pObj) )
// pResult = Aig_Latch( p, pFanReal0, Aig_ObjInit(pObj) );
else
assert( 0 );
// replace the node with buffer by the node without buffer
Aig_ObjReplace( p, pObj, pResult, fUpdateLevel );
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManPropagateBuffers( Aig_Man_t * p, int fUpdateLevel )
{
Aig_Obj_t * pObj;
int nSteps;
assert( p->pFanData );
for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
{
// get the node with a buffer fanin
for ( pObj = Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) );
// replace this node by a node without buffer
Aig_NodeFixBufferFanins( p, pObj, fUpdateLevel );
// stop if a cycle occured
if ( nSteps > 1000000 )
{
printf( "Error: A cycle is encountered while propagating buffers.\n" );
break;
}
}
return nSteps;
}
/**Function*************************************************************
Synopsis [Replaces one object by another.]
Description [The new object (pObjNew) should be used instead of the old
object (pObjOld). If the new object is complemented or used, the buffer
is added and the new object remains in the manager; otherwise, the new
object is deleted.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fUpdateLevel )
{
Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
// the object to be replaced cannot be complemented
assert( !Aig_IsComplement(pObjOld) );
// the object to be replaced cannot be a terminal
assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) );
// the object to be used cannot be a buffer or a PO
assert( !Aig_ObjIsBuf(pObjNewR) && !Aig_ObjIsPo(pObjNewR) );
// the object cannot be the same
assert( pObjOld != pObjNewR );
// make sure object is not pointing to itself
assert( pObjOld != Aig_ObjFanin0(pObjNewR) );
assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
if ( pObjOld == Aig_ObjFanin0(pObjNewR) || pObjOld == Aig_ObjFanin1(pObjNewR) )
{
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( pObjNewR->pHaig->pHaig == NULL );
assert( !Aig_IsComplement(pObjNewR->pHaig) );
pObjNewR->pHaig->pHaig = pObjOld->pHaig;
}
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 );
pObjNewR->nRefs--;
// if the new object is complemented or already used, create a buffer
p->nObjs[pObjOld->Type]--;
if ( Aig_IsComplement(pObjNew) || Aig_ObjRefs(pObjNew) > 0 || !Aig_ObjIsNode(pObjNew) )
{
pObjOld->Type = AIG_OBJ_BUF;
Aig_ObjConnect( p, pObjOld, pObjNew, NULL );
p->nBufReplaces++;
}
else
{
Aig_Obj_t * pFanin0 = pObjNew->pFanin0;
Aig_Obj_t * pFanin1 = pObjNew->pFanin1;
int LevelOld = pObjOld->Level;
pObjOld->Type = pObjNew->Type;
Aig_ObjDisconnect( p, pObjNew );
Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
// delete the new object
Aig_ObjDelete( p, pObjNew );
// update levels
if ( p->pFanData )
{
pObjOld->Level = LevelOld;
Aig_ManUpdateLevel( p, pObjOld );
}
if ( fUpdateLevel )
{
Aig_ObjClearReverseLevel( p, pObjOld );
Aig_ManUpdateReverseLevel( p, pObjOld );
}
}
p->nObjs[pObjOld->Type]++;
// store buffers if fanout is allocated
if ( p->pFanData && Aig_ObjIsBuf(pObjOld) )
{
Vec_PtrPush( p->vBufs, pObjOld );
p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
Aig_ManPropagateBuffers( p, fUpdateLevel );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/aig/aigPart.c
View File

@ -1323,7 +1323,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
// create the equivalent nodes lists
Aig_ManMarkValidChoices( pAig );
// reconstruct the network
pAig = Aig_ManDupDfsOrder( pTemp = pAig, Vec_PtrEntry(vAigs,0) );
pAig = Aig_ManDupDfsGuided( pTemp = pAig, Vec_PtrEntry(vAigs,0) );
Aig_ManStop( pTemp );
// duplicate the timing manager
pTemp = Vec_PtrEntry( vAigs, 0 );
@ -1566,7 +1566,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
// create the equivalent nodes lists
Aig_ManMarkValidChoices( pNew );
// reconstruct the network
pNew = Aig_ManDupDfsOrder( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) );
pNew = Aig_ManDupDfsGuided( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) );
Aig_ManStop( pTemp );
// duplicate the timing manager
pTemp = Vec_PtrEntry( vAigs, 0 );

4
src/aig/aig/aigScl.c
View File

@ -103,7 +103,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDup(): The check has failed.\n" );
printf( "Aig_ManRemap(): The check has failed.\n" );
return pNew;
}
@ -598,7 +598,7 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
// store the original AIG
assert( pAig->vFlopNums == NULL );
pAigInit = pAig;
pAig = Aig_ManDup( pAig );
pAig = Aig_ManDupSimple( pAig );
// create storage for latch numbers
pAig->vFlopNums = Vec_IntStartNatural( pAig->nRegs );
pAig->vFlopReprs = Vec_IntAlloc( 100 );

3
src/aig/aig/aigTable.c
View File

@ -68,6 +68,7 @@ void Aig_TableResize( Aig_Man_t * p )
Aig_Obj_t * pEntry, * pNext;
Aig_Obj_t ** pTableOld, ** ppPlace;
int nTableSizeOld, Counter, i, clk;
assert( p->pTable != NULL );
clk = clock();
// save the old table
pTableOld = p->pTable;
@ -115,7 +116,7 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
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)) )
if ( p->pTable == NULL || !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 )
{

2
src/aig/cnf/cnfWrite.c
View File

@ -333,7 +333,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
Synopsis [Derives a simple CNF for the AIG.]
Description [The last argument shows the number of last outputs
Description [The last argument lists the number of last outputs
of the manager, which will not be converted into clauses.
New variables will be introduced for these outputs.]

28
src/aig/dar/darBalance.c
View File

@ -353,7 +353,18 @@ 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 );
Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
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( pObjNewR->pHaig->pHaig == NULL );
assert( !Aig_IsComplement(pObjNewR->pHaig) );
pObjNewR->pHaig->pHaig = pObjOld->pHaig;
}
else
Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
return pObjOld->pData = pObjNew;
}
@ -383,6 +394,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pNew->nAsserts = p->nAsserts;
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);
@ -401,6 +418,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
// copy the PI
pObjNew = Aig_ObjCreatePi(pNew);
pObj->pData = pObjNew;
pObjNew->pHaig = pObj->pHaig;
// set the arrival time of the new PI
arrTime = Tim_ManGetCiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
pObjNew->Level = (int)arrTime;
@ -411,10 +429,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
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_ManSetCoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
// create PO
pObjNew = Aig_ObjCreatePo( pNew, pObjNew );
pObjNew->pHaig = pObj->pHaig;
}
else
assert( 0 );
@ -429,13 +449,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
pObjNew = Aig_ObjCreatePi(pNew);
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
pObjNew->pHaig = pObj->pHaig;
}
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 );
pObjNew = Aig_ObjCreatePo( pNew, pObjNew );
pObjNew->pHaig = pObj->pHaig;
}
}
Vec_VecFree( vStore );

4
src/aig/dar/darCore.c
View File

@ -133,7 +133,7 @@ p->timeCuts += clock() - clk;
// remove the old cuts
Dar_ObjSetCuts( pObj, NULL );
// replace the node
Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
continue;
}
@ -156,7 +156,7 @@ p->timeCuts += clock() - clk;
pObjNew = Aig_NotCond( pObjNew, Aig_ObjPhaseReal(pObjNew) ^ pObj->fPhase );
assert( (int)Aig_Regular(pObjNew)->Level <= Required );
// replace the node
Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
// compare the gains
nNodeAfter = Aig_ManNodeNum( pAig );
assert( p->GainBest <= nNodeBefore - nNodeAfter );

2
src/aig/dar/darRefact.c
View File

@ -582,7 +582,7 @@ p->timeEval += clock() - clk;
pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest );
assert( (int)Aig_Regular(pObjNew)->Level <= Required );
// replace the node
Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
// compare the gains
nNodeAfter = Aig_ManNodeNum( pAig );
assert( p->GainBest <= nNodeBefore - nNodeAfter );

6
src/aig/fra/fraInd.c
View File

@ -105,9 +105,9 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p
// set the new node
Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
// add the constraint
pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
pMiter = Aig_Not( pMiter );
pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
assert( Aig_ObjPhaseReal(pMiter) == 1 );
Aig_ObjCreatePo( pManFraig, pMiter );
}

34
src/aig/fra/fraSec.c
View File

@ -82,7 +82,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
float TimeLeft = 0.0;
// try the miter before solving
pNew = Aig_ManDup( p );
pNew = Aig_ManDupSimple( p );
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue >= 0 )
goto finish;
@ -144,7 +144,7 @@ clk = clock();
PRT( "Time", clock() - clk );
}
}
// run latch correspondence
clk = clock();
if ( pNew->nRegs )
@ -165,21 +165,26 @@ clk = clock();
}
}
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
if ( pNew == NULL )
{
pNew = pTemp;
RetValue = -1;
TimeOut = 1;
goto finish;
}
p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
Aig_ManStop( pTemp );
if ( pNew == NULL )
{
RetValue = 0;
printf( "Networks are NOT EQUIVALENT after simulation. " );
if ( p->pSeqModel )
{
RetValue = 0;
printf( "Networks are NOT EQUIVALENT after simulation. " );
PRT( "Time", clock() - clkTotal );
return RetValue;
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
PRT( "Time", clock() - clkTotal );
}
return RetValue;
}
pNew = pTemp;
RetValue = -1;
TimeOut = 1;
goto finish;
}
if ( pParSec->fVerbose )
@ -354,6 +359,11 @@ PRT( "Time", clock() - clk );
RetValue = 0;
printf( "Networks are NOT EQUIVALENT after simulation. " );
PRT( "Time", clock() - clkTotal );
if ( pParSec->fReportSolution && !pParSec->fRecursive )
{
printf( "SOLUTION: FAIL " );
PRT( "Time", clock() - clkTotal );
}
return RetValue;
}
Fra_SmlStop( pSml );

BIN
src/aig/fra/fraSec80516.zip Normal file
View File

Binary file not shown.

2
src/aig/fra/fraSim.c
View File

@ -994,7 +994,7 @@ Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
}
return pCex;
}
/**Function*************************************************************
Synopsis [Generates seq counter-example from the combinational one.]

2
src/aig/ntl/ntlMap.c
View File

@ -129,7 +129,7 @@ void Ntl_ManSetIfParsDefault( If_Par_t * pPars )
pPars->nFlowIters = 1;
pPars->nAreaIters = 2;
pPars->DelayTarget = -1;
pPars->Epsilon = (float)0.001;
pPars->Epsilon = (float)0.005;
pPars->fPreprocess = 1;
pPars->fArea = 0;
pPars->fFancy = 0;

5
src/aig/nwk/nwk.h
View File

@ -29,8 +29,6 @@ extern "C" {
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#pragma warning( disable : 4273 )
#include "aig.h"
#include "hop.h"
#include "tim.h"
@ -119,6 +117,9 @@ struct Nwk_Obj_t_
////////////////////////////////////////////////////////////////////////
/// INLINED FUNCTIONS ///
////////////////////////////////////////////////////////////////////////
//#pragma warning( disable : 4273 )
#ifdef WIN32
#define DLLEXPORT __declspec(dllexport)
#define DLLIMPORT __declspec(dllimport)

1
src/aig/saig/module.make
View File

@ -1,5 +1,6 @@
SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigCone.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigInter.c \
src/aig/saig/saigIoa.c \
src/aig/saig/saigPhase.c \

2
src/aig/saig/saig.h
View File

@ -79,6 +79,8 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) {
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigHaig.c ==========================================================*/
extern void Saig_ManHaigRecord( Aig_Man_t * p );
/*=== saigIoa.c ==========================================================*/
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );

29
src/aig/saig/saigBmc.c
View File

@ -145,11 +145,11 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
{
pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
if ( Counter >= nSizeMax )
{
Aig_ManCleanup( pFrames );
return pFrames;
}
}
if ( Counter >= nSizeMax )
{
Aig_ManCleanup( pFrames );
return pFrames;
}
if ( f == nFrames - 1 )
break;
@ -201,6 +201,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames),
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
PRT( "Time", clock() - clk );
fflush( stdout );
}
// rewrite the timeframes
if ( fRewrite )
@ -214,6 +215,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
PRT( "Time", clock() - clk );
fflush( stdout );
}
}
// create the SAT solver
@ -230,15 +232,20 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
{
printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
PRT( "Time", clock() - clk );
fflush( stdout );
}
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
if ( fVerbose )
{
printf( "The BMC problem is trivially UNSAT\n" );
fflush( stdout );
}
}
else
{
int clkPart = clock();
Aig_ManForEachPo( pFrames, pObj, i )
{
Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
@ -247,12 +254,14 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
clk = clock();
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( fVerbose )
if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
{
printf( "Solved output %2d of frame %3d. ",
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
printf( "Solved %2d outputs of frame %3d. ",
Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
PRT( "Time", clock() - clk );
PRT( "Time", clock() - clkPart );
clkPart = clock();
fflush( stdout );
}
if ( status == l_False )
{
@ -272,7 +281,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
}
else
{
*piFrame = i;
*piFrame = i / Saig_ManPoNum(pAig);
RetValue = -1;
break;
}

472
src/aig/saig/saigHaig.c Normal file
View File

@ -0,0 +1,472 @@
/**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 "satSolver.h"
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// 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;
// skip nodes without representative
pObjRepr = pObj->pHaig;
if ( pObjRepr == NULL )
return;
assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = pObj->pData;
// get the new node of the representative
pObjReprNew = pObjRepr->pData;
// if this is the same node, no need to add constraints
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
pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
assert( Aig_ObjPhaseReal(pMiter) == 1 );
Aig_ObjCreatePo( pFrames, pMiter );
}
/**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 = Aig_UtilStrsav( pHaig->pName );
pFrames->pSpec = Aig_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_ObjCreatePi( pFrames );
// add timeframes
Aig_ManSetPioNumbers( pHaig );
for ( f = 0; f < nFrames; f++ )
{
Aig_ManForEachObj( pHaig, pObj, i )
{
if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPo(pObj) )
continue;
if ( Saig_ObjIsPi(pHaig, pObj) )
{
pObj->pData = Aig_ObjCreatePi( pFrames );
continue;
}
if ( Saig_ObjIsLo(pHaig, pObj) )
{
Aig_ManHaigSpeculate( pFrames, pObj );
continue;
}
if ( Aig_ObjIsNode(pObj) )
{
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_ManHaigSpeculate( pFrames, pObj );
continue;
}
assert( 0 );
}
if ( f == nFrames - 2 )
nAssumptions = Aig_ManPoNum(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_ManPoNum(pFrames) - nAssumptions;
Aig_ManSetRegNum( pFrames, 0 );
return pFrames;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
{
int nBTLimit = 0;
Aig_Man_t * pFrames;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj;
int i, Lit, RetValue, Counter;
int clk = clock();
// create time frames with speculative reduction and convert them into CNF
clk = clock();
pFrames = Aig_ManHaigFrames( pHaig, nFrames );
Aig_ManShow( pFrames, 0, NULL );
printf( "AIG: " );
Aig_ManPrintStats( pAig );
printf( "HAIG: " );
Aig_ManPrintStats( pHaig );
printf( "Frames: " );
Aig_ManPrintStats( pFrames );
printf( "Additional frames stats: Assumptions = %d. Asserts = %d.\n",
Aig_ManPoNum(pFrames) - pFrames->nAsserts, pFrames->nAsserts );
pCnf = Cnf_DeriveSimple( pFrames, pFrames->nAsserts );
PRT( "Preparation", clock() - clk );
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(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 = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
return -1;
}
// solve each output
clk = clock();
if ( pFrames->nAsserts == 0 )
{
RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
printf( "SAT solver is wrong\n" );
}
else
{
Counter = 0;
Aig_ManForEachPo( pFrames, pObj, i )
{
if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
continue;
Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
Counter++;
}
PRT( "Solving ", clock() - clk );
if ( Counter )
printf( "Verification failed for %d classes.\n", Counter );
else
printf( "Verification is successful.\n" );
}
// clean up
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
{
int nBTLimit = 0;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj, * pRepr;
int i, RetValue, Counter, Lits[2];
int nClasses = 0;
int clk = clock();
assert( nFrames == 1 || nFrames == 2 );
clk = clock();
pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) );
// create the SAT solver to be used for this problem
pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
if ( pSat == NULL )
{
printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
return -1;
}
if ( nFrames == 2 )
{
// add clauses for the first frame
Aig_ManForEachObj( pHaig, pObj, i )
{
pRepr = pObj->pHaig;
if ( pRepr == NULL )
continue;
if ( pRepr->fPhase ^ pObj->fPhase )
{
Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pRepr->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[pObj->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pRepr->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;
}
}
}
// add clauses for the next timeframe
{
int nLitsAll = 2 * pCnf->nVars;
int * pLits = pCnf->pClauses[0];
for ( i = 0; i < pCnf->nLiterals; i++ )
pLits[i] += nLitsAll;
}
}
PRT( "Preparation", clock() - clk );
// check in the second timeframe
clk = clock();
Counter = 0;
nClasses = 0;
Aig_ManForEachObj( pHaig, pObj, i )
{
pRepr = pObj->pHaig;
if ( pRepr == NULL )
continue;
nClasses++;
if ( pRepr->fPhase ^ pObj->fPhase )
{
Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
Counter++;
Lits[0]++;
Lits[1]++;
RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
Counter++;
}
else
{
Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
Counter++;
Lits[0]++;
Lits[1]--;
RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_False )
Counter++;
}
}
PRT( "Solving ", clock() - clk );
if ( Counter )
printf( "Verification failed for %d out of %d classes.\n", Counter, nClasses );
else
printf( "Verification is successful for all %d classes.\n", nClasses );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManHaigRecord( Aig_Man_t * p )
{
extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
int fUseRetiming = (int)( Aig_ManRegNum(p) > 0 );
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Aig_Man_t * pNew, * pTemp;
Aig_Obj_t * pObj;
int i;
Dar_ManDefaultRwrParams( pParsRwr );
// duplicate this manager
pNew = Aig_ManDupSimple( p );
// create its history AIG
pNew->pManHaig = Aig_ManDupSimple( pNew );
Aig_ManForEachObj( pNew, pObj, i )
pObj->pHaig = pObj->pData;
// remove structural hashing table
Aig_TableClear( pNew->pManHaig );
// perform retiming
if ( fUseRetiming )
{
/*
// perform balancing
pNew = Dar_ManBalance( pTemp = pNew, 0 );
assert( pNew->pManHaig != NULL );
assert( pTemp->pManHaig == NULL );
Aig_ManStop( pTemp );
// perform rewriting
Dar_ManRewrite( pNew, pParsRwr );
pNew = Aig_ManDupDfs( pTemp = pNew );
assert( pNew->pManHaig != NULL );
assert( pTemp->pManHaig == NULL );
Aig_ManStop( pTemp );
*/
// perform retiming
Saig_ManRetimeSteps( pNew, 1000, 1 );
pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
assert( pNew->pManHaig != NULL );
assert( pTemp->pManHaig == NULL );
Aig_ManStop( pTemp );
// perform balancing
pNew = Dar_ManBalance( pTemp = pNew, 0 );
assert( pNew->pManHaig != NULL );
assert( pTemp->pManHaig == NULL );
Aig_ManStop( pTemp );
// perform rewriting
Dar_ManRewrite( pNew, pParsRwr );
pNew = Aig_ManDupDfs( pTemp = pNew );
assert( pNew->pManHaig != NULL );
assert( pTemp->pManHaig == NULL );
Aig_ManStop( pTemp );
}
else
{
// perform balancing
pNew = Dar_ManBalance( pTemp = pNew, 0 );
assert( pNew->pManHaig != NULL );
assert( pTemp->pManHaig == NULL );
Aig_ManStop( pTemp );
/*
// perform rewriting
Dar_ManRewrite( pNew, pParsRwr );
pNew = Aig_ManDupDfs( pTemp = pNew );
assert( pNew->pManHaig != NULL );
assert( pTemp->pManHaig == NULL );
Aig_ManStop( pTemp );
*/
}
// use the haig for verification
Aig_ManAntiCleanup( pNew->pManHaig );
Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
//Aig_ManShow( pNew->pManHaig, 0, NULL );
printf( "AIG: " );
Aig_ManPrintStats( pNew );
printf( "HAIG: " );
Aig_ManPrintStats( pNew->pManHaig );
if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fUseRetiming ) )
printf( "Constructing SAT solver has failed.\n" );
// cleanup
Aig_ManStop( pNew->pManHaig );
pNew->pManHaig = NULL;
Aig_ManStop( pNew );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/saig/saigPhase.c
View File

@ -885,7 +885,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
Saig_TsiStop( pTsi );
if ( pNew == NULL )
pNew = Aig_ManDup( p );
pNew = Aig_ManDupSimple( p );
return pNew;
}

4
src/aig/saig/saigRetMin.c
View File

@ -622,7 +622,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
Vec_Ptr_t * vCut;
Aig_Man_t * pNew, * pTemp, * pCopy;
int i, fChanges;
pNew = Aig_ManDup( p );
pNew = Aig_ManDupSimple( p );
// perform several iterations of forward retiming
fChanges = 0;
if ( !fBackwardOnly )
@ -672,7 +672,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
{
if ( Saig_ManRegNum(pNew) == 0 )
break;
pCopy = Aig_ManDup( pNew );
pCopy = Aig_ManDupSimple( pNew );
pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
Aig_ManStop( pCopy );
if ( pTemp == NULL )

19
src/aig/saig/saigRetStep.c
View File

@ -44,6 +44,7 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
Aig_Obj_t * pFanin0, * pFanin1;
Aig_Obj_t * pInput0, * pInput1;
Aig_Obj_t * pObjNew, * pObjLi, * pObjLo;
int fCompl;
assert( Saig_ManRegNum(p) > 0 );
assert( Aig_ObjIsNode(pObj) );
@ -68,22 +69,26 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
pInput1 = Aig_ObjChild0( pInput1 );
pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) );
pInput1 = Aig_NotCond( pInput1, Aig_ObjFaninC1(pObj) );
// get the condition when the register should be complemetned
fCompl = Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj);
// create new node
pObjNew = Aig_And( p, pInput0, pInput1 );
// create new register input
pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, pObjNew->fPhase) );
pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, fCompl) );
pObjLi->PioNum = Aig_ManPoNum(p) - 1;
assert( pObjLi->fPhase == 0 );
// create new register output
pObjLo = Aig_ObjCreatePi( p );
pObjLo->PioNum = Aig_ManPiNum(p) - 1;
p->nRegs++;
//printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n",
// pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl );
// return register output
return Aig_NotCond( pObjLo, pObjNew->fPhase );
return Aig_NotCond( pObjLo, fCompl );
}
/**Function*************************************************************
@ -163,6 +168,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
int RetValue, s, i;
Aig_ManSetPioNumbers( p );
Aig_ManFanoutStart( p );
p->fCreatePios = 1;
if ( fForward )
{
for ( s = 0; s < nSteps; s++ )
@ -172,7 +178,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
pObjNew = Saig_ManRetimeNodeFwd( p, pObj );
if ( pObjNew == NULL )
continue;
Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
Aig_ObjReplace( p, pObj, pObjNew, 0 );
break;
}
}
@ -186,13 +192,16 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
pObjNew = Saig_ManRetimeNodeBwd( p, pObj );
if ( pObjNew == NULL )
continue;
Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
Aig_ObjReplace( p, pObj, pObjNew, 0 );
break;
}
}
}
p->fCreatePios = 0;
Aig_ManFanoutStop( p );
RetValue = Aig_ManCleanup( p );
assert( RetValue == 0 );
Aig_ManSetRegNum( p, p->nRegs );
}
////////////////////////////////////////////////////////////////////////

4
src/base/abc/abc.h
View File

@ -29,8 +29,6 @@ extern "C" {
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#pragma warning( disable : 4273 )
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
@ -226,6 +224,8 @@ struct Abc_Lib_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
//#pragma warning( disable : 4273 )
#ifdef WIN32
#define DLLEXPORT __declspec(dllexport)
#define DLLIMPORT __declspec(dllimport)

57
src/base/abci/abc.c
View File

@ -2762,19 +2762,36 @@ usage:
int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int fCleanupPis;
int fCleanupPos;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fCleanupPis = 1;
fCleanupPos = 1;
fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "iovh" ) ) != EOF )
{
switch ( c )
{
case 'i':
fCleanupPis ^= 1;
break;
case 'o':
fCleanupPos ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -2789,16 +2806,35 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
if ( !fCleanupPos && !fCleanupPos )
{
printf( "Cleanup for PIs and POs is not enabled.\n" );
pNtkRes = Abc_NtkDup( pNtk );
}
else
pNtkRes = Abc_NtkDarCleanupAig( pNtk, fCleanupPis, fCleanupPos, fVerbose );
}
else
{
Abc_NtkCleanup( pNtk, fVerbose );
pNtkRes = Abc_NtkDup( pNtk );
}
if ( pNtkRes == NULL )
{
fprintf( pErr, "Cleanup has failed.\n" );
return 1;
}
// modify the current network
Abc_NtkCleanup( pNtk, 1 );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: cleanup [-h]\n" );
fprintf( pErr, "\t removes dangling nodes\n" );
fprintf( pErr, "usage: cleanup [-iovh]\n" );
fprintf( pErr, "\t for logic networks, removes dangling combinatinal logic\n" );
fprintf( pErr, "\t for AIGs, removes PIs w/o fanout and POs driven by const-0\n" );
fprintf( pErr, "\t-i : toggles removing PIs without fanout [default = %s]\n", fCleanupPis? "yes": "no" );
fprintf( pErr, "\t-o : toggles removing POs with const-0 drivers [default = %s]\n", fCleanupPos? "yes": "no" );
fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -7469,7 +7505,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
// extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
// extern void Abc_NtkDarTestBlif( char * pFileName );
// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
@ -7661,7 +7697,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
// Abc_NtkDarPartition( pNtk );
Abc_NtkDarTest( pNtk );
//Abc_NtkDarTest( pNtk );
Abc_NtkDarHaigRecord( pNtk );
return 0;
pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );

98
src/base/abci/abcDar.c
View File

@ -94,16 +94,6 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
pMan->fCatchExor = fExors;
pMan->pName = Extra_UtilStrsav( pNtk->pName );
// save the number of registers
if ( fRegisters )
{
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
// pMan->vFlopNums = NULL;
// pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
if ( pNtk->vOnehots )
pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
}
// transfer the pointers to the basic nodes
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
Abc_NtkForEachCi( pNtk, pObj, i )
@ -134,6 +124,16 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
if ( !fExors && nNodes )
printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
//Aig_ManDumpVerilog( pMan, "test.v" );
// save the number of registers
if ( fRegisters )
{
Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
// pMan->vFlopNums = NULL;
// pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
if ( pNtk->vOnehots )
pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
}
if ( !Aig_ManCheck( pMan ) )
{
printf( "Abc_NtkToDar: AIG check has failed.\n" );
@ -1220,8 +1220,6 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
return RetValue;
}
assert( pMan->nRegs > 0 );
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
// perform verification
if ( fNewAlgo )
{
@ -1282,8 +1280,6 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra
return -1;
}
assert( pMan->nRegs > 0 );
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fVerbose, &Depth );
if ( RetValue == 1 )
printf( "Property proved. " );
@ -1593,9 +1589,6 @@ Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbo
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
Aig_ManStop( pTemp );
@ -1630,9 +1623,6 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwa
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
Aig_ManStop( pTemp );
@ -1664,11 +1654,8 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
Aig_ManPrintStats(pMan);
Saig_ManRetimeSteps( pMan, 1, 0 );
Saig_ManRetimeSteps( pMan, 1000, 1 );
Aig_ManPrintStats(pMan);
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
@ -1689,18 +1676,16 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
***********************************************************************/
void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
{
/*
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return;
// Aig_ManReduceLachesCount( pMan );
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
Aig_ManHaigRecord( pMan );
Saig_ManHaigRecord( pMan );
Aig_ManStop( pMan );
*/
}
/**Function*************************************************************
@ -2006,8 +1991,6 @@ void Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
if ( pMan == NULL )
return;
assert( Aig_ManRegNum(pMan) > 0 );
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
Saig_ManPrintCones( pMan );
Aig_ManStop( pMan );
}
@ -2063,10 +2046,7 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
Vec_Int_t * vInits;
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 0 );
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
vInits = Abc_NtkGetLatchValues(pNtk);
@ -2097,10 +2077,7 @@ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fI
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 0 );
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
@ -2114,6 +2091,43 @@ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fI
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Performs phase abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
if ( fCleanupPis )
{
int Temp = Aig_ManPiCleanup( pMan );
if ( fVerbose )
printf( "Cleanup removed %d primary inputs without fanout.\n", Temp );
}
if ( fCleanupPos )
{
int Temp = Aig_ManPoCleanup( pMan );
if ( fVerbose )
printf( "Cleanup removed %d primary outputs driven by const-0.\n", Temp );
}
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Performs BDD-based reachability analysis.]
@ -2129,10 +2143,7 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
{
extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 0 );
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return;
Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
@ -2156,9 +2167,6 @@ void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
Aig_Man_t * pMan;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
if ( pMan == NULL )
return;

1
src/base/abci/abcRec.c
View File

@ -523,6 +523,7 @@ void Abc_NtkRecAdd( Abc_Ntk_t * pNtk )
pPars->nFlowIters = 0;
pPars->nAreaIters = 0;
pPars->DelayTarget = -1;
pPars->Epsilon = (float)0.005;
pPars->fPreprocess = 0;
pPars->fArea = 1;
pPars->fFancy = 0;

1
src/base/abci/abcRenode.c
View File

@ -74,6 +74,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
pPars->nFlowIters = nFlowIters;
pPars->nAreaIters = nAreaIters;
pPars->DelayTarget = -1;
pPars->Epsilon = (float)0.005;
pPars->fPreprocess = 1;
pPars->fArea = fArea;
pPars->fFancy = 0;

1
src/opt/lpk/lpkCore.c
View File

@ -53,6 +53,7 @@ void Lpk_IfManStart( Lpk_Man_t * p )
pPars->nFlowIters = 0; // 1
pPars->nAreaIters = 0; // 1
pPars->DelayTarget = -1;
pPars->Epsilon = (float)0.005;
pPars->fPreprocess = 0;
pPars->fArea = 1;
pPars->fFancy = 0;