Skip to content

A
abc
Commit 416ffc11 by Alan Mishchenko
Options

Version abc80327

parent e258fcb2
Showing with 1768 additions and 441 deletions
Makefile
......@@ -19,7 +19,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
src/aig/bdc src/aig/bar src/aig/ntl src/aig/tim
src/aig/bdc src/aig/bar src/aig/ntl src/aig/ntk src/aig/tim
default: $(PROG)
......
abc.dsp
......@@ -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/tim" /I "src/opt/mfs" /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/ntk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /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/tim" /I "src/opt/mfs" /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/ntk" /I "src/aig/tim" /I "src/opt/mfs" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
......@@ -1898,6 +1898,10 @@ SOURCE=.\src\map\if\ifCut.c
# End Source File
# Begin Source File
SOURCE=.\src\map\if\ifLib.c
# End Source File
# Begin Source File
SOURCE=.\src\map\if\ifMan.c
# End Source File
# Begin Source File
......@@ -2478,6 +2482,10 @@ SOURCE=.\src\aig\hop\hopTable.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\hop\hopTruth.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\hop\hopUtil.c
# End Source File
# End Group
......@@ -2942,10 +2950,6 @@ SOURCE=.\src\aig\aig\aigFrames.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigHaig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigInter.c
# End Source File
# Begin Source File
......@@ -3102,6 +3106,14 @@ SOURCE=.\src\aig\ntk\ntk.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntk\ntkBidec.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntk\ntkCheck.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ntk\ntkDfs.c
# End Source File
# Begin Source File
......
src/aig/aig/aig.h
......@@ -103,6 +103,7 @@ struct Aig_Box_t_
struct Aig_Man_t_
{
char * pName; // the design name
char * pSpec; // the input file name
// AIG nodes
Vec_Ptr_t * vPis; // the array of PIs
Vec_Ptr_t * vPos; // the array of POs
......@@ -328,7 +329,6 @@ static inline int Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert(
static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); }
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_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)pObj->pNext; }
static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{
......@@ -540,6 +540,7 @@ extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
extern Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
extern Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose );
/*=== aigPartReg.c =========================================================*/
extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
......@@ -612,6 +613,7 @@ extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
extern void Aig_ManSetPioNumbers( Aig_Man_t * p );
extern void Aig_ManCleanPioNumbers( Aig_Man_t * p );
extern int Aig_ManCountChoices( Aig_Man_t * p );
/*=== aigWin.c =========================================================*/
extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
......
src/aig/aig/aigMan.c
......@@ -96,6 +96,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->Level = pObj->Level;
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
return pNew;
......@@ -114,20 +115,16 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
***********************************************************************/
Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjNew;
if ( pObj->pData )
return pObj->pData;
Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
if ( Aig_ObjIsBuf(pObj) )
return pObj->pData = Aig_ObjChild0Copy(pObj);
Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
if ( pNew->pManHaig == NULL )
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else
{
Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
return pObj->pData = pObjNew;
}
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
return pObj->pData = pObjNew;
}
/**Function*************************************************************
......@@ -156,8 +153,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
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;
// duplicate internal nodes
if ( fOrdered )
{
......@@ -165,61 +160,42 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
{
if ( Aig_ObjIsBuf(pObj) )
{
if ( pNew->pManHaig == NULL )
pObj->pData = Aig_ObjChild0Copy(pObj);
else
{
Aig_Obj_t * pObjNew = Aig_ObjChild0Copy(pObj);
Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
pObj->pData = pObjNew;
}
pObjNew = Aig_ObjChild0Copy(pObj);
}
else if ( Aig_ObjIsNode(pObj) )
{
if ( pNew->pManHaig == NULL )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
else
{
Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
pObj->pData = pObjNew;
}
pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
else if ( Aig_ObjIsPi(pObj) )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsPo(pObj) )
{
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsConst1(pObj) )
{
pObjNew = Aig_ManConst1(pNew);
}
else
assert( 0 );
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
}
else
{
/*
Aig_ManForEachPi( p, pObj, i )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
pObj->pData = pObjNew;
}
*/
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjIsPi(pObj) )
{
pObjNew = Aig_ObjCreatePi( pNew );
pObjNew->pHaig = pObj->pHaig;
pObjNew->Level = pObj->Level;
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
else if ( Aig_ObjIsPo(pObj) )
......@@ -227,18 +203,10 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
}
/*
Aig_ManForEachPo( p, pObj, i )
{
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
pObjNew->pHaig = pObj->pHaig;
pObj->pData = pObjNew;
}
*/
}
// add the POs
assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
......@@ -372,6 +340,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
FREE( p->pSeqModel );
FREE( p->pName );
FREE( p->pSpec );
FREE( p->pObjCopies );
FREE( p->pReprs );
FREE( p->pEquivs );
......@@ -410,6 +379,27 @@ int Aig_ManCleanup( 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 []
......@@ -421,8 +411,12 @@ int Aig_ManCleanup( Aig_Man_t * p )
***********************************************************************/
void Aig_ManPrintStats( Aig_Man_t * p )
{
int nChoices = Aig_ManCountChoices(p);
printf( "PI/PO/Lat = %5d/%5d/%5d ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
printf( "A = %7d. ", Aig_ManAndNum(p) );
printf( "A = %7d. ", Aig_ManAndNum(p) );
printf( "Eq = %7d. ", Aig_ManHaigCounter(p) );
if ( nChoices )
printf( "Ch = %5d. ", nChoices );
if ( Aig_ManExorNum(p) )
printf( "X = %5d. ", Aig_ManExorNum(p) );
if ( Aig_ManBufNum(p) )
......
src/aig/aig/aigObj.c
......@@ -97,12 +97,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 );
}
*/
return pObj;
}
......@@ -360,6 +362,7 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
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
......@@ -422,6 +425,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel );
}
pObjOld->pHaig = pHaig;
}
////////////////////////////////////////////////////////////////////////
......
src/aig/aig/aigPart.c
......@@ -19,6 +19,7 @@
***********************************************************************/
#include "aig.h"
#include "tim.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -1346,6 +1347,235 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM
}
/**Function*************************************************************
Synopsis [Set the representative.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
{
assert( p->pReprs != NULL );
assert( !Aig_IsComplement(pNode1) );
assert( !Aig_IsComplement(pNode2) );
assert( pNode1->Id < p->nReprsAlloc );
assert( pNode2->Id < p->nReprsAlloc );
if ( pNode1 == pNode2 )
return;
if ( pNode1->Id < pNode2->Id )
p->pReprs[pNode2->Id] = pNode1;
else
p->pReprs[pNode1->Id] = pNode2;
}
/**Function*************************************************************
Synopsis [Constructively accumulates choices.]
Description [pNew is a new AIG with choices under construction.
pPrev is the AIG preceding pThis in the order of deriving choices.
pThis is the current AIG to be added to pNew while creating choices.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_t * pThis )
{
Aig_Obj_t * pObj, * pObjNew;
int i;
assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pPrev) );
assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pThis) );
assert( Aig_ManPoNum(pNew) == Aig_ManPoNum(pPrev) );
assert( Aig_ManPoNum(pNew) == Aig_ManPoNum(pThis) );
// make sure the nodes of pPrev point to pNew
Aig_ManForEachObj( pNew, pObj, i )
pObj->fMarkB = 1;
Aig_ManForEachObj( pPrev, pObj, i )
assert( Aig_Regular(pObj->pData)->fMarkB );
Aig_ManForEachObj( pNew, pObj, i )
pObj->fMarkB = 0;
// 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
pObj = Aig_ManConst1(pThis);
pObj->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( pThis, pObj, i )
pObj->pData = Aig_ManPi(pNew, i);
Aig_ManForEachPo( pThis, pObj, i )
pObj->pData = Aig_ManPo(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(pObj->pData), Aig_Regular(pObj->pHaig->pData) );
}
// set the inputs of POs as equivalent
Aig_ManForEachPo( pThis, pObj, i )
{
pObjNew = Aig_ObjFanin0( Aig_ManPo(pNew,i) );
// pObjNew and Aig_ObjFanin0(pObj)->pData are equivalent
Aig_ObjSetRepr( pNew, pObjNew, Aig_Regular(Aig_ObjFanin0(pObj)->pData) );
}
}
/**Function*************************************************************
Synopsis [Computes levels for AIG with choices and white boxes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
{
Aig_Obj_t * pNext;
int i, iBox, iTerm1, nTerms, LevelMax = 0;
if ( Aig_ObjIsTravIdCurrent( pNew, pObj ) )
return;
Aig_ObjSetTravIdCurrent( pNew, pObj );
if ( Aig_ObjIsPi(pObj) )
{
if ( pNew->pManTime )
{
iBox = Tim_ManBoxForCi( pNew->pManTime, Aig_ObjPioNum(pObj) );
if ( iBox >= 0 ) // this is not a true PI
{
iTerm1 = Tim_ManBoxInputFirst( pNew->pManTime, iBox );
nTerms = Tim_ManBoxInputNum( pNew->pManTime, iBox );
for ( i = 0; i < nTerms; i++ )
{
pNext = Aig_ManPo(pNew, iTerm1 + i);
Aig_ManChoiceLevel_rec( pNew, pNext );
if ( LevelMax < Aig_ObjLevel(pNext) )
LevelMax = Aig_ObjLevel(pNext);
}
LevelMax++;
}
}
}
else if ( Aig_ObjIsPo(pObj) )
{
pNext = Aig_ObjFanin0(pObj);
Aig_ManChoiceLevel_rec( pNew, pNext );
if ( LevelMax < Aig_ObjLevel(pNext) )
LevelMax = Aig_ObjLevel(pNext);
}
else if ( Aig_ObjIsNode(pObj) )
{
// get the maximum level of the two fanins
pNext = Aig_ObjFanin0(pObj);
Aig_ManChoiceLevel_rec( pNew, pNext );
if ( LevelMax < Aig_ObjLevel(pNext) )
LevelMax = Aig_ObjLevel(pNext);
pNext = Aig_ObjFanin1(pObj);
Aig_ManChoiceLevel_rec( pNew, pNext );
if ( LevelMax < Aig_ObjLevel(pNext) )
LevelMax = Aig_ObjLevel(pNext);
LevelMax++;
// get the level of the nodes in the choice node
if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->iData]) )
{
Aig_ManChoiceLevel_rec( pNew, pNext );
if ( LevelMax < Aig_ObjLevel(pNext) )
LevelMax = Aig_ObjLevel(pNext);
}
}
else
assert( 0 );
Aig_ObjSetLevel( pObj, LevelMax );
}
/**Function*************************************************************
Synopsis [Computes levels for AIG with choices and white boxes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManChoiceLevel( Aig_Man_t * pNew )
{
Aig_Obj_t * pObj;
int i, LevelMax = 0;
Aig_ManForEachObj( pNew, pObj, i )
Aig_ObjSetLevel( pObj, 0 );
Aig_ManSetPioNumbers( pNew );
Aig_ManIncrementTravId( pNew );
Aig_ManForEachPo( pNew, pObj, i )
{
Aig_ManChoiceLevel_rec( pNew, pObj );
if ( LevelMax < Aig_ObjLevel(pObj) )
LevelMax = Aig_ObjLevel(pObj);
}
Aig_ManCleanPioNumbers( pNew );
return LevelMax;
}
/**Function*************************************************************
Synopsis [Constructively accumulates choices.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
{
Aig_Man_t * pNew, * pThis, * pPrev;
int i;
// start AIG with choices
pPrev = Vec_PtrEntry( vAigs, 0 );
pNew = Aig_ManDup( pPrev, 1 );
// create room for equivalent nodes and representatives
assert( pNew->pReprs == NULL );
pNew->nReprsAlloc = Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pNew);
pNew->pReprs = ALLOC( Aig_Obj_t *, pNew->nReprsAlloc );
memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * pNew->nReprsAlloc );
// add other AIGs one by one
Vec_PtrForEachEntryStart( vAigs, pThis, i, 1 )
{
Aig_ManChoiceConstructiveOne( pNew, pPrev, pThis );
pPrev = pThis;
}
// derive the result of choicing
//Aig_ManPrintStats( pNew );
pNew = Aig_ManRehash( pNew );
//Aig_ManPrintStats( pNew );
// create the equivalent nodes lists
Aig_ManMarkValidChoices( pNew );
//Aig_ManPrintStats( pNew );
// reset levels
Aig_ManChoiceLevel( pNew );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/aig/aigRetF.c
......@@ -178,6 +178,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
p->nObjs[AIG_OBJ_BUF]++;
Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL );
// create HAIG if defined
/*
if ( p->pManHaig )
{
// create HAIG latch
......@@ -188,6 +189,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
assert( pObjLo->pHaig->pHaig == NULL );
pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig);
}
*/
// mark the change
fChange = 1;
// check the limit
......
src/aig/aig/aigUtil.c
......@@ -890,6 +890,28 @@ void Aig_ManCleanPioNumbers( Aig_Man_t * p )
pObj->pNext = NULL;
}
/**Function*************************************************************
Synopsis [Sets the PI/PO numbers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManCountChoices( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i, Counter = 0;
Aig_ManForEachNode( p, pObj, i )
Counter += Aig_ObjIsChoice( p, pObj );
return Counter;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/aig/module.make
......@@ -3,7 +3,6 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigDfs.c \
src/aig/aig/aigFanout.c \
src/aig/aig/aigFrames.c \
src/aig/aig/aigHaig.c \
src/aig/aig/aigInter.c \
src/aig/aig/aigMan.c \
src/aig/aig/aigMem.c \
......
src/aig/bdc/bdc.h
......@@ -37,6 +37,7 @@ extern "C" {
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Bdc_Fun_t_ Bdc_Fun_t;
typedef struct Bdc_Man_t_ Bdc_Man_t;
typedef struct Bdc_Par_t_ Bdc_Par_t;
struct Bdc_Par_t_
......@@ -47,6 +48,12 @@ struct Bdc_Par_t_
int fVeryVerbose; // enable detailed stats
};
// working with complemented attributes of objects
static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)(c!=0)); }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -59,6 +66,13 @@ struct Bdc_Par_t_
extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
extern void Bdc_ManFree( Bdc_Man_t * p );
extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax );
extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i );
extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p );
extern int Bdc_ManNodeNum( Bdc_Man_t * p );
extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p );
extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p );
extern void * Bdc_FuncCopy( Bdc_Fun_t * p );
extern void Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy );
#ifdef __cplusplus
......
src/aig/bdc/bdcCore.c
......@@ -24,12 +24,32 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Accessing contents of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ) { return Bdc_FunWithId(p, i); }
Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ) { return p->pRoot; }
int Bdc_ManNodeNum( Bdc_Man_t * p ) { return p->nNodes; }
Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ) { return p->pFan0; }
Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ) { return p->pFan1; }
void * Bdc_FuncCopy( Bdc_Fun_t * p ) { return p->pCopy; }
void Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy ) { p->pCopy = pCopy; }
/**Function*************************************************************
Synopsis [Allocate resynthesis manager.]
Description []
......
src/aig/bdc/bdcInt.h
......@@ -54,7 +54,6 @@ typedef enum {
BDC_TYPE_OTHER // 7: unused
} Bdc_Type_t;
typedef struct Bdc_Fun_t_ Bdc_Fun_t;
struct Bdc_Fun_t_
{
int Type; // Const1, PI, AND, XOR, MUX
......@@ -122,12 +121,6 @@ struct Bdc_Man_t_
int timeTotal;
};
// working with complemented attributes of objects
static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)01); }
static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^ (PORT_PTRUINT_T)(c!=0)); }
static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; }
static inline Bdc_Fun_t * Bdc_FunWithId( Bdc_Man_t * p, int Id ) { assert( Id < p->nNodes ); return p->pNodes + Id; }
static inline int Bdc_FunId( Bdc_Man_t * p, Bdc_Fun_t * pFun ) { return pFun - p->pNodes; }
......
src/aig/dar/dar.h
......@@ -92,7 +92,7 @@ extern Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig );
extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
#ifdef __cplusplus
}
......
src/aig/dar/darBalance.c
......@@ -164,6 +164,7 @@ 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;
return pObjOld->pData = pObjNew;
}
......
src/aig/dar/darScript.c
......@@ -112,6 +112,26 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
return pAig;
}
/**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*************************************************************
......@@ -314,42 +334,28 @@ 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_ManDup(pAig, 0);
Vec_PtrPush( vAigs, pAig );
pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
Vec_PtrPush( vAigs, pAig );
pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
Vec_PtrPush( vAigs, pAig );
return vAigs;
}
/**Function*************************************************************
Aig_ManForEachObj( pAig, pObj, i )
pObj->pHaig = pObj;
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );
SeeAlso []
Aig_ManForEachObj( pAig, pObj, i )
pObj->pHaig = pObj;
***********************************************************************/
/*
Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
{
Vec_Ptr_t * vAigs;
Aig_Man_t * pMan;
vAigs = Vec_PtrAlloc( 3 );
pMan = Ioa_ReadAiger( "i10_1.aig", 1 );
Vec_PtrPush( vAigs, pMan );
pMan = Ioa_ReadAiger( "i10_2.aig", 1 );
Vec_PtrPush( vAigs, pMan );
pMan = Ioa_ReadAiger( "i10_3.aig", 1 );
Vec_PtrPush( vAigs, pMan );
pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );
return vAigs;
}
*/
/**Function*************************************************************
......@@ -362,7 +368,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Vec_Ptr_t * vAigs;
......@@ -374,16 +380,22 @@ clk = clock();
// swap the first and last network
// this should lead to the primary choice being "better" because of synthesis
pMan = Vec_PtrPop( vAigs );
Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
Vec_PtrWriteEntry( vAigs, 0, pMan );
if ( !fConstruct )
{
pMan = Vec_PtrPop( vAigs );
Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
Vec_PtrWriteEntry( vAigs, 0, pMan );
}
if ( fVerbose )
{
PRT( "Synthesis time", clock() - clk );
}
clk = clock();
pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
if ( fConstruct )
pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
else
pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
Vec_PtrForEachEntry( vAigs, pTemp, i )
Aig_ManStop( pTemp );
Vec_PtrFree( vAigs );
......
src/aig/hop/hop.h
......@@ -321,6 +321,8 @@ extern void Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj );
extern void Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj );
extern int Hop_TableCountEntries( Hop_Man_t * p );
extern void Hop_TableProfile( Hop_Man_t * p );
/*=== hopTruth.c ========================================================*/
unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
/*=== hopUtil.c =========================================================*/
extern void Hop_ManIncrementTravId( Hop_Man_t * p );
extern void Hop_ManCleanData( Hop_Man_t * p );
......
src/aig/hop/hopTruth.c 0 → 100644
/**CFile****************************************************************
FileName [hopTruth.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Minimalistic And-Inverter Graph package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: hopTruth.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "hop.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Hop_ManTruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline void Hop_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn[w];
}
static inline void Hop_ManTruthClear( unsigned * pOut, int nVars )
{
int w;
for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = 0;
}
static inline void Hop_ManTruthFill( unsigned * pOut, int nVars )
{
int w;
for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~(unsigned)0;
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Construct BDDs and mark AIG nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Hop_ManConvertAigToTruth_rec1( Hop_Obj_t * pObj )
{
int Counter = 0;
assert( !Hop_IsComplement(pObj) );
if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
return 0;
Counter += Hop_ManConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) );
Counter += Hop_ManConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
Hop_ObjSetMarkA( pObj );
return Counter + 1;
}
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Hop_ManConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
{
unsigned * pTruth, * pTruth0, * pTruth1;
int i;
assert( !Hop_IsComplement(pObj) );
if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
return pObj->pData;
// compute the truth tables of the fanins
pTruth0 = Hop_ManConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
pTruth1 = Hop_ManConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
// creat the truth table of the node
pTruth = Vec_IntFetch( vTruth, nWords );
if ( Hop_ObjIsExor(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] ^ pTruth1[i];
else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & pTruth1[i];
else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & ~pTruth1[i];
else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & pTruth1[i];
else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
assert( Hop_ObjIsMarkA(pObj) ); // loop detection
Hop_ObjClearMarkA( pObj );
pObj->pData = pTruth;
return pTruth;
}
/**Function*************************************************************
Synopsis [Computes truth table of the node.]
Description [Assumes that the structural support is no more than 8 inputs.
Uses array vTruth to store temporary truth tables. The returned pointer should
be used immediately.]
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
{
static unsigned uTruths[8][8] = { // elementary truth tables
{ 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
{ 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
{ 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
{ 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
{ 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 },
{ 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF },
{ 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF },
{ 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
};
Hop_Obj_t * pObj;
unsigned * pTruth, * pTruth2;
int i, nWords, nNodes;
Vec_Ptr_t * vTtElems;
// if the number of variables is more than 8, allocate truth tables
if ( nVars > 8 )
vTtElems = Vec_PtrAllocTruthTables( nVars );
else
vTtElems = NULL;
// clear the data fields and set marks
nNodes = Hop_ManConvertAigToTruth_rec1( pRoot );
// prepare memory
nWords = Hop_TruthWordNum( nVars );
Vec_IntClear( vTruth );
Vec_IntGrow( vTruth, nWords * (nNodes+1) );
pTruth = Vec_IntFetch( vTruth, nWords );
// check the case of a constant
if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
{
assert( nNodes == 0 );
if ( Hop_IsComplement(pRoot) )
Hop_ManTruthClear( pTruth, nVars );
else
Hop_ManTruthFill( pTruth, nVars );
return pTruth;
}
// set elementary truth tables at the leaves
assert( nVars <= Hop_ManPiNum(p) );
// assert( Hop_ManPiNum(p) <= 8 );
if ( fMsbFirst )
{
Hop_ManForEachPi( p, pObj, i )
{
if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
else
pObj->pData = (void *)uTruths[nVars-1-i];
}
}
else
{
Hop_ManForEachPi( p, pObj, i )
{
if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, i);
else
pObj->pData = (void *)uTruths[i];
}
}
// clear the marks and compute the truth table
pTruth2 = Hop_ManConvertAigToTruth_rec2( pRoot, vTruth, nWords );
// copy the result
Hop_ManTruthCopy( pTruth, pTruth2, nVars );
if ( vTtElems )
Vec_PtrFree( vTtElems );
return pTruth;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/hop/hop_.c
/**CFile****************************************************************
FileName [ivy_.c]
FileName [hop_.c]
SystemName [ABC: Logic synthesis and verification system.]
......@@ -14,11 +14,11 @@
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
Revision [$Id: hop_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ivy.h"
#include "hop.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......
src/aig/hop/module.make
......@@ -6,4 +6,5 @@ SRC += src/aig/hop/hopBalance.c \
src/aig/hop/hopObj.c \
src/aig/hop/hopOper.c \
src/aig/hop/hopTable.c \
src/aig/hop/hopTruth.c \
src/aig/hop/hopUtil.c
src/aig/ntk/module.make 0 → 100644
SRC += src/aig/ntk/ntkCheck.c \
src/aig/ntk/ntkBidec.c \
src/aig/ntk/ntkDfs.c \
src/aig/ntk/ntkFanio.c \
src/aig/ntk/ntkMan.c \
src/aig/ntk/ntkMap.c \
src/aig/ntk/ntkObj.c \
src/aig/ntk/ntkTiming.c \
src/aig/ntk/ntkUtil.c
src/aig/ntk/ntk.h
......@@ -30,7 +30,9 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
#include "aig.h"
#include "hop.h"
#include "tim.h"
#include "if.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
......@@ -66,7 +68,7 @@ struct Ntk_Man_t_
int nObjs[NTK_OBJ_VOID]; // counter of objects of each type
int nFanioPlus; // the number of extra fanins/fanouts alloc by default
// functionality, timing, memory, etc
Aig_Man_t * pAig; // the functionality representation
Hop_Man_t * pManHop; // the functionality representation
Tim_Man_t * pManTime; // the timing manager
Aig_MmFlex_t * pMemObjs; // memory for objects
Vec_Ptr_t * vTemp; // array used for incremental updates
......@@ -77,9 +79,10 @@ struct Ntk_Obj_t_
{
Ntk_Man_t * pMan; // the manager
void * pCopy; // temporary pointer
void * pFunc; // functionality
Hop_Obj_t * pFunc; // functionality
// node information
int Id; // unique ID
int PioId; // number of this node in the PI/PO list
unsigned Type : 3; // object type
unsigned fCompl : 1; // complemented attribute
unsigned MarkA : 1; // temporary mark
......@@ -113,6 +116,10 @@ static inline int Ntk_ManLatchNum( Ntk_Man_t * p ) { return p->nO
static inline int Ntk_ManBoxNum( Ntk_Man_t * p ) { return p->nObjs[NTK_OBJ_BOX]; }
static inline int Ntk_ManObjNumMax( Ntk_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
static inline Ntk_Obj_t * Ntk_ManCi( Ntk_Man_t * p, int i ) { return Vec_PtrEntry( p->vCis, i ); }
static inline Ntk_Obj_t * Ntk_ManCo( Ntk_Man_t * p, int i ) { return Vec_PtrEntry( p->vCos, i ); }
static inline Ntk_Obj_t * Ntk_ManObj( Ntk_Man_t * p, int i ) { return Vec_PtrEntry( p->vObjs, i ); }
static inline int Ntk_ObjFaninNum( Ntk_Obj_t * p ) { return p->nFanins; }
static inline int Ntk_ObjFanoutNum( Ntk_Obj_t * p ) { return p->nFanouts; }
......@@ -126,8 +133,8 @@ static inline int Ntk_ObjIsCo( Ntk_Obj_t * p ) { return p->Ty
static inline int Ntk_ObjIsNode( Ntk_Obj_t * p ) { return p->Type == NTK_OBJ_NODE; }
static inline int Ntk_ObjIsLatch( Ntk_Obj_t * p ) { return p->Type == NTK_OBJ_LATCH; }
static inline int Ntk_ObjIsBox( Ntk_Obj_t * p ) { return p->Type == NTK_OBJ_BOX; }
static inline int Ntk_ObjIsPi( Ntk_Obj_t * p ) { return Ntk_ObjFaninNum(p) == 0 || (Ntk_ObjFaninNum(p) == 1 && Ntk_ObjIsLatch(Ntk_ObjFanin0(p))); }
static inline int Ntk_ObjIsPo( Ntk_Obj_t * p ) { return Ntk_ObjFanoutNum(p)== 0 || (Ntk_ObjFanoutNum(p)== 1 && Ntk_ObjIsLatch(Ntk_ObjFanout0(p))); }
static inline int Ntk_ObjIsPi( Ntk_Obj_t * p ) { return Ntk_ObjIsCi(p) && Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1; }
static inline int Ntk_ObjIsPo( Ntk_Obj_t * p ) { return Ntk_ObjIsCo(p) && Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1; }
static inline float Ntk_ObjArrival( Ntk_Obj_t * pObj ) { return pObj->tArrival; }
static inline float Ntk_ObjRequired( Ntk_Obj_t * pObj ) { return pObj->tRequired; }
......@@ -181,42 +188,41 @@ static inline int Ntk_ObjIsTravIdPrevious( Ntk_Obj_t * pObj ) { r
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== ntlDfs.c ==========================================================*/
/*=== ntkDfs.c ==========================================================*/
extern int Ntk_ManLevel( Ntk_Man_t * pNtk );
extern int Ntk_ManLevel2( Ntk_Man_t * pNtk );
extern Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk );
extern Vec_Ptr_t * Ntk_ManDfsReverse( Ntk_Man_t * pNtk );
/*=== ntlFanio.c ==========================================================*/
/*=== ntkFanio.c ==========================================================*/
extern void Ntk_ObjCollectFanins( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes );
extern void Ntk_ObjCollectFanouts( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes );
extern void Ntk_ObjAddFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin );
extern void Ntk_ObjDeleteFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin );
extern void Ntk_ObjPatchFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFaninOld, Ntk_Obj_t * pFaninNew );
extern void Ntk_ObjReplace( Ntk_Obj_t * pNodeOld, Ntk_Obj_t * pNodeNew );
/*=== ntlMan.c ============================================================*/
/*=== ntkMan.c ============================================================*/
extern Ntk_Man_t * Ntk_ManAlloc();
extern void Ntk_ManFree( Ntk_Man_t * p );
extern void Ntk_ManPrintStats( Ntk_Man_t * p );
/*=== ntlMap.c ============================================================*/
extern Ntk_Man_t * Ntk_MappingIf( Aig_Man_t * p, void * pPars );
/*=== ntlObj.c ============================================================*/
extern Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * pMan );
extern Ntk_Obj_t * Ntk_ManCreatePo( Ntk_Man_t * pMan );
extern void Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib );
/*=== ntkMap.c ============================================================*/
/*=== ntkObj.c ============================================================*/
extern Ntk_Obj_t * Ntk_ManCreateCi( Ntk_Man_t * pMan, int nFanouts );
extern Ntk_Obj_t * Ntk_ManCreateCo( Ntk_Man_t * pMan );
extern Ntk_Obj_t * Ntk_ManCreateNode( Ntk_Man_t * pMan, int nFanins, int nFanouts );
extern Ntk_Obj_t * Ntk_ManCreateBox( Ntk_Man_t * pMan, int nFanins, int nFanouts );
extern Ntk_Obj_t * Ntk_ManCreateLatch( Ntk_Man_t * pMan );
extern void Ntk_ManDeleteNode( Ntk_Obj_t * pObj );
extern void Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj );
/*=== ntlUtil.c ============================================================*/
/*=== ntkTiming.c ============================================================*/
extern float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib );
extern void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib );
/*=== ntkUtil.c ============================================================*/
extern void Ntk_ManIncrementTravId( Ntk_Man_t * pNtk );
extern int Ntk_ManGetFaninMax( Ntk_Man_t * pNtk );
extern int Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk );
extern int Ntk_ManLevel( Ntk_Man_t * pNtk );
extern int Ntk_ManPiNum( Ntk_Man_t * pNtk );
extern int Ntk_ManPoNum( Ntk_Man_t * pNtk );
/*=== ntlReadBlif.c ==========================================================*/
extern Ntk_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
/*=== ntlWriteBlif.c ==========================================================*/
extern void Ioa_WriteBlif( Ntk_Man_t * p, char * pFileName );
extern int Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk );
#ifdef __cplusplus
}
......
src/aig/ntk/ntkBidec.c 0 → 100644
/**CFile****************************************************************
FileName [ntkBidec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Bi-decomposition of local functions.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntkBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntk.h"
#include "bdc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Resynthesizes nodes using bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hop_Obj_t * Ntk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare )
{
unsigned * pTruth;
Bdc_Fun_t * pFunc;
int nNodes, i;
assert( nVars <= 16 );
// derive truth table
pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
if ( Hop_IsComplement(pRoot) )
for ( i = Aig_TruthWordNum(nVars)-1; i >= 0; i-- )
pTruth[i] = ~pTruth[i];
// decompose truth table
Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
// convert back into HOP
Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) );
for ( i = 0; i < nVars; i++ )
Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) );
nNodes = Bdc_ManNodeNum(p);
for ( i = nVars + 1; i < nNodes; i++ )
{
pFunc = Bdc_ManFunc( p, i );
Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
}
return Bdc_FunCopyHop( Bdc_ManRoot(p) );
}
/**Function*************************************************************
Synopsis [Resynthesizes nodes using bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntk_ManBidecResyn( Ntk_Man_t * pNtk, int fVerbose )
{
Bdc_Par_t Pars = {0}, * pPars = &Pars;
Bdc_Man_t * p;
Ntk_Obj_t * pObj;
Vec_Int_t * vTruth;
int i, nGainTotal = 0, nNodes1, nNodes2;
int clk = clock();
pPars->nVarsMax = Ntk_ManGetFaninMax( pNtk );
pPars->fVerbose = fVerbose;
if ( pPars->nVarsMax > 15 )
{
if ( fVerbose )
printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" );
pPars->nVarsMax = 15;
}
vTruth = Vec_IntAlloc( 0 );
p = Bdc_ManAlloc( pPars );
Ntk_ManForEachNode( pNtk, pObj, i )
{
if ( Ntk_ObjFaninNum(pObj) > 15 )
continue;
nNodes1 = Hop_DagSize(pObj->pFunc);
pObj->pFunc = Ntk_NodeIfNodeResyn( p, pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, NULL );
nNodes2 = Hop_DagSize(pObj->pFunc);
nGainTotal += nNodes1 - nNodes2;
}
Bdc_ManFree( p );
Vec_IntFree( vTruth );
if ( fVerbose )
{
printf( "Total gain in AIG nodes = %d. ", nGainTotal );
PRT( "Total runtime", clock() - clk );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntk/ntkCheck.c 0 → 100644
/**CFile****************************************************************
FileName [ntk_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: ntk_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ntk.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/ntk/ntkDfs.c
......@@ -30,6 +30,62 @@
/**Function*************************************************************
Synopsis [Computes the number of logic levels not counting PIs/POs.]
Description [Assumes that white boxes have unit level.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ntk_ManLevel( Ntk_Man_t * pNtk )
{
Tim_Man_t * pManTimeUnit;
Ntk_Obj_t * pObj, * pFanin;
int i, k, LevelMax, Level;
// clean the levels
Ntk_ManForEachObj( pNtk, pObj, i )
Ntk_ObjSetLevel( pObj, 0 );
// perform level computation
LevelMax = 0;
pManTimeUnit = Tim_ManDupUnit( pNtk->pManTime );
Tim_ManIncrementTravId( pManTimeUnit );
Ntk_ManForEachObj( pNtk, pObj, i )
{
if ( Ntk_ObjIsCi(pObj) )
{
Level = (int)Tim_ManGetPiArrival( pManTimeUnit, pObj->PioId );
Ntk_ObjSetLevel( pObj, Level );
}
else if ( Ntk_ObjIsCo(pObj) )
{
Level = Ntk_ObjLevel( Ntk_ObjFanin0(pObj) );
Tim_ManSetPoArrival( pManTimeUnit, pObj->PioId, (float)Level );
Ntk_ObjSetLevel( pObj, Level );
if ( LevelMax < Ntk_ObjLevel(pObj) )
LevelMax = Ntk_ObjLevel(pObj);
}
else if ( Ntk_ObjIsNode(pObj) )
{
Level = 0;
Ntk_ObjForEachFanin( pObj, pFanin, k )
if ( Level < Ntk_ObjLevel(pFanin) )
Level = Ntk_ObjLevel(pFanin);
Ntk_ObjSetLevel( pObj, Level + 1 );
}
else
assert( 0 );
}
// set the old timing manager
Tim_ManStop( pManTimeUnit );
return LevelMax;
}
/**Function*************************************************************
Synopsis [Performs DFS for one node.]
Description []
......@@ -39,16 +95,96 @@
SeeAlso []
***********************************************************************/
void Ntk_ManDfs_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
void Ntk_ManLevel2_rec( Ntk_Obj_t * pObj )
{
Ntk_Obj_t * pNext;
int i, iBox, iTerm1, nTerms, LevelMax = 0;
if ( Ntk_ObjIsTravIdCurrent( pObj ) )
return;
Ntk_ObjSetTravIdCurrent( pObj );
if ( Ntk_ObjIsCi(pObj) )
{
iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId );
if ( iBox >= 0 ) // this is not a true PI
{
iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox );
nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox );
for ( i = 0; i < nTerms; i++ )
{
pNext = Ntk_ManCo(pObj->pMan, iTerm1 + i);
Ntk_ManLevel2_rec( pNext );
if ( LevelMax < Ntk_ObjLevel(pNext) )
LevelMax = Ntk_ObjLevel(pNext);
}
LevelMax++;
}
}
else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCo(pObj) )
{
Ntk_ObjForEachFanin( pObj, pNext, i )
{
Ntk_ManLevel2_rec( pNext );
if ( LevelMax < Ntk_ObjLevel(pNext) )
LevelMax = Ntk_ObjLevel(pNext);
}
if ( Ntk_ObjIsNode(pObj) )
LevelMax++;
}
else
assert( 0 );
Ntk_ObjSetLevel( pObj, LevelMax );
}
/**Function*************************************************************
Synopsis [Returns the DFS ordered array of all objects except latches.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntk_ManLevel2( Ntk_Man_t * pNtk )
{
Ntk_Obj_t * pObj;
int i, LevelMax = 0;
Ntk_ManForEachObj( pNtk, pObj, i )
Ntk_ObjSetLevel( pObj, 0 );
Ntk_ManIncrementTravId( pNtk );
Ntk_ManForEachPo( pNtk, pObj, i )
{
Ntk_ManLevel2_rec( pObj );
if ( LevelMax < Ntk_ObjLevel(pObj) )
LevelMax = Ntk_ObjLevel(pObj);
}
return LevelMax;
}
/**Function*************************************************************
Synopsis [Performs DFS for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ntk_ManDfs_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
Ntk_Obj_t * pNext;
int i;
if ( Ntk_ObjIsTravIdCurrent( pNode ) )
if ( Ntk_ObjIsTravIdCurrent( pObj ) )
return;
Ntk_ObjSetTravIdCurrent( pNode );
Ntk_ObjForEachFanin( pNode, pNext, i )
Ntk_ObjSetTravIdCurrent( pObj );
Ntk_ObjForEachFanin( pObj, pNext, i )
Ntk_ManDfs_rec( pNext, vNodes );
Vec_PtrPush( vNodes, pNode );
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
......@@ -69,8 +205,16 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
int i;
Ntk_ManIncrementTravId( pNtk );
vNodes = Vec_PtrAlloc( 100 );
Ntk_ManForEachPo( pNtk, pObj, i )
Ntk_ManDfs_rec( pObj, vNodes );
Ntk_ManForEachObj( pNtk, pObj, i )
{
if ( Ntk_ObjIsCi(pObj) )
{
Ntk_ObjSetTravIdCurrent( pObj );
Vec_PtrPush( vNodes, pObj );
}
else if ( Ntk_ObjIsCo(pObj) )
Ntk_ManDfs_rec( pObj, vNodes );
}
return vNodes;
}
......@@ -85,16 +229,35 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
SeeAlso []
***********************************************************************/
void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
Ntk_Obj_t * pNext;
int i;
if ( Ntk_ObjIsTravIdCurrent( pNode ) )
int i, iBox, iTerm1, nTerms;
if ( Ntk_ObjIsTravIdCurrent( pObj ) )
return;
Ntk_ObjSetTravIdCurrent( pNode );
Ntk_ObjForEachFanout( pNode, pNext, i )
Ntk_ManDfsReverse_rec( pNext, vNodes );
Vec_PtrPush( vNodes, pNode );
Ntk_ObjSetTravIdCurrent( pObj );
if ( Ntk_ObjIsCo(pObj) )
{
iBox = Tim_ManBoxForCo( pObj->pMan->pManTime, pObj->PioId );
if ( iBox >= 0 ) // this is not a true PO
{
iTerm1 = Tim_ManBoxOutputFirst( pObj->pMan->pManTime, iBox );
nTerms = Tim_ManBoxOutputNum( pObj->pMan->pManTime, iBox );
for ( i = 0; i < nTerms; i++ )
{
pNext = Ntk_ManCi(pObj->pMan, iTerm1 + i);
Ntk_ManDfsReverse_rec( pNext, vNodes );
}
}
}
else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCi(pObj) )
{
Ntk_ObjForEachFanout( pObj, pNext, i )
Ntk_ManDfsReverse_rec( pNext, vNodes );
}
else
assert( 0 );
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
......
src/aig/ntk/ntkFanio.c
......@@ -279,7 +279,7 @@ void Ntk_ObjTransferFanout( Ntk_Obj_t * pNodeFrom, Ntk_Obj_t * pNodeTo )
Vec_Ptr_t * vFanouts = pNodeFrom->pMan->vTemp;
Ntk_Obj_t * pTemp;
int nFanoutsOld, i;
assert( !Ntk_ObjIsPo(pNodeFrom) && !Ntk_ObjIsPo(pNodeTo) );
assert( !Ntk_ObjIsCo(pNodeFrom) && !Ntk_ObjIsCo(pNodeTo) );
assert( pNodeFrom->pMan == pNodeTo->pMan );
assert( pNodeFrom != pNodeTo );
assert( Ntk_ObjFanoutNum(pNodeFrom) > 0 );
......
src/aig/ntk/ntkMan.c
......@@ -50,6 +50,7 @@ Ntk_Man_t * Ntk_ManAlloc()
p->vTemp = Vec_PtrAlloc( 1000 );
p->nFanioPlus = 4;
p->pMemObjs = Aig_MmFlexStart();
p->pManHop = Hop_ManStart();
return p;
}
......@@ -72,9 +73,9 @@ void Ntk_ManFree( Ntk_Man_t * p )
if ( p->vCos ) Vec_PtrFree( p->vCos );
if ( p->vObjs ) Vec_PtrFree( p->vObjs );
if ( p->vTemp ) Vec_PtrFree( p->vTemp );
if ( p->pAig ) Aig_ManStop( p->pAig );
if ( p->pManTime ) Tim_ManStop( p->pManTime );
if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
if ( p->pManHop ) Hop_ManStop( p->pManHop );
free( p );
}
......@@ -89,7 +90,7 @@ void Ntk_ManFree( Ntk_Man_t * p )
SeeAlso []
***********************************************************************/
void Ntk_ManPrintStats( Ntk_Man_t * p )
void Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib )
{
printf( "%-15s : ", p->pName );
printf( "pi = %5d ", Ntk_ManPiNum(p) );
......@@ -97,10 +98,15 @@ void Ntk_ManPrintStats( Ntk_Man_t * p )
printf( "ci = %5d ", Ntk_ManCiNum(p) );
printf( "co = %5d ", Ntk_ManCoNum(p) );
printf( "lat = %5d ", Ntk_ManLatchNum(p) );
printf( "box = %5d ", Ntk_ManBoxNum(p) );
// printf( "box = %5d ", Ntk_ManBoxNum(p) );
printf( "node = %5d ", Ntk_ManNodeNum(p) );
printf( "aig = %6d ", Aig_ManNodeNum(p->pAig) );
printf( "aig = %6d ", Ntk_ManGetAigNodeNum(p) );
printf( "lev = %3d ", Ntk_ManLevel(p) );
printf( "lev2 = %3d ", Ntk_ManLevel2(p) );
printf( "delay = %5.2f", Ntk_ManDelayTraceLut(p, pLutLib) );
printf( "\n" );
Ntk_ManDelayTracePrint( p, pLutLib );
}
////////////////////////////////////////////////////////////////////////
......
src/aig/ntk/ntkObj.c
......@@ -63,10 +63,11 @@ Ntk_Obj_t * Ntk_ManCreateObj( Ntk_Man_t * p, int nFanins, int nFanouts )
SeeAlso []
***********************************************************************/
Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
Ntk_Obj_t * Ntk_ManCreateCi( Ntk_Man_t * p, int nFanouts )
{
Ntk_Obj_t * pObj;
pObj = Ntk_ManCreateObj( p, 1, 1 );
pObj = Ntk_ManCreateObj( p, 1, nFanouts );
pObj->PioId = Vec_PtrSize( p->vCis );
Vec_PtrPush( p->vCis, pObj );
pObj->Type = NTK_OBJ_CI;
p->nObjs[NTK_OBJ_CI]++;
......@@ -84,10 +85,11 @@ Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
SeeAlso []
***********************************************************************/
Ntk_Obj_t * Ntk_ManCreatePo( Ntk_Man_t * p )
Ntk_Obj_t * Ntk_ManCreateCo( Ntk_Man_t * p )
{
Ntk_Obj_t * pObj;
pObj = Ntk_ManCreateObj( p, 1, 1 );
pObj->PioId = Vec_PtrSize( p->vCos );
Vec_PtrPush( p->vCos, pObj );
pObj->Type = NTK_OBJ_CO;
p->nObjs[NTK_OBJ_CO]++;
......@@ -200,7 +202,7 @@ void Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj )
{
Vec_Ptr_t * vNodes;
int i;
assert( !Ntk_ObjIsPi(pObj) );
assert( !Ntk_ObjIsCi(pObj) );
assert( Ntk_ObjFanoutNum(pObj) == 0 );
vNodes = Vec_PtrAlloc( 100 );
Ntk_ObjCollectFanins( pObj, vNodes );
......
src/aig/ntk/ntkUtil.c
......@@ -95,36 +95,25 @@ int Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk )
return nFanins;
}
/**Function*************************************************************
Synopsis [Computes the number of logic levels not counting PIs/POs.]
Synopsis []
Description [Assumes topological ordering of the nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntk_ManLevel( Ntk_Man_t * pNtk )
int Ntk_ManPiNum( Ntk_Man_t * pNtk )
{
Ntk_Obj_t * pObj, * pFanin;
int i, k, LevelMax;
Ntk_ManForEachPi( pNtk, pObj, i )
Ntk_ObjSetLevel( pObj, 0 );
Ntk_ManForEachNode( pNtk, pObj, i )
{
LevelMax = 0;
Ntk_ObjForEachFanin( pObj, pFanin, k )
if ( LevelMax < Ntk_ObjLevel(pFanin) )
LevelMax = Ntk_ObjLevel(pFanin);
Ntk_ObjSetLevel( pFanin, LevelMax+1 );
}
LevelMax = 0;
Ntk_ManForEachPo( pNtk, pObj, i )
if ( LevelMax < Ntk_ObjLevel(pObj) )
LevelMax = Ntk_ObjLevel(pObj);
return LevelMax;
Ntk_Obj_t * pNode;
int i, Counter = 0;
Ntk_ManForEachCi( pNtk, pNode, i )
Counter += Ntk_ObjIsPi( pNode );
return Counter;
}
/**Function*************************************************************
......@@ -138,18 +127,18 @@ int Ntk_ManLevel( Ntk_Man_t * pNtk )
SeeAlso []
***********************************************************************/
int Ntk_ManPiNum( Ntk_Man_t * pNtk )
int Ntk_ManPoNum( Ntk_Man_t * pNtk )
{
Ntk_Obj_t * pNode;
int i, Counter = 0;
Ntk_ManForEachPi( pNtk, pNode, i )
Counter++;
Ntk_ManForEachCo( pNtk, pNode, i )
Counter += Ntk_ObjIsPo( pNode );
return Counter;
}
/**Function*************************************************************
Synopsis []
Synopsis [Reads the number of BDD nodes.]
Description []
......@@ -158,13 +147,22 @@ int Ntk_ManPiNum( Ntk_Man_t * pNtk )
SeeAlso []
***********************************************************************/
int Ntk_ManPoNum( Ntk_Man_t * pNtk )
int Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk )
{
Ntk_Obj_t * pNode;
int i, Counter = 0;
Ntk_ManForEachPo( pNtk, pNode, i )
Counter++;
return Counter;
int i, nNodes = 0;
Ntk_ManForEachNode( pNtk, pNode, i )
{
if ( pNode->pFunc == NULL )
{
printf( "Ntk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id );
continue;
}
if ( Ntk_ObjFaninNum(pNode) < 2 )
continue;
nNodes += Hop_DagSize( pNode->pFunc );
}
return nNodes;
}
////////////////////////////////////////////////////////////////////////
......
src/aig/ntl/ntl.h
......@@ -31,6 +31,7 @@ extern "C" {
#include "aig.h"
#include "tim.h"
#include "ntk.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
......@@ -227,6 +228,7 @@ extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p );
extern char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
/*=== ntlInsert.c ==========================================================*/
extern int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
extern int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk );
/*=== ntlCheck.c ==========================================================*/
extern int Ntl_ManCheck( Ntl_Man_t * pMan );
extern int Ntl_ModelCheck( Ntl_Mod_t * pModel );
......@@ -236,6 +238,7 @@ extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName );
extern void Ntl_ManFree( Ntl_Man_t * p );
extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
extern void Ntl_ManPrintStats( Ntl_Man_t * p );
extern Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p );
extern Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
extern void Ntl_ModelFree( Ntl_Mod_t * p );
/*=== ntlMap.c ============================================================*/
......
src/aig/ntl/ntlExtract.c
......@@ -438,6 +438,8 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
// start the AIG manager
assert( p->pAig == NULL );
p->pAig = Aig_ManStart( 10000 );
p->pAig->pName = Aig_UtilStrsav( p->pName );
p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
// get the root model
pRoot = Vec_PtrEntry( p->vModels, 0 );
// collect primary inputs
......
src/aig/ntl/ntlInsert.c
......@@ -123,6 +123,105 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
return 1;
}
/**Function*************************************************************
Synopsis [Inserts the given mapping into the netlist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk )
{
char Buffer[100];
Vec_Int_t * vTruth;
Vec_Int_t * vCover;
Ntl_Mod_t * pRoot;
Ntl_Obj_t * pNode;
Ntl_Net_t * pNet, * pNetCo;
Ntk_Obj_t * pObj, * pFanin;
int i, k, nDigits;
unsigned * pTruth;
assert( Vec_PtrSize(p->vCis) == Ntk_ManCiNum(pNtk) );
assert( Vec_PtrSize(p->vCos) == Ntk_ManCoNum(pNtk) );
// set the correspondence between the PI/PO nodes
Ntl_ManForEachCiNet( p, pNet, i )
Ntk_ManCi( pNtk, i )->pCopy = pNet;
// Ntl_ManForEachCoNet( p, pNet, i )
// Ntk_ManCo( pNtk, i )->pCopy = pNet;
// remove old nodes
pRoot = Vec_PtrEntry( p->vModels, 0 );
Ntl_ModelForEachNode( pRoot, pNode, i )
Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
// create a new node for each LUT
vTruth = Vec_IntAlloc( 1 << 16 );
vCover = Vec_IntAlloc( 1 << 16 );
nDigits = Aig_Base10Log( Ntk_ManNodeNum(pNtk) );
Ntk_ManForEachNode( pNtk, pObj, i )
{
pNode = Ntl_ModelCreateNode( pRoot, Ntk_ObjFaninNum(pObj) );
pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, 0 );
pNode->pSop = Ntl_SopFromTruth( p, pTruth, Ntk_ObjFaninNum(pObj), vCover );
if ( !Kit_TruthIsConst0(pTruth, Ntk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Ntk_ObjFaninNum(pObj)) )
{
Ntk_ObjForEachFanin( pObj, pFanin, k )
{
pNet = pFanin->pCopy;
if ( pNet == NULL )
{
printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
return 0;
}
Ntl_ObjSetFanin( pNode, pNet, k );
}
}
sprintf( Buffer, "lut%0*d", nDigits, i );
if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
{
printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
return 0;
}
pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
{
printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
return 0;
}
pObj->pCopy = pNet;
}
Vec_IntFree( vCover );
Vec_IntFree( vTruth );
// mark CIs and outputs of the registers
Ntl_ManForEachCiNet( p, pNetCo, i )
pNetCo->nVisits = 101;
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
if ( pNetCo->nVisits == 101 )
continue;
pNetCo->nVisits = 101;
// get the corresponding PO and its driver
pObj = Ntk_ManCo( pNtk, i );
pFanin = Ntk_ObjFanin0( pObj );
// get the net driving the driver
pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
pNode = Ntl_ModelCreateNode( pRoot, 1 );
pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pFunc)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
pNetCo->pDriver = NULL;
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
return 0;
}
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/aig/ntl/ntlMan.c
......@@ -139,6 +139,22 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
/**Function*************************************************************
Synopsis [Deallocates the netlist manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p )
{
return p->pManTime;
}
/**Function*************************************************************
Synopsis [Allocates the model.]
Description []
......
src/aig/ntl/ntlMap.c
......@@ -117,7 +117,7 @@ Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
SeeAlso []
***********************************************************************/
void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
void Ntl_ManSetIfParsDefault( If_Par_t * pPars )
{
// extern void * Abc_FrameReadLibLut();
// set defaults
......@@ -162,57 +162,6 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
*/
}
/**Function*************************************************************
Synopsis [Load the network into FPGA manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
{
If_Man_t * pIfMan;
Aig_Obj_t * pNode;//, * pFanin, * pPrev;
Vec_Ptr_t * vNodes;
int i;
// start the mapping manager and set its parameters
pIfMan = If_ManStart( pPars );
// print warning about excessive memory usage
if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n",
1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
// load the AIG into the mapper
vNodes = Aig_ManDfsPio( p );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Aig_ObjIsAnd(pNode) )
pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan,
If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ),
If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
else if ( Aig_ObjIsPi(pNode) )
pNode->pData = If_ManCreateCi( pIfMan );
else if ( Aig_ObjIsPo(pNode) )
If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
else if ( Aig_ObjIsConst1(pNode) )
Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
else // add the node to the mapper
assert( 0 );
// set up the choice node
// if ( Aig_AigNodeIsChoice( pNode ) )
// {
// pIfMan->nChoices++;
// for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
// If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
// If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
// }
}
Vec_PtrFree( vNodes );
return pIfMan;
}
/**Function*************************************************************
......@@ -225,7 +174,7 @@ If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
SeeAlso []
***********************************************************************/
If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
If_Man_t * Ntl_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
{
If_Man_t * pIfMan;
Aig_Obj_t * pNode;//, * pFanin, * pPrev;
......@@ -251,7 +200,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
pIfMan->nLevelMax = (int)pNode->Level;
}
else if ( Aig_ObjIsPo(pNode) )
If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
else if ( Aig_ObjIsConst1(pNode) )
Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
else // add the node to the mapper
......@@ -264,6 +213,11 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
// If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
// If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
// }
{
If_Obj_t * pIfObj = pNode->pData;
assert( !If_IsComplement(pIfObj) );
assert( pIfObj->Id == pNode->Id );
}
}
return pIfMan;
}
......@@ -279,7 +233,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
Vec_Ptr_t * Ntl_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
{
Vec_Ptr_t * vIfMap;
If_Obj_t * pNode, * pLeaf;
......@@ -356,12 +310,12 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
If_Par_t Pars, * pPars = &Pars;
If_Man_t * pIfMan;
// perform FPGA mapping
Ntk_ManSetIfParsDefault( pPars );
Ntl_ManSetIfParsDefault( pPars );
// set the arrival times
pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
// translate into the mapper
pIfMan = Ntk_ManToIf( p, pPars );
pIfMan = Ntl_ManToIf( p, pPars );
if ( pIfMan == NULL )
return NULL;
pIfMan->pManTim = Tim_ManDup( pMan->pManTime, 0 );
......@@ -371,7 +325,7 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
return NULL;
}
// transform the result of mapping into the new network
vMapping = Ntk_ManFromIf( p, pIfMan );
vMapping = Ntl_ManFromIf( p, pIfMan );
If_ManStop( pIfMan );
if ( vMapping == NULL )
return NULL;
......
src/aig/tim/tim.c
......@@ -150,7 +150,8 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
Synopsis [Duplicates the timing manager.]
Description []
Description [Derives discrete-delay-model timing manager.
Useful for AIG optimization with approximate timing information.]
SideEffects []
......@@ -171,16 +172,21 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
for ( k = 0; k < p->nPos; k++ )
pNew->pPos[k].TravId = 0;
if ( fDiscrete )
{
for ( k = 0; k < p->nPis; k++ )
pNew->pPis[k].timeArr = 0.0; // modify here
// modify the required times
}
pNew->vDelayTables = Vec_PtrAlloc( 100 );
Tim_ManForEachBox( p, pBox, i )
{
pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs );
Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
if ( fDiscrete )
{
for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
pDelayTableNew[k] = 1.0; // modify here
}
else
memcpy( pDelayTableNew, pBox->pDelayTable, sizeof(float) * pBox->nInputs * pBox->nOutputs );
Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs,
......@@ -191,6 +197,47 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
/**Function*************************************************************
Synopsis [Duplicates the timing manager.]
Description [Derives unit-delay-model timing manager.
Useful for levelizing the network.]
SideEffects []
SeeAlso []
***********************************************************************/
Tim_Man_t * Tim_ManDupUnit( Tim_Man_t * p )
{
Tim_Man_t * pNew;
Tim_Box_t * pBox;
float * pDelayTableNew;
int i, k;
pNew = Tim_ManStart( p->nPis, p->nPos );
memcpy( pNew->pPis, p->pPis, sizeof(Tim_Obj_t) * p->nPis );
memcpy( pNew->pPos, p->pPos, sizeof(Tim_Obj_t) * p->nPos );
for ( k = 0; k < p->nPis; k++ )
{
pNew->pPis[k].TravId = 0;
pNew->pPis[k].timeArr = 0.0;
}
for ( k = 0; k < p->nPos; k++ )
pNew->pPos[k].TravId = 0;
pNew->vDelayTables = Vec_PtrAlloc( 100 );
Tim_ManForEachBox( p, pBox, i )
{
pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs );
Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
pDelayTableNew[k] = 1.0;
Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs,
pBox->Inouts[pBox->nInputs], pBox->nOutputs, pDelayTableNew );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Stops the timing manager.]
Description []
......@@ -567,6 +614,110 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
return pObjThis->timeReq;
}
/**Function*************************************************************
Synopsis [Returns the box number for the given input.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Tim_ManBoxForCi( Tim_Man_t * p, int iCi )
{
if ( iCi >= p->nPis )
return -1;
return p->pPis[iCi].iObj2Box;
}
/**Function*************************************************************
Synopsis [Returns the box number for the given output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Tim_ManBoxForCo( Tim_Man_t * p, int iCo )
{
if ( iCo >= p->nPos )
return -1;
return p->pPos[iCo].iObj2Box;
}
/**Function*************************************************************
Synopsis [Returns the first input of the box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox )
{
Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
return pBox->Inouts[0];
}
/**Function*************************************************************
Synopsis [Returns the first input of the box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox )
{
Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
return pBox->Inouts[pBox->nInputs];
}
/**Function*************************************************************
Synopsis [Returns the first input of the box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Tim_ManBoxInputNum( Tim_Man_t * p, int iBox )
{
Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
return pBox->nInputs;
}
/**Function*************************************************************
Synopsis [Returns the first input of the box.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox )
{
Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
return pBox->nOutputs;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/aig/tim/tim.h
......@@ -59,6 +59,7 @@ typedef struct Tim_Man_t_ Tim_Man_t;
/*=== time.c ===========================================================*/
extern Tim_Man_t * Tim_ManStart( int nPis, int nPos );
extern Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete );
extern Tim_Man_t * Tim_ManDupUnit( Tim_Man_t * p );
extern void Tim_ManStop( Tim_Man_t * p );
extern void Tim_ManPrint( Tim_Man_t * p );
extern void Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
......@@ -73,6 +74,12 @@ extern void Tim_ManSetPoRequired( Tim_Man_t * p, int iPo, float Delay
extern void Tim_ManSetPoRequiredAll( Tim_Man_t * p, float Delay );
extern float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi );
extern float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo );
extern int Tim_ManBoxForCi( Tim_Man_t * p, int iCo );
extern int Tim_ManBoxForCo( Tim_Man_t * p, int iCi );
extern int Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox );
extern int Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox );
extern int Tim_ManBoxInputNum( Tim_Man_t * p, int iBox );
extern int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox );
#ifdef __cplusplus
}
......
src/base/abc/abc.h
......@@ -582,6 +582,7 @@ extern Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
extern Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk );
extern int Abc_NtkLevel( Abc_Ntk_t * pNtk );
extern int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
extern bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
......@@ -612,7 +613,6 @@ extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
extern unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk );
......
src/base/abc/abcDfs.c
......@@ -978,6 +978,32 @@ int Abc_NtkLevelReverse_rec( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
Vec_Vec_t * vLevels;
int nLevels, i;
nLevels = Abc_NtkLevel( pNtk );
vLevels = Vec_VecStart( nLevels + 1 );
Abc_NtkForEachNode( pNtk, pObj, i )
{
assert( (int)pObj->Level <= nLevels );
Vec_VecPush( vLevels, pObj->Level, pObj );
}
return vLevels;
}
/**Function*************************************************************
Synopsis [Computes the number of logic levels not counting PIs/POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkLevel( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
......
src/base/abc/abcFunc.c
......@@ -785,159 +785,6 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
/**Function*************************************************************
Synopsis [Construct BDDs and mark AIG nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ConvertAigToTruth_rec1( Hop_Obj_t * pObj )
{
int Counter = 0;
assert( !Hop_IsComplement(pObj) );
if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
return 0;
Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) );
Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
Hop_ObjSetMarkA( pObj );
return Counter + 1;
}
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
{
unsigned * pTruth, * pTruth0, * pTruth1;
int i;
assert( !Hop_IsComplement(pObj) );
if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
return pObj->pData;
// compute the truth tables of the fanins
pTruth0 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
pTruth1 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
// creat the truth table of the node
pTruth = Vec_IntFetch( vTruth, nWords );
if ( Hop_ObjIsExor(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] ^ pTruth1[i];
else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & pTruth1[i];
else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & ~pTruth1[i];
else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & pTruth1[i];
else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
assert( Hop_ObjIsMarkA(pObj) ); // loop detection
Hop_ObjClearMarkA( pObj );
pObj->pData = pTruth;
return pTruth;
}
/**Function*************************************************************
Synopsis [Computes truth table of the node.]
Description [Assumes that the structural support is no more than 8 inputs.
Uses array vTruth to store temporary truth tables. The returned pointer should
be used immediately.]
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
{
static unsigned uTruths[8][8] = { // elementary truth tables
{ 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
{ 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
{ 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
{ 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
{ 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 },
{ 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF },
{ 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF },
{ 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
};
Hop_Obj_t * pObj;
unsigned * pTruth, * pTruth2;
int i, nWords, nNodes;
Vec_Ptr_t * vTtElems;
// if the number of variables is more than 8, allocate truth tables
if ( nVars > 8 )
vTtElems = Vec_PtrAllocTruthTables( nVars );
else
vTtElems = NULL;
// clear the data fields and set marks
nNodes = Abc_ConvertAigToTruth_rec1( pRoot );
// prepare memory
nWords = Hop_TruthWordNum( nVars );
Vec_IntClear( vTruth );
Vec_IntGrow( vTruth, nWords * (nNodes+1) );
pTruth = Vec_IntFetch( vTruth, nWords );
// check the case of a constant
if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
{
assert( nNodes == 0 );
if ( Hop_IsComplement(pRoot) )
Extra_TruthClear( pTruth, nVars );
else
Extra_TruthFill( pTruth, nVars );
return pTruth;
}
// set elementary truth tables at the leaves
assert( nVars <= Hop_ManPiNum(p) );
// assert( Hop_ManPiNum(p) <= 8 );
if ( fMsbFirst )
{
Hop_ManForEachPi( p, pObj, i )
{
if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
else
pObj->pData = (void *)uTruths[nVars-1-i];
}
}
else
{
Hop_ManForEachPi( p, pObj, i )
{
if ( vTtElems )
pObj->pData = Vec_PtrEntry(vTtElems, i);
else
pObj->pData = (void *)uTruths[i];
}
}
// clear the marks and compute the truth table
pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
// copy the result
Extra_TruthCopy( pTruth, pTruth2, nVars );
if ( vTtElems )
Vec_PtrFree( vTtElems );
return pTruth;
}
/**Function*************************************************************
......
src/base/abci/abcBidec.c
......@@ -19,15 +19,13 @@
***********************************************************************/
#include "abc.h"
#include "bdc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); }
static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -48,24 +46,25 @@ Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pR
{
unsigned * pTruth;
Bdc_Fun_t * pFunc;
int i;
int nNodes, i;
assert( nVars <= 16 );
// derive truth table
pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
if ( Hop_IsComplement(pRoot) )
Extra_TruthNot( pTruth, pTruth, nVars );
// decompose truth table
Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
// convert back into HOP
Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) );
for ( i = 0; i < nVars; i++ )
Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
for ( i = nVars + 1; i < p->nNodes; i++ )
Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) );
nNodes = Bdc_ManNodeNum(p);
for ( i = nVars + 1; i < nNodes; i++ )
{
pFunc = Bdc_FunWithId( p, i );
pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
pFunc = Bdc_ManFunc( p, i );
Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
}
return Bdc_FunCopyHop(p->pRoot);
return Bdc_FunCopyHop( Bdc_ManRoot(p) );
}
/**Function*************************************************************
......
src/base/abci/abcDar.c
......@@ -769,7 +769,7 @@ clk = clock();
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
......@@ -777,7 +777,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
pMan = Abc_NtkToDar( pNtk, 0 );
if ( pMan == NULL )
return NULL;
pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
Aig_ManStop( pMan );
......@@ -1432,6 +1432,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
***********************************************************************/
void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
{
/*
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
......@@ -1442,6 +1443,7 @@ void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
pMan->vFlopNums = NULL;
Aig_ManHaigRecord( pMan );
Aig_ManStop( pMan );
*/
}
/**Function*************************************************************
......
src/base/abci/abcStrash.c
......@@ -383,7 +383,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco
extern int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
int nVars = Abc_NtkRecVarNum();
Vec_Int_t * vMemory = Abc_NtkRecMemory();
unsigned * pTruth = Abc_ConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 );
unsigned * pTruth = Hop_ManConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 );
assert( Extra_TruthSupportSize(pTruth, nVars) == Abc_ObjFaninNum(pNodeOld) ); // should be swept
if ( Hop_IsComplement(pRoot) )
Extra_TruthNot( pTruth, pTruth, nVars );
......
src/base/io/ioWriteBench.c
......@@ -258,7 +258,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
nFanins = Abc_ObjFaninNum(pNode);
assert( nFanins <= 8 );
// compute the truth table
pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
pTruth = Hop_ManConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
if ( Hop_IsComplement(pNode->pData) )
Extra_TruthNot( pTruth, pTruth, nFanins );
// consider simple cases
......
src/base/main/mainInt.h
......@@ -78,6 +78,7 @@ struct Abc_Frame_t_
void * pAbc8Ntl; // the current design
void * pAbc8Ntk; // the current mapped network
void * pAbc8Aig; // the current AIG
void * pAbc8Lib; // the current LUT library
};
////////////////////////////////////////////////////////////////////////
......
src/map/fpga/fpga.c
......@@ -146,7 +146,7 @@ int Fpga_CommandReadLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
fclose( pFile );
// set the new network
pLib = Fpga_LutLibCreate( FileName, fVerbose );
pLib = Fpga_LutLibRead( FileName, fVerbose );
if ( pLib == NULL )
{
fprintf( pErr, "Reading LUT library has failed.\n" );
......@@ -228,7 +228,7 @@ int Fpga_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
fprintf( pErr, "\nusage: read_print [-vh]\n");
fprintf( pErr, "\nusage: print_lut [-vh]\n");
fprintf( pErr, "\t print the current LUT library\n" );
fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", (fVerbose? "yes" : "no") );
fprintf( pErr, "\t-h : print the command usage\n");
......
src/map/fpga/fpgaInt.h
......@@ -314,7 +314,7 @@ extern void Fpga_NodeAddFaninFanout( Fpga_Node_t * pFanin, Fpga_Nod
extern void Fpga_NodeRemoveFaninFanout( Fpga_Node_t * pFanin, Fpga_Node_t * pFanoutToRemove );
extern int Fpga_NodeGetFanoutNum( Fpga_Node_t * pNode );
/*=== fpgaLib.c ============================================================*/
extern Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose );
extern Fpga_LutLib_t * Fpga_LutLibRead( char * FileName, int fVerbose );
extern void Fpga_LutLibFree( Fpga_LutLib_t * p );
extern void Fpga_LutLibPrint( Fpga_LutLib_t * pLutLib );
extern int Fpga_LutLibDelaysAreDiscrete( Fpga_LutLib_t * pLutLib );
......
src/map/fpga/fpgaLib.c
......@@ -52,7 +52,7 @@ float Fpga_LutLibReadLutArea( Fpga_LutLib_t * p, int Size ) { assert( S
SeeAlso []
***********************************************************************/
Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose )
Fpga_LutLib_t * Fpga_LutLibRead( char * FileName, int fVerbose )
{
char pBuffer[1000], * pToken;
Fpga_LutLib_t * p;
......
src/map/if/if.h
......@@ -245,8 +245,9 @@ static inline If_Obj_t * If_ManObj( If_Man_t * p, int i ) { r
static inline int If_ObjIsConst1( If_Obj_t * pObj ) { return pObj->Type == IF_CONST1; }
static inline int If_ObjIsCi( If_Obj_t * pObj ) { return pObj->Type == IF_CI; }
static inline int If_ObjIsCo( If_Obj_t * pObj ) { return pObj->Type == IF_CO; }
//static inline int If_ObjIsPi( If_Obj_t * pObj ) { return If_ObjIsCi(pObj) && pObj->pFanin0 == NULL; }
static inline int If_ObjIsLatch( If_Obj_t * pObj ) { return If_ObjIsCi(pObj) && pObj->pFanin0 != NULL; }
static inline int If_ObjIsTerm( If_Obj_t * pObj ) { return pObj->Type == IF_CI || pObj->Type == IF_CO; }
//static inline int If_ObjIsPi( If_Obj_t * pObj ) { return If_ObjIsCi(pObj) && pObj->pFanin0 == NULL; }
static inline int If_ObjIsLatch( If_Obj_t * pObj ) { return If_ObjIsCi(pObj) && pObj->pFanin0 != NULL; }
static inline int If_ObjIsAnd( If_Obj_t * pObj ) { return pObj->Type == IF_AND; }
static inline If_Obj_t * If_ObjFanin0( If_Obj_t * pObj ) { return pObj->pFanin0; }
......@@ -402,6 +403,8 @@ extern int If_ManCrossCut( If_Man_t * p );
extern Vec_Ptr_t * If_ManReverseOrder( If_Man_t * p );
extern void If_ManMarkMapping( If_Man_t * p );
extern Vec_Ptr_t * If_ManCollectMappingDirect( If_Man_t * p );
extern Vec_Int_t * If_ManCollectMappingInt( If_Man_t * p );
extern int If_ManCountSpecialPos( If_Man_t * p );
......
src/map/if/ifLib.c 0 → 100644
/**CFile****************************************************************
FileName [ifLib.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [FPGA mapping based on priority cuts.]
Synopsis [LUT library.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - November 21, 2006.]
Revision [$Id: ifLib.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
***********************************************************************/
#include "if.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline char * If_UtilStrsav( char *s ) { return !s ? s : strcpy(ALLOC(char, strlen(s)+1), s); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Reads the description of LUTs from the LUT library file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Lib_t * If_LutLibRead( char * FileName )
{
char pBuffer[1000], * pToken;
If_Lib_t * p;
FILE * pFile;
int i, k;
pFile = fopen( FileName, "r" );
if ( pFile == NULL )
{
printf( "Cannot open LUT library file \"%s\".\n", FileName );
return NULL;
}
p = ALLOC( If_Lib_t, 1 );
memset( p, 0, sizeof(If_Lib_t) );
p->pName = If_UtilStrsav( FileName );
i = 1;
while ( fgets( pBuffer, 1000, pFile ) != NULL )
{
pToken = strtok( pBuffer, " \t\n" );
if ( pToken == NULL )
continue;
if ( pToken[0] == '#' )
continue;
if ( i != atoi(pToken) )
{
printf( "Error in the LUT library file \"%s\".\n", FileName );
free( p );
return NULL;
}
// read area
pToken = strtok( NULL, " \t\n" );
p->pLutAreas[i] = (float)atof(pToken);
// read delays
k = 0;
while ( pToken = strtok( NULL, " \t\n" ) )
p->pLutDelays[i][k++] = (float)atof(pToken);
// check for out-of-bound
if ( k > i )
{
printf( "LUT %d has too many pins (%d). Max allowed is %d.\n", i, k, i );
return NULL;
}
// check if var delays are specifies
if ( k > 1 )
p->fVarPinDelays = 1;
if ( i == IF_MAX_LUTSIZE )
{
printf( "Skipping LUTs of size more than %d.\n", i );
return NULL;
}
i++;
}
p->LutMax = i-1;
// check the library
if ( p->fVarPinDelays )
{
for ( i = 1; i <= p->LutMax; i++ )
for ( k = 0; k < i; k++ )
{
if ( p->pLutDelays[i][k] <= 0.0 )
printf( "Warning: Pin %d of LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n",
k, i, p->pLutDelays[i][k] );
if ( k && p->pLutDelays[i][k-1] > p->pLutDelays[i][k] )
printf( "Warning: Pin %d of LUT %d has delay %f. Pin %d of LUT %d has delay %f. Pin delays should be in non-decreasing order. Technology mapping may not work correctly.\n",
k-1, i, p->pLutDelays[i][k-1],
k, i, p->pLutDelays[i][k] );
}
}
else
{
for ( i = 1; i <= p->LutMax; i++ )
{
if ( p->pLutDelays[i][0] <= 0.0 )
printf( "Warning: LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n",
k, i, p->pLutDelays[i][0] );
}
}
return p;
}
/**Function*************************************************************
Synopsis [Duplicates the LUT library.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Lib_t * If_LutLibDup( If_Lib_t * p )
{
If_Lib_t * pNew;
pNew = ALLOC( If_Lib_t, 1 );
*pNew = *p;
pNew->pName = If_UtilStrsav( pNew->pName );
return pNew;
}
/**Function*************************************************************
Synopsis [Frees the LUT library.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_LutLibFree( If_Lib_t * pLutLib )
{
if ( pLutLib == NULL )
return;
FREE( pLutLib->pName );
FREE( pLutLib );
}
/**Function*************************************************************
Synopsis [Prints the LUT library.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_LutLibPrint( If_Lib_t * pLutLib )
{
int i, k;
printf( "# The area/delay of k-variable LUTs:\n" );
printf( "# k area delay\n" );
if ( pLutLib->fVarPinDelays )
{
for ( i = 1; i <= pLutLib->LutMax; i++ )
{
printf( "%d %7.2f ", i, pLutLib->pLutAreas[i] );
for ( k = 0; k < i; k++ )
printf( " %7.2f", pLutLib->pLutDelays[i][k] );
printf( "\n" );
}
}
else
for ( i = 1; i <= pLutLib->LutMax; i++ )
printf( "%d %7.2f %7.2f\n", i, pLutLib->pLutAreas[i], pLutLib->pLutDelays[i][0] );
}
/**Function*************************************************************
Synopsis [Returns 1 if the delays are discrete.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_LutLibDelaysAreDiscrete( If_Lib_t * pLutLib )
{
float Delay;
int i;
for ( i = 1; i <= pLutLib->LutMax; i++ )
{
Delay = pLutLib->pLutDelays[i][0];
if ( ((float)((int)Delay)) != Delay )
return 0;
}
return 1;
}
/**Function*************************************************************
Synopsis [Sets simple LUT library.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
If_Lib_t * If_SetSimpleLutLib( int nLutSize )
{
If_Lib_t s_LutLib10= { "lutlib",10, 0, {0,1,1,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1},{1},{1}} };
If_Lib_t s_LutLib9 = { "lutlib", 9, 0, {0,1,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1},{1}} };
If_Lib_t s_LutLib8 = { "lutlib", 8, 0, {0,1,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1},{1}} };
If_Lib_t s_LutLib7 = { "lutlib", 7, 0, {0,1,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1},{1}} };
If_Lib_t s_LutLib6 = { "lutlib", 6, 0, {0,1,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1},{1}} };
If_Lib_t s_LutLib5 = { "lutlib", 5, 0, {0,1,1,1,1,1}, {{0},{1},{1},{1},{1},{1}} };
If_Lib_t s_LutLib4 = { "lutlib", 4, 0, {0,1,1,1,1}, {{0},{1},{1},{1},{1}} };
If_Lib_t s_LutLib3 = { "lutlib", 3, 0, {0,1,1,1}, {{0},{1},{1},{1}} };
If_Lib_t * pLutLib;
assert( nLutSize >= 3 && nLutSize <= 10 );
switch ( nLutSize )
{
case 3: pLutLib = &s_LutLib3; break;
case 4: pLutLib = &s_LutLib4; break;
case 5: pLutLib = &s_LutLib5; break;
case 6: pLutLib = &s_LutLib6; break;
case 7: pLutLib = &s_LutLib7; break;
case 8: pLutLib = &s_LutLib8; break;
case 9: pLutLib = &s_LutLib9; break;
case 10: pLutLib = &s_LutLib10; break;
default: pLutLib = NULL; break;
}
if ( pLutLib == NULL )
return NULL;
return If_LutLibDup(pLutLib);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/map/if/ifMap.c
......@@ -295,13 +295,6 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
{
arrTime = Tim_ManGetPiArrival( p->pManTim, pObj->IdPio );
If_ObjSetArrTime( pObj, arrTime );
/*
if ( pObj->IdPio >= 2000 )
{
int x = 0;
printf( "+%d %6.3f ", pObj->IdPio, arrTime );
}
*/
}
else if ( If_ObjIsCo(pObj) )
{
......
src/map/if/ifUtil.c
......@@ -653,6 +653,40 @@ Vec_Ptr_t * If_ManCollectMappingDirect( If_Man_t * p )
/**Function*************************************************************
Synopsis [Collects nodes used in the mapping in the topological order.]
Description [Represents mapping as an array of integers.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * If_ManCollectMappingInt( If_Man_t * p )
{
Vec_Int_t * vOrder;
If_Cut_t * pCutBest;
If_Obj_t * pObj;
int i, k, nLeaves, * ppLeaves;
If_ManMarkMapping( p );
vOrder = Vec_IntAlloc( If_ManObjNum(p) );
If_ManForEachObj( p, pObj, i )
if ( If_ObjIsAnd(pObj) && pObj->nRefs )
{
pCutBest = If_ObjCutBest( pObj );
nLeaves = If_CutLeaveNum( pCutBest );
ppLeaves = If_CutLeaves( pCutBest );
// save the number of leaves, the leaves, and finally, the root
Vec_IntPush( vOrder, nLeaves );
for ( k = 0; k < nLeaves; k++ )
Vec_IntPush( vOrder, ppLeaves[k] );
Vec_IntPush( vOrder, pObj->Id );
}
return vOrder;
}
/**Function*************************************************************
Synopsis [Returns the number of POs pointing to the same internal nodes.]
Description []
......
src/map/if/module.make
SRC += src/map/if/ifCore.c \
src/map/if/ifCut.c \
src/map/if/ifLib.c \
src/map/if/ifMan.c \
src/map/if/ifMap.c \
src/map/if/ifReduce.c \
......
src/opt/mfs/mfsCore.c
......@@ -101,6 +101,7 @@ p->timeSat += clock() - clk;
int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Hop_Obj_t * pObj;
int RetValue;
extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
int nGain, clk;
......@@ -129,8 +130,15 @@ clk = clock();
if ( p->pSat == NULL )
return 0;
// solve the SAT problem
Abc_NtkMfsSolveSat( p, pNode );
RetValue = Abc_NtkMfsSolveSat( p, pNode );
p->nTotConfLevel += p->pSat->stats.conflicts;
p->timeSat += clock() - clk;
if ( RetValue == 0 )
{
p->nTimeOutsLevel++;
p->nTimeOuts++;
return 0;
}
// minimize the local function of the node using bi-decomposition
assert( p->nFanins == Abc_ObjFaninNum(pNode) );
pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare );
......@@ -139,6 +147,7 @@ p->timeSat += clock() - clk;
{
p->nNodesDec++;
p->nNodesGained += nGain;
p->nNodesGainedLevel += nGain;
pNode->pData = pObj;
}
return 1;
......@@ -163,7 +172,9 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
ProgressBar * pProgress;
Mfs_Man_t * p;
Abc_Obj_t * pObj;
int i, nFaninMax, clk = clock();
Vec_Vec_t * vLevels;
Vec_Ptr_t * vNodes;
int i, k, nNodes, nFaninMax, clk = clock(), clk2;
int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
......@@ -223,24 +234,44 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// compute don't-cares for each node
nNodes = 0;
p->nTotalNodesBeg = nTotalNodesBeg;
p->nTotalEdgesBeg = nTotalEdgesBeg;
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
vLevels = Abc_NtkLevelize( pNtk );
Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
{
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
continue;
if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
continue;
if ( !p->pPars->fVeryVerbose )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
Abc_NtkMfsNode( p, pObj );
Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
p->nNodesGainedLevel = 0;
p->nTotConfLevel = 0;
p->nTimeOutsLevel = 0;
clk2 = clock();
Vec_PtrForEachEntry( vNodes, pObj, i )
{
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
break;
if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
continue;
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
Abc_NtkMfsNode( p, pObj );
}
nNodes += Vec_PtrSize(vNodes);
if ( pPars->fVerbose )
{
printf( "Lev = %2d. Node = %4d. Ave gain = %6.2f. Ave conf = %6.2f. Timeouts = %6.2f %% ",
k, Vec_PtrSize(vNodes),
1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
PRT( "Time", clock() - clk2 );
}
}
Extra_ProgressBarStop( pProgress );
Abc_NtkStopReverseLevels( pNtk );
Vec_VecFree( vLevels );
// perform the sweeping
if ( !pPars->fResub )
......
src/opt/mfs/mfsInt.h
......@@ -70,6 +70,7 @@ struct Mfs_Man_t_
Bdc_Man_t * pManDec;
int nNodesDec;
int nNodesGained;
int nNodesGainedLevel;
// solving data
Aig_Man_t * pAigWin; // window AIG with constraints
Cnf_Dat_t * pCnf; // the CNF for the window
......@@ -78,6 +79,8 @@ struct Mfs_Man_t_
Vec_Int_t * vMem; // memory for intermediate SOPs
Vec_Vec_t * vLevels; // levelized structure for updating
Vec_Ptr_t * vFanins; // the new set of fanins
int nTotConfLim; // total conflict limit
int nTotConfLevel; // total conflicts on this level
// the result of solving
int nFanins; // the number of fanins
int nWords; // the number of words
......@@ -91,6 +94,7 @@ struct Mfs_Man_t_
int nNodesBad;
int nTotalDivs;
int nTimeOuts;
int nTimeOutsLevel;
int nDcMints;
double dTotalRatios;
// node/edge stats
......@@ -136,7 +140,7 @@ extern int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode
extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsSat.c ==========================================================*/
extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsStrash.c ==========================================================*/
extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
......
src/opt/mfs/mfsMan.c
......@@ -126,13 +126,13 @@ void Mfs_ManPrint( Mfs_Man_t * p )
}
else
{
printf( "Nodes = %d. DC mints in local space = %d. Total mints = %d. Ratio = %5.2f.\n",
p->nNodesTried, p->nMintsTotal-p->nMintsCare, p->nMintsTotal,
printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n",
Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare,
1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
// printf( "Average ratio of sequential DCs in the global space = %5.2f.\n",
// 1.0-(p->dTotalRatios/p->nNodesTried) );
printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d.\n",
p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained );
printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n",
p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts );
}
/*
PRTP( "Win", p->timeWin , p->timeTotal );
......
src/opt/mfs/mfsSat.c
......@@ -42,9 +42,14 @@
int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
{
int Lits[MFS_FANIN_MAX];
int RetValue, iVar, b, Mint;
RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
assert( RetValue == l_False || RetValue == l_True );
int RetValue, nBTLimit, iVar, b, Mint;
if ( p->nTotConfLim && p->nTotConfLim <= p->pSat->stats.conflicts )
return -1;
nBTLimit = p->nTotConfLim? p->nTotConfLim - p->pSat->stats.conflicts : 0;
RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
assert( RetValue == l_Undef || RetValue == l_True || RetValue == l_False );
if ( RetValue == l_Undef )
return -1;
if ( RetValue == l_False )
return 0;
p->nCares++;
......@@ -77,12 +82,12 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Aig_Obj_t * pObjPo;
int i;
int RetValue, i;
// collect projection variables
Vec_IntClear( p->vProjVars );
Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
......@@ -98,7 +103,10 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
// iterate through the SAT assignments
p->nCares = 0;
while ( Abc_NtkMfsSolveSat_iter(p) );
p->nTotConfLim = p->pPars->nBTLimit;
while ( (RetValue = Abc_NtkMfsSolveSat_iter(p)) == 1 );
if ( RetValue == -1 )
return 0;
// write statistics
p->nMintsCare += p->nCares;
......@@ -113,7 +121,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
// map the care
if ( p->nFanins > 4 )
return;
return 1;
if ( p->nFanins == 4 )
p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16);
if ( p->nFanins == 3 )
......@@ -122,6 +130,7 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
p->uCare[0] = p->uCare[0] | (p->uCare[0] << 4) | (p->uCare[0] << 8) | (p->uCare[0] << 12) |
(p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28);
assert( p->nFanins != 1 );
return 1;
}
////////////////////////////////////////////////////////////////////////
......
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