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

Version abc70906

This commit is contained in:
Alan Mishchenko 2007-09-06 08:01:00 -07:00
parent b2470dd3da
commit 9be1b07693
84 changed files with 3175 additions and 870 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Makefile
View File

@ -10,12 +10,12 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
src/base/io src/base/main src/base/ver \
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/ec src/aig/aig src/aig/kit \
src/aig/bdc \
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
src/aig/bdc src/aig/bar \
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
src/bdd/parse src/bdd/reo src/bdd/cas \
src/map/fpga src/map/mapper src/map/mio \
src/map/super src/map/if \
src/map/super src/map/if src/map/pcm \
src/misc/extra src/misc/mvc src/misc/st src/misc/util \
src/misc/espresso src/misc/nm src/misc/vec \
src/misc/hash \

106
abc.dsp
View File

@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\res" /I "src\opt\lpk" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\aig" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\aig\kit" /I "src\aig\bdc" /I "src\temp\esop" /I "src\phys\place" /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\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\res" /I "src\opt\lpk" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\aig" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\aig\kit" /I "src\aig\bdc" /I "src\aig\ioa" /I "src\aig\bar" /I "src\aig\pcm" /I "src\temp\esop" /I "src\phys\place" /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\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\res" /I "src\opt\lpk" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\aig" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\aig\kit" /I "src\aig\bdc" /I "src\temp\esop" /I "src\phys\place" /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\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\res" /I "src\opt\lpk" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\aig" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\aig\kit" /I "src\aig\bdc" /I "src\aig\ioa" /I "src\aig\bar" /I "src\aig\pcm" /I "src\temp\esop" /I "src\phys\place" /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"
@ -1845,6 +1845,74 @@ SOURCE=.\src\map\if\ifTruth.c
SOURCE=.\src\map\if\ifUtil.c
# End Source File
# End Group
# Begin Group "pcm"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\map\pcm\pcm.h
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmAbc.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmAig.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmApi.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmCore.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmCut.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmInt.h
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmIter.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmLib.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmMan.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmMap.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmPar.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmReduce.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmTime.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmTruth.c
# End Source File
# Begin Source File
SOURCE=.\src\map\pcm\pcmUtil.c
# End Source File
# End Group
# End Group
# Begin Group "misc"
@ -2509,9 +2577,25 @@ SOURCE=.\src\aig\mem\mem.c
SOURCE=.\src\aig\mem\mem.h
# End Source File
# End Group
# Begin Group "ec"
# Begin Group "ioa"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\aig\ioa\ioa.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\ioa\ioaReadAig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ioa\ioaUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ioa\ioaWriteAig.c
# End Source File
# End Group
# Begin Group "dar"
@ -2550,6 +2634,10 @@ SOURCE=.\src\aig\dar\darMan.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darPrec.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darRefact.c
# End Source File
# Begin Source File
@ -2849,6 +2937,18 @@ SOURCE=.\src\aig\aig\aigUtil.c
SOURCE=.\src\aig\aig\aigWin.c
# End Source File
# End Group
# Begin Group "bar"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\aig\bar\bar.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\bar\bar.h
# End Source File
# End Group
# End Group
# End Group
# Begin Group "Header Files"

3
abc.rc
View File

@ -168,7 +168,8 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
#alias t "r i10.blif; st; ps; csweep; ps; cec"
#alias t "r c/5/csat_777.bench; st; csweep -v"
#alias t "r i10.blif; st; drw -v"
alias t "r c.blif; st; drf"
#alias t "r c.blif; st; drf"
alias t "r i10.blif; st; dchoice; ps"
alias bmc "frames -i -F 10; orpos; iprove"

32
src/aig/aig/aig.h
View File

@ -85,6 +85,7 @@ struct Aig_Obj_t_ // 8 words
// the AIG manager
struct Aig_Man_t_
{
char * pName; // the design name
// AIG nodes
Vec_Ptr_t * vPis; // the array of PIs
Vec_Ptr_t * vPos; // the array of POs
@ -148,13 +149,16 @@ struct Aig_Man_t_
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
static inline int Aig_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Aig_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline unsigned Aig_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
static inline int Aig_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
static inline int Aig_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
static inline char * Aig_UtilStrsav( char * s ) { return s ? strcpy(ALLOC(char, strlen(s)+1), s) : NULL; }
static inline int Aig_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Aig_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline unsigned Aig_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
static inline int Aig_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
@ -178,7 +182,7 @@ static inline int Aig_ManLatchNum( Aig_Man_t * p ) { return p->nO
static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; }
static inline int Aig_ManObjIdMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
static inline int Aig_ManObjNumMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); }
@ -200,8 +204,9 @@ static inline int Aig_ObjIsAnd( Aig_Obj_t * pObj ) { return pObj-
static inline int Aig_ObjIsExor( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjIsLatch( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_LATCH; }
static inline int Aig_ObjIsNode( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; }
static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1; }
static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR || pObj->Type == AIG_OBJ_LATCH; }
static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1; }
static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR || pObj->Type == AIG_OBJ_LATCH; }
static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; }
static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; }
static inline void Aig_ObjSetMarkA( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; }
@ -234,6 +239,7 @@ static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj-
static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
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 int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )
{
if ( Aig_ObjFanin0(pObj) == pFanin ) return 0;
@ -362,6 +368,7 @@ extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p );
extern int Aig_ManLevelNum( Aig_Man_t * p );
extern int Aig_ManCountLevels( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj );
extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
@ -428,14 +435,15 @@ extern void Aig_ObjOrderAdvance( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan );
extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize );
/*=== aigRepr.c =========================================================*/
extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
extern void Aig_ManReprStop( Aig_Man_t * p );
extern void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern void Aig_ManCreateChoices( Aig_Man_t * p );
extern void Aig_ManMarkValidChoices( Aig_Man_t * p );
/*=== aigRet.c ========================================================*/
extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
/*=== aigScl.c ==========================================================*/

2
src/aig/aig/aigCheck.c
View File

@ -1,5 +1,5 @@
/**CFile****************************************************************
FileName [aigCheck.c]
SystemName [ABC: Logic synthesis and verification system.]

21
src/aig/aig/aigDfs.c
View File

@ -232,6 +232,27 @@ Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
return vNodes;
}
/**Function*************************************************************
Synopsis [Computes the max number of levels in the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManLevelNum( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
int i, LevelsMax;
LevelsMax = 0;
Aig_ManForEachPo( p, pObj, i )
LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
return LevelsMax;
}
/**Function*************************************************************
Synopsis [Computes the max number of levels in the manager.]

2
src/aig/aig/aigFanout.c
View File

@ -57,7 +57,7 @@ void Aig_ManFanoutStart( Aig_Man_t * p )
assert( Aig_ManBufNum(p) == 0 );
// allocate fanout datastructure
assert( p->pFanData == NULL );
p->nFansAlloc = 2 * Aig_ManObjIdMax(p);
p->nFansAlloc = 2 * Aig_ManObjNumMax(p);
if ( p->nFansAlloc < (1<<12) )
p->nFansAlloc = (1<<12);
p->pFanData = ALLOC( int, 5 * p->nFansAlloc );

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

@ -87,7 +87,8 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
Aig_Obj_t * pObj;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
// create the PIs
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
@ -134,7 +135,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
Aig_Obj_t * pObj;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
// create the PIs
@ -187,7 +189,8 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t *
Aig_Obj_t * pObj;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@ -240,6 +243,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vBufs ) Vec_PtrFree( p->vBufs );
if ( p->vLevelR ) Vec_IntFree( p->vLevelR );
if ( p->vLevels ) Vec_VecFree( p->vLevels );
FREE( p->pName );
FREE( p->pObjCopies );
FREE( p->pReprs );
FREE( p->pEquivs );
@ -298,7 +302,7 @@ void Aig_ManPrintStats( Aig_Man_t * p )
// printf( "Cre = %6d. ", p->nCreated );
// printf( "Del = %6d. ", p->nDeleted );
// printf( "Lev = %3d. ", Aig_ManCountLevels(p) );
printf( "Max = %7d. ", Aig_ManObjIdMax(p) );
printf( "Max = %7d. ", Aig_ManObjNumMax(p) );
printf( "Lev = %3d. ", Aig_ManLevels(p) );
printf( "\n" );
}

2
src/aig/aig/aigOrder.c
View File

@ -46,7 +46,7 @@ void Aig_ManOrderStart( Aig_Man_t * p )
assert( Aig_ManBufNum(p) == 0 );
// allocate order datastructure
assert( p->pOrderData == NULL );
p->nOrderAlloc = 2 * Aig_ManObjIdMax(p);
p->nOrderAlloc = 2 * Aig_ManObjNumMax(p);
if ( p->nOrderAlloc < (1<<12) )
p->nOrderAlloc = (1<<12);
p->pOrderData = ALLOC( unsigned, 2 * p->nOrderAlloc );

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

@ -445,7 +445,7 @@ int Aig_ManPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
if ( Vec_IntSize(vPartSupp) < 100 )
Repulse = 1;
else
Repulse = 1+Extra_Base2Log(Vec_IntSize(vPartSupp)-100);
Repulse = 1+Aig_Base2Log(Vec_IntSize(vPartSupp)-100);
Value = Attract/Repulse;
if ( ValueBest < Value )
{
@ -484,7 +484,7 @@ void Aig_ManPartitionPrint( Aig_Man_t * p, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vP
break;
}
assert( Counter == Aig_ManPoNum(p) );
printf( "\nTotal = %d. Outputs = %d.\n", Counter, Aig_ManPoNum(p) );
// printf( "\nTotal = %d. Outputs = %d.\n", Counter, Aig_ManPoNum(p) );
}
/**Function*************************************************************
@ -719,18 +719,22 @@ Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize )
SeeAlso []
***********************************************************************/
Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t * pObj, Vec_Int_t * vSuppMap )
{
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
if ( Aig_ObjIsTravIdCurrent(pOld, pObj) )
return pObj->pData;
Aig_ObjSetTravIdCurrent(pOld, pObj);
if ( Aig_ObjIsPi(pObj) )
{
assert( Vec_IntSize(vSuppMap) == Aig_ManPiNum(pNew) );
Vec_IntPush( vSuppMap, (int)pObj->pNext );
return pObj->pData = Aig_ObjCreatePi(pNew);
}
assert( Aig_ObjIsNode(pObj) );
Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin0(pObj) );
Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin1(pObj) );
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
Aig_ObjSetTravIdCurrent(p, pObj);
return pObj->pData;
Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin0(pObj), vSuppMap );
Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin1(pObj), vSuppMap );
return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
/**Function*************************************************************
@ -744,43 +748,60 @@ Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManDupPart( Aig_Man_t * pNew, Aig_Man_t * p, Vec_Int_t * vPart, Vec_Int_t * vPartSupp, int fInverse )
Vec_Ptr_t * Aig_ManDupPart( Aig_Man_t * pNew, Aig_Man_t * pOld, Vec_Int_t * vPart, Vec_Int_t * vSuppMap, int fInverse )
{
Vec_Ptr_t * vOutputs;
Aig_Obj_t * pObj, * pObjNew;
int Entry, k;
Vec_Ptr_t * vOutsTotal;
Aig_Obj_t * pObj;
int Entry, i;
// create the PIs
Aig_ManIncrementTravId( p );
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManIncrementTravId( pOld );
Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
Aig_ObjSetTravIdCurrent( pOld, Aig_ManConst1(pOld) );
if ( !fInverse )
{
Vec_IntForEachEntry( vPartSupp, Entry, k )
Vec_IntForEachEntry( vSuppMap, Entry, i )
{
pObj = Aig_ManPi( p, Entry );
pObj->pData = Aig_ManPi( pNew, k );
Aig_ObjSetTravIdCurrent( p, pObj );
pObj = Aig_ManPi( pOld, Entry );
pObj->pData = Aig_ManPi( pNew, i );
Aig_ObjSetTravIdCurrent( pOld, pObj );
}
}
else
{
Vec_IntForEachEntry( vPartSupp, Entry, k )
Vec_IntForEachEntry( vSuppMap, Entry, i )
{
pObj = Aig_ManPi( p, k );
pObj = Aig_ManPi( pOld, i );
pObj->pData = Aig_ManPi( pNew, Entry );
Aig_ObjSetTravIdCurrent( p, pObj );
Aig_ObjSetTravIdCurrent( pOld, pObj );
}
vSuppMap = NULL; // should not be useful
}
// create the internal nodes
vOutputs = Vec_PtrAlloc( Vec_IntSize(vPart) );
Vec_IntForEachEntry( vPart, Entry, k )
vOutsTotal = Vec_PtrAlloc( Vec_IntSize(vPart) );
if ( !fInverse )
{
pObj = Aig_ManPo( p, Entry );
pObjNew = Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin0(pObj) );
pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
Vec_PtrPush( vOutputs, pObjNew );
Vec_IntForEachEntry( vPart, Entry, i )
{
pObj = Aig_ManPo( pOld, Entry );
Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin0(pObj), vSuppMap );
Vec_PtrPush( vOutsTotal, Aig_ObjChild0Copy(pObj) );
}
}
return vOutputs;
else
{
Aig_ManForEachObj( pOld, pObj, i )
{
if ( Aig_ObjIsPo(pObj) )
{
Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin0(pObj), vSuppMap );
Vec_PtrPush( vOutsTotal, Aig_ObjChild0Copy(pObj) );
}
else if ( Aig_ObjIsNode(pObj) && pObj->nRefs == 0 )
Aig_ManDupPart_rec( pNew, pOld, pObj, vSuppMap );
}
}
return vOutsTotal;
}
/**Function*************************************************************
@ -814,6 +835,7 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
vPartSupp = Vec_PtrEntry( vPartSupps, i );
// create the new miter
pNew = Aig_ManStart( 1000 );
// pNew->pName = Extra_UtilStrsav( p1->pName );
// create the PIs
for ( k = 0; k < Vec_IntSize(vPartSupp); k++ )
Aig_ObjCreatePi( pNew );
@ -822,6 +844,8 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
vNodes2 = Aig_ManDupPart( pNew, p2, vPart, vPartSupp, 0 );
// create the miter
pMiter = Aig_MiterTwo( pNew, vNodes1, vNodes2 );
Vec_PtrFree( vNodes1 );
Vec_PtrFree( vNodes2 );
// create the output
Aig_ObjCreatePo( pNew, pMiter );
// clean up
@ -847,90 +871,115 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
***********************************************************************/
Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
{
Aig_Man_t * pChoice, * pNew, * pAig, * p;
Aig_Obj_t * pObj;
Vec_Ptr_t * vMiters, * vNodes;
Vec_Ptr_t * vParts, * vPartSupps;
extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
extern void * Abc_FrameGetGlobalFrame();
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
Vec_Ptr_t * vOutsTotal, * vOuts;
Aig_Man_t * pAigTotal, * pAigPart, * pAig;
Vec_Int_t * vPart, * vPartSupp;
Vec_Ptr_t * vParts;
Aig_Obj_t * pObj;
void ** ppData;
int i, k, m;
// partition the first AIG
// partition the first AIG in the array
assert( Vec_PtrSize(vAigs) > 1 );
pAig = Vec_PtrEntry( vAigs, 0 );
vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, &vPartSupps );
vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, NULL );
// derive the AIG partitions
vMiters = Vec_PtrAlloc( Vec_PtrSize(vParts) );
for ( i = 0; i < Vec_PtrSize(vParts); i++ )
// start the total fraiged AIG
pAigTotal = Aig_ManStartFrom( pAig );
Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) );
vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) );
// set the PI numbers
Vec_PtrForEachEntry( vAigs, pAig, i )
Aig_ManForEachPi( pAig, pObj, k )
pObj->pNext = (Aig_Obj_t *)k;
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
// create the total fraiged AIG
vPartSupp = Vec_IntAlloc( 100 ); // maps part PI num into total PI num
Vec_PtrForEachEntry( vParts, vPart, i )
{
// get partitions and their support
vPart = Vec_PtrEntry( vParts, i );
vPartSupp = Vec_PtrEntry( vPartSupps, i );
// create the new miter
pNew = Aig_ManStart( 1000 );
// create the PIs
for ( k = 0; k < Vec_IntSize(vPartSupp); k++ )
Aig_ObjCreatePi( pNew );
// copy the components
Vec_PtrForEachEntry( vAigs, p, k )
// derive the partition AIG
pAigPart = Aig_ManStart( 5000 );
// pAigPart->pName = Extra_UtilStrsav( pAigPart->pName );
Vec_IntClear( vPartSupp );
Vec_PtrForEachEntry( vAigs, pAig, k )
{
vNodes = Aig_ManDupPart( pNew, p, vPart, vPartSupp, 0 );
Vec_PtrForEachEntry( vNodes, pObj, m )
Aig_ObjCreatePo( pNew, pObj );
Vec_PtrFree( vNodes );
}
// add to the partitions
Vec_PtrPush( vMiters, pNew );
}
// perform choicing for each derived AIG
Vec_PtrForEachEntry( vMiters, pNew, i )
{
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
pNew = Fra_FraigChoice( p = pNew );
Vec_PtrWriteEntry( vMiters, i, pNew );
Aig_ManStop( p );
}
// combine the resulting AIGs
pNew = Aig_ManStartFrom( pAig );
Vec_PtrForEachEntry( vMiters, p, i )
{
// get partitions and their support
vPart = Vec_PtrEntry( vParts, i );
vPartSupp = Vec_PtrEntry( vPartSupps, i );
// copy the component
vNodes = Aig_ManDupPart( pNew, p, vPart, vPartSupp, 1 );
assert( Vec_PtrSize(vNodes) == Vec_PtrSize(vParts) * Vec_PtrSize(vAigs) );
// create choice node
for ( k = 0; k < Vec_PtrSize(vParts); k++ )
{
for ( m = 0; m < Vec_PtrSize(vAigs); m++ )
vOuts = Aig_ManDupPart( pAigPart, pAig, vPart, vPartSupp, 0 );
if ( k == 0 )
{
pObj = Aig_ObjChild0( Vec_PtrEntry(vNodes, k * Vec_PtrSize(vAigs) + m) );
break;
Vec_PtrForEachEntry( vOuts, pObj, m )
Aig_ObjCreatePo( pAigPart, pObj );
}
Aig_ObjCreatePo( pNew, pObj );
Vec_PtrFree( vOuts );
}
Vec_PtrFree( vNodes );
// derive the total AIG from the partitioned AIG
vOuts = Aig_ManDupPart( pAigTotal, pAigPart, vPart, vPartSupp, 1 );
// add to the outputs
Vec_PtrForEachEntry( vOuts, pObj, k )
{
assert( Vec_PtrEntry( vOutsTotal, Vec_IntEntry(vPart,k) ) == NULL );
Vec_PtrWriteEntry( vOutsTotal, Vec_IntEntry(vPart,k), pObj );
}
Vec_PtrFree( vOuts );
// store contents of pData pointers
ppData = ALLOC( void *, Aig_ManObjNumMax(pAigPart) );
Aig_ManForEachObj( pAigPart, pObj, k )
ppData[k] = pObj->pData;
// report the process
printf( "Fraiging part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart),
Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) );
// compute equivalence classes (to be stored in pNew->pReprs)
pAig = Fra_FraigChoice( pAigPart, 1000 );
Aig_ManStop( pAig );
// reset the pData pointers
Aig_ManForEachObj( pAigPart, pObj, k )
pObj->pData = ppData[k];
free( ppData );
// transfer representatives to the total AIG
if ( pAigPart->pReprs )
Aig_ManTransferRepr( pAigTotal, pAigPart );
Aig_ManStop( pAigPart );
}
printf( " \r" );
Vec_VecFree( (Vec_Vec_t *)vParts );
Vec_VecFree( (Vec_Vec_t *)vPartSupps );
Vec_IntFree( vPartSupp );
// trasfer representatives
Aig_ManReprStart( pNew, Aig_ManObjIdMax(pNew)+1 );
Vec_PtrForEachEntry( vMiters, p, i )
{
Aig_ManTransferRepr( pNew, p );
Aig_ManStop( p );
}
Vec_PtrFree( vMiters );
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
// clear the PI numbers
Vec_PtrForEachEntry( vAigs, pAig, i )
Aig_ManForEachPi( pAig, pObj, k )
pObj->pNext = NULL;
/*
// collect the missing outputs (outputs whose driver is not a node)
pAig = Vec_PtrEntry( vAigs, 0 );
Aig_ManConst1(pAig)->pData = Aig_ManConst1(pAigTotal);
Aig_ManForEachPi( pAig, pObj, i )
pAig->pData = Aig_ManPi( pAigTotal, i );
Aig_ManForEachPo( pAig, pObj, i )
if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) )
{
assert( Vec_PtrEntry( vOutsTotal, i ) == NULL );
Vec_PtrWriteEntry( vOutsTotal, i, Aig_ObjChild0Copy(pObj) );
}
*/
// add the outputs in the same order
Vec_PtrForEachEntry( vOutsTotal, pObj, i )
Aig_ObjCreatePo( pAigTotal, pObj );
Vec_PtrFree( vOutsTotal );
// derive the result of choicing
pChoice = Aig_ManRehash( pNew );
if ( pChoice != pNew )
Aig_ManStop( pNew );
return pChoice;
pAig = Aig_ManRehash( pAigTotal );
// create the equivalent nodes lists
Aig_ManMarkValidChoices( pAig );
return pAig;
}

49
src/aig/aig/aigRepr.c
View File

@ -164,11 +164,13 @@ static inline void Aig_ObjClearRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
SeeAlso []
***********************************************************************/
static inline Aig_Obj_t * Aig_ObjFindReprTrans( Aig_Man_t * p, Aig_Obj_t * pNode )
static inline Aig_Obj_t * Aig_ObjFindReprTransitive( Aig_Man_t * p, Aig_Obj_t * pNode )
{
Aig_Obj_t * pPrev, * pRepr;
for ( pPrev = NULL, pRepr = Aig_ObjFindRepr(p, pNode); pRepr; pPrev = pRepr, pRepr = Aig_ObjFindRepr(p, pRepr) );
return pPrev;
Aig_Obj_t * pNext, * pRepr;
if ( (pRepr = Aig_ObjFindRepr(p, pNode)) )
while ( (pNext = Aig_ObjFindRepr(p, pRepr)) )
pRepr = pNext;
return pRepr;
}
/**Function*************************************************************
@ -203,14 +205,22 @@ static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) {
SeeAlso []
***********************************************************************/
void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * pOld )
{
Aig_Obj_t * pObj, * pRepr;
int k;
assert( pNew->pReprs != NULL );
// extend storage to fix pNew
if ( pNew->nReprsAlloc < Aig_ManObjNumMax(pNew) )
{
int nReprsAllocNew = 2 * Aig_ManObjNumMax(pNew);
pNew->pReprs = REALLOC( Aig_Obj_t *, pNew->pReprs, nReprsAllocNew );
memset( pNew->pReprs + pNew->nReprsAlloc, 0, sizeof(Aig_Obj_t *) * (nReprsAllocNew-pNew->nReprsAlloc) );
pNew->nReprsAlloc = nReprsAllocNew;
}
// go through the nodes which have representatives
Aig_ManForEachObj( p, pObj, k )
if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
Aig_ManForEachObj( pOld, pObj, k )
if ( (pRepr = Aig_ObjFindRepr(pOld, pObj)) )
Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) );
}
@ -251,16 +261,15 @@ Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
{
int fOrdered = 0;
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
// start the HOP package
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 );
// map the const and primary inputs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@ -303,7 +312,7 @@ int Aig_ManRemapRepr( Aig_Man_t * p )
int i, nFanouts = 0;
Aig_ManForEachNode( p, pObj, i )
{
pRepr = Aig_ObjFindReprTrans( p, pObj );
pRepr = Aig_ObjFindReprTransitive( p, pObj );
if ( pRepr == NULL )
continue;
assert( pRepr->Id < pObj->Id );
@ -379,10 +388,14 @@ int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld )
Aig_Man_t * Aig_ManRehash( Aig_Man_t * p )
{
Aig_Man_t * pTemp;
int i, nFanouts;
assert( p->pReprs != NULL );
while ( Aig_ManRemapRepr( p ) )
for ( i = 0; nFanouts = Aig_ManRemapRepr( p ); i++ )
{
p = Aig_ManDupRepr( pTemp = p );
// printf( "Iter = %3d. Fanouts = %6d. Nodes = %7d.\n", i+1, nFanouts, Aig_ManNodeNum(p) );
p = Aig_ManDupRepr( pTemp = p, 1 );
Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
Aig_ManTransferRepr( p, pTemp );
Aig_ManStop( pTemp );
}
return p;
@ -390,7 +403,7 @@ Aig_Man_t * Aig_ManRehash( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Creates choices.]
Synopsis [Marks the nodes that are Creates choices.]
Description [The input AIG is assumed to have representatives assigned.]
@ -399,15 +412,15 @@ Aig_Man_t * Aig_ManRehash( Aig_Man_t * p )
SeeAlso []
***********************************************************************/
void Aig_ManCreateChoices( Aig_Man_t * p )
void Aig_ManMarkValidChoices( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pRepr;
int i;
assert( p->pReprs != NULL );
// create equivalent nodes in the manager
assert( p->pEquivs == NULL );
p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p) + 1 );
memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p) + 1) );
p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
// make the choice nodes
Aig_ManForEachNode( p, pObj, i )
{

5
src/aig/aig/aigRet.c
View File

@ -275,10 +275,12 @@ void Rtm_PrintEdge( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
{
unsigned LData = pEdge->LData;
printf( "%d : ", pEdge->nLats );
/*
if ( pEdge->nLats > 10 )
Extra_PrintBinary( stdout, p->pExtra + pEdge->LData, 2*(pEdge->nLats+1) );
else
Extra_PrintBinary( stdout, &LData, 2*(pEdge->nLats+1) );
*/
printf( "\n" );
}
@ -804,7 +806,7 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
pObjNew = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + m );
pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE );
}
assert( Aig_Regular(pObjNew)->nRefs > 0 );
// assert( Aig_Regular(pObjNew)->nRefs > 0 );
}
free( pLatches );
pNew->nRegs = nLatches;
@ -947,6 +949,7 @@ clk = clock();
// get the new manager
pNew = Rtm_ManToAig( pRtm );
pNew->pName = Aig_UtilStrsav( p->pName );
Rtm_ManFree( pRtm );
// group the registers
clk = clock();

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

@ -46,7 +46,8 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
Aig_Obj_t * pObj, * pObjMapped;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
// create the PIs
@ -285,7 +286,7 @@ Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
Aig_ManForEachPiSeq( p, pObj, i )
Vec_PtrPush( vMap, pObj );
// create mapping of fanin nodes into the corresponding latch outputs
pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) );
pMapping = ALLOC( int, 2 * Aig_ManObjNumMax(p) );
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
pFanin = Aig_ObjFanin0(pObjLi);
@ -358,6 +359,8 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
printf( "\n" );
}
if ( p->nRegs == 0 )
break;
}
return p;
}

2
src/aig/aig/aigShow.c
View File

@ -128,7 +128,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
fprintf( pFile, "%s", "AIG structure visualized by ABC" );
fprintf( pFile, "\\n" );
fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" );
fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
// fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
fprintf( pFile, "\"\n" );
fprintf( pFile, " ];\n" );
fprintf( pFile, "}" );

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

@ -74,7 +74,7 @@ void Aig_TableResize( Aig_Man_t * p )
{
Aig_Obj_t * pEntry, * pNext;
Aig_Obj_t ** pTableOld, ** ppPlace;
int nTableSizeOld, Counter, nEntries, i, clk;
int nTableSizeOld, Counter, i, clk;
clk = clock();
// save the old table
pTableOld = p->pTable;
@ -97,10 +97,9 @@ clk = clock();
pEntry->pNext = NULL;
Counter++;
}
nEntries = Aig_ManNodeNum(p);
assert( Counter == nEntries );
printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
PRT( "Time", clock() - clk );
assert( Counter == Aig_ManNodeNum(p) );
// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
// PRT( "Time", clock() - clk );
// replace the table and the parameters
free( pTableOld );
}

2
src/aig/aig/aigTiming.c
View File

@ -147,7 +147,7 @@ void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease )
p->nLevelMax = Aig_ManLevels(p) + nMaxLevelIncrease;
// start the reverse levels
p->vLevelR = Vec_IntAlloc( 0 );
Vec_IntFill( p->vLevelR, 1 + Aig_ManObjIdMax(p), 0 );
Vec_IntFill( p->vLevelR, Aig_ManObjNumMax(p), 0 );
// compute levels in reverse topological order
vNodes = Aig_ManDfsReverse( p );
Vec_PtrForEachEntry( vNodes, pObj, i )

2
src/aig/aig/aigUtil.c
View File

@ -679,7 +679,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
pObj->pData = (void *)Counter++;
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pData = (void *)Counter++;
nDigits = Extra_Base10Log( Counter );
nDigits = Aig_Base10Log( Counter );
// write the file
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif() in ABC\n" );

177
src/aig/bar/bar.c Normal file
View File

@ -0,0 +1,177 @@
/**CFile****************************************************************
FileName [bar.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [extra]
Synopsis [Progress bar.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bar.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
struct Bar_Progress_t_
{
int nItemsNext; // the number of items for the next update of the progress bar
int nItemsTotal; // the total number of items
int posTotal; // the total number of positions
int posCur; // the current position
FILE * pFile; // the output stream
};
static void Bar_ProgressShow( Bar_Progress_t * p, char * pString );
static void Bar_ProgressClean( Bar_Progress_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the progress bar.]
Description [The first parameter is the output stream (pFile), where
the progress is printed. The current printing position should be the
first one on the given line. The second parameters is the total
number of items that correspond to 100% position of the progress bar.]
SideEffects []
SeeAlso []
***********************************************************************/
Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal )
{
Bar_Progress_t * p;
// extern int Abc_FrameShowProgress( void * p );
// extern void * Abc_FrameGetGlobalFrame();
// if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
p = (Bar_Progress_t *) malloc(sizeof(Bar_Progress_t));
memset( p, 0, sizeof(Bar_Progress_t) );
p->pFile = pFile;
p->nItemsTotal = nItemsTotal;
p->posTotal = 78;
p->posCur = 1;
p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal);
Bar_ProgressShow( p, NULL );
return p;
}
/**Function*************************************************************
Synopsis [Updates the progress bar.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bar_ProgressUpdate_int( Bar_Progress_t * p, int nItemsCur, char * pString )
{
if ( p == NULL ) return;
if ( nItemsCur < p->nItemsNext )
return;
if ( nItemsCur >= p->nItemsTotal )
{
p->posCur = 78;
p->nItemsNext = 0x7FFFFFFF;
}
else
{
p->posCur += 7;
p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal);
}
Bar_ProgressShow( p, pString );
}
/**Function*************************************************************
Synopsis [Stops the progress bar.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bar_ProgressStop( Bar_Progress_t * p )
{
if ( p == NULL ) return;
Bar_ProgressClean( p );
free( p );
}
/**Function*************************************************************
Synopsis [Prints the progress bar of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bar_ProgressShow( Bar_Progress_t * p, char * pString )
{
int i;
if ( p == NULL ) return;
if ( pString )
fprintf( p->pFile, "%s ", pString );
for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ )
fprintf( p->pFile, "-" );
if ( i == p->posCur )
fprintf( p->pFile, ">" );
for ( i++ ; i <= p->posTotal; i++ )
fprintf( p->pFile, " " );
fprintf( p->pFile, "\r" );
fflush( stdout );
}
/**Function*************************************************************
Synopsis [Cleans the progress bar before quitting.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bar_ProgressClean( Bar_Progress_t * p )
{
int i;
if ( p == NULL ) return;
for ( i = 0; i <= p->posTotal; i++ )
fprintf( p->pFile, " " );
fprintf( p->pFile, "\r" );
fflush( stdout );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

74
src/aig/bar/bar.h Normal file
View File

@ -0,0 +1,74 @@
/**CFile****************************************************************
FileName [bar.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Progress bar.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bar.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __BAR_H__
#define __BAR_H__
#ifdef __cplusplus
extern "C" {
#endif
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define BAR_PROGRESS_USE 1
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Bar_Progress_t_ Bar_Progress_t;
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== bar.c ==========================================================*/
extern Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal );
extern void Bar_ProgressStop( Bar_Progress_t * p );
extern void Bar_ProgressUpdate_int( Bar_Progress_t * p, int nItemsCur, char * pString );
static inline void Bar_ProgressUpdate( Bar_Progress_t * p, int nItemsCur, char * pString ) {
if ( BAR_PROGRESS_USE && p && (nItemsCur < *((int*)p)) ) return; Bar_ProgressUpdate_int(p, nItemsCur, pString); }
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/aig/bar/module.make Normal file
View File

@ -0,0 +1 @@
SRC += src/aig/bar/bar.c

4
src/aig/cnf/cnfMap.c
View File

@ -100,8 +100,8 @@ void Cnf_DeriveMapping( Cnf_Man_t * p )
Dar_Cut_t * pCut, * pCutBest;
int i, k, AreaFlow, * pAreaFlows;
// allocate area flows
pAreaFlows = ALLOC( int, Aig_ManObjIdMax(p->pManAig) + 1 );
memset( pAreaFlows, 0, sizeof(int) * (Aig_ManObjIdMax(p->pManAig) + 1) );
pAreaFlows = ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
memset( pAreaFlows, 0, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
// visit the nodes in the topological order and update their best cuts
vSuper = Vec_PtrAlloc( 100 );
Aig_ManForEachNode( p->pManAig, pObj, i )

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

@ -214,8 +214,8 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
// create room for variable numbers
pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) );
pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
// assign variables to the last (nOutputs) POs
Number = 1;
if ( nOutputs )
@ -246,7 +246,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
for ( k = 0; k < (int)pCut->nFanins; k++ )
{
pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
assert( pVars[k] <= Aig_ManObjIdMax(p->pManAig) );
assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
}
// positive polarity of the cut
@ -285,7 +285,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
// write the constant literal
OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
assert( OutVar <= Aig_ManObjIdMax(p->pManAig) );
assert( OutVar <= Aig_ManObjNumMax(p->pManAig) );
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
@ -353,8 +353,8 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
// create room for variable numbers
pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p)) );
pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
// assign variables to the last (nOutputs) POs
Number = 1;
if ( nOutputs )
@ -403,7 +403,7 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
// write the constant literal
OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
assert( OutVar <= Aig_ManObjIdMax(p) );
assert( OutVar <= Aig_ManObjNumMax(p) );
*pClas++ = pLits;
*pLits++ = 2 * OutVar;

10
src/aig/csw/cswMan.c
View File

@ -57,11 +57,11 @@ Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVer
p->pManRes = Aig_ManStartFrom( pMan );
assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManRes) );
// allocate room for cuts and equivalent nodes
p->pnRefs = ALLOC( int, Aig_ManObjIdMax(pMan) + 1 );
p->pEquiv = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(pMan) + 1 );
p->pCuts = ALLOC( Csw_Cut_t *, Aig_ManObjIdMax(pMan) + 1 );
memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pMan) + 1) );
memset( p->pnRefs, 0, sizeof(int) * (Aig_ManObjIdMax(pMan) + 1) );
p->pnRefs = ALLOC( int, Aig_ManObjNumMax(pMan) );
p->pEquiv = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pMan) );
p->pCuts = ALLOC( Csw_Cut_t *, Aig_ManObjNumMax(pMan) );
memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) );
memset( p->pnRefs, 0, sizeof(int) * Aig_ManObjNumMax(pMan) );
// allocate memory manager
p->nTruthWords = Aig_TruthWordNum(nLeafMax);
p->nCutSize = sizeof(Csw_Cut_t) + sizeof(int) * nLeafMax + sizeof(unsigned) * p->nTruthWords;

4
src/aig/dar/dar.h
View File

@ -86,8 +86,10 @@ extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
/*=== darScript.c ========================================================*/
extern Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig );
extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
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 fVerbose );
extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
#ifdef __cplusplus
}

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

@ -53,7 +53,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
Vec_Vec_t * vStore;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->nRegs = p->nRegs;
pNew->nAsserts = p->nAsserts;
// map the PI nodes

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

@ -65,7 +65,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
{
Dar_Man_t * p;
ProgressBar * pProgress;
Bar_Progress_t * pProgress;
Dar_Cut_t * pCut;
Aig_Obj_t * pObj, * pObjNew;
int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
@ -88,15 +88,15 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
p->nNodesInit = Aig_ManNodeNum(pAig);
nNodesOld = Vec_PtrSize( pAig->vObjs );
pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
pProgress = Bar_ProgressStart( stdout, nNodesOld );
Aig_ManForEachObj( pAig, pObj, i )
// pProgress = Extra_ProgressBarStart( stdout, 100 );
// pProgress = Bar_ProgressStart( stdout, 100 );
// Aig_ManOrderStart( pAig );
// Aig_ManForEachNodeInOrder( pAig, pObj )
{
// Extra_ProgressBarUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
// Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL );
Extra_ProgressBarUpdate( pProgress, i, NULL );
Bar_ProgressUpdate( pProgress, i, NULL );
if ( !Aig_ObjIsNode(pObj) )
continue;
if ( i > nNodesOld )
@ -167,7 +167,7 @@ p->timeCuts += clock() - clk;
p->timeTotal = clock() - clkStart;
p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
Extra_ProgressBarStop( pProgress );
Bar_ProgressStop( pProgress );
p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
Dar_ManCutsFree( p );
// put the nodes into the DFS order and reassign their IDs

4
src/aig/dar/darInt.h
View File

@ -38,6 +38,7 @@ extern "C" {
#include "vec.h"
#include "aig.h"
#include "dar.h"
#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -148,6 +149,9 @@ extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
extern void Dar_ManStop( Dar_Man_t * p );
extern void Dar_ManPrintStats( Dar_Man_t * p );
/*=== darPrec.c ============================================================*/
extern char ** Dar_Permutations( int n );
extern void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );
#ifdef __cplusplus
}

8
src/aig/dar/darLib.c
View File

@ -129,8 +129,8 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs )
p->pObjs = ALLOC( Dar_LibObj_t, nObjs );
memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs );
// allocate canonical data
p->pPerms4 = Extra_Permutations( 4 );
Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
p->pPerms4 = Dar_Permutations( 4 );
Dar_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
// start the elementary objects
p->iObj = 4;
for ( i = 0; i < 4; i++ )
@ -570,8 +570,8 @@ void Dar_LibStart()
int clk = clock();
assert( s_DarLib == NULL );
s_DarLib = Dar_LibRead();
printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
PRT( "Time", clock() - clk );
// printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
// PRT( "Time", clock() - clk );
}
/**Function*************************************************************

388
src/aig/dar/darPrec.c Normal file
View File

@ -0,0 +1,388 @@
/**CFile****************************************************************
FileName [darPrec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis [Truth table precomputation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: darPrec.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "darInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocated one-memory-chunk array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void ** Dar_ArrayAlloc( int nCols, int nRows, int Size )
{
char ** pRes;
char * pBuffer;
int i;
assert( nCols > 0 && nRows > 0 && Size > 0 );
pBuffer = ALLOC( char, nCols * (sizeof(void *) + nRows * Size) );
pRes = (char **)pBuffer;
pRes[0] = pBuffer + nCols * sizeof(void *);
for ( i = 1; i < nCols; i++ )
pRes[i] = pRes[0] + i * nRows * Size;
return pRes;
}
/**Function********************************************************************
Synopsis [Computes the factorial.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Dar_Factorial( int n )
{
int i, Res = 1;
for ( i = 1; i <= n; i++ )
Res *= i;
return Res;
}
/**Function********************************************************************
Synopsis [Fills in the array of permutations.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
void Dar_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
{
char ** pNext;
int nFactNext;
int iTemp, iCur, iLast, k;
if ( n == 1 )
{
pRes[0][0] = Array[0];
return;
}
// get the next factorial
nFactNext = nFact / n;
// get the last entry
iLast = n - 1;
for ( iCur = 0; iCur < n; iCur++ )
{
// swap Cur and Last
iTemp = Array[iCur];
Array[iCur] = Array[iLast];
Array[iLast] = iTemp;
// get the pointer to the current section
pNext = pRes + (n - 1 - iCur) * nFactNext;
// set the last entry
for ( k = 0; k < nFactNext; k++ )
pNext[k][iLast] = Array[iLast];
// call recursively for this part
Dar_Permutations_rec( pNext, nFactNext, n - 1, Array );
// swap them back
iTemp = Array[iCur];
Array[iCur] = Array[iLast];
Array[iLast] = iTemp;
}
}
/**Function********************************************************************
Synopsis [Computes the set of all permutations.]
Description [The number of permutations in the array is n!. The number of
entries in each permutation is n. Therefore, the resulting array is a
two-dimentional array of the size: n! x n. To free the resulting array,
call free() on the pointer returned by this procedure.]
SideEffects []
SeeAlso []
******************************************************************************/
char ** Dar_Permutations( int n )
{
char Array[50];
char ** pRes;
int nFact, i;
// allocate memory
nFact = Dar_Factorial( n );
pRes = (char **)Dar_ArrayAlloc( nFact, n, sizeof(char) );
// fill in the permutations
for ( i = 0; i < n; i++ )
Array[i] = i;
Dar_Permutations_rec( pRes, nFact, n, Array );
// print the permutations
/*
{
int i, k;
for ( i = 0; i < nFact; i++ )
{
printf( "{" );
for ( k = 0; k < n; k++ )
printf( " %d", pRes[i][k] );
printf( " }\n" );
}
}
*/
return pRes;
}
/**Function*************************************************************
Synopsis [Permutes the given vector of minterms.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_TruthPermute_int( int * pMints, int nMints, char * pPerm, int nVars, int * pMintsP )
{
int m, v;
// clean the storage for minterms
memset( pMintsP, 0, sizeof(int) * nMints );
// go through minterms and add the variables
for ( m = 0; m < nMints; m++ )
for ( v = 0; v < nVars; v++ )
if ( pMints[m] & (1 << v) )
pMintsP[m] |= (1 << pPerm[v]);
}
/**Function*************************************************************
Synopsis [Permutes the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Dar_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReverse )
{
unsigned Result;
int * pMints;
int * pMintsP;
int nMints;
int i, m;
assert( nVars < 6 );
nMints = (1 << nVars);
pMints = ALLOC( int, nMints );
pMintsP = ALLOC( int, nMints );
for ( i = 0; i < nMints; i++ )
pMints[i] = i;
Dar_TruthPermute_int( pMints, nMints, pPerms, nVars, pMintsP );
Result = 0;
if ( fReverse )
{
for ( m = 0; m < nMints; m++ )
if ( Truth & (1 << pMintsP[m]) )
Result |= (1 << m);
}
else
{
for ( m = 0; m < nMints; m++ )
if ( Truth & (1 << m) )
Result |= (1 << pMintsP[m]);
}
free( pMints );
free( pMintsP );
return Result;
}
/**Function*************************************************************
Synopsis [Changes the phase of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Dar_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
{
// elementary truth tables
static unsigned Signs[5] = {
0xAAAAAAAA, // 1010 1010 1010 1010 1010 1010 1010 1010
0xCCCCCCCC, // 1010 1010 1010 1010 1010 1010 1010 1010
0xF0F0F0F0, // 1111 0000 1111 0000 1111 0000 1111 0000
0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000
0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000
};
unsigned uTruthRes, uCof0, uCof1;
int nMints, Shift, v;
assert( nVars < 6 );
nMints = (1 << nVars);
uTruthRes = uTruth;
for ( v = 0; v < nVars; v++ )
if ( Polarity & (1 << v) )
{
uCof0 = uTruth & ~Signs[v];
uCof1 = uTruth & Signs[v];
Shift = (1 << v);
uCof0 <<= Shift;
uCof1 >>= Shift;
uTruth = uCof0 | uCof1;
}
return uTruth;
}
/**Function*************************************************************
Synopsis [Computes NPN canonical forms for 4-variable functions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap )
{
unsigned short * uCanons;
unsigned char * uMap;
unsigned uTruth, uPhase, uPerm;
char ** pPerms4, * uPhases, * uPerms;
int nFuncs, nClasses;
int i, k;
nFuncs = (1 << 16);
uCanons = ALLOC( unsigned short, nFuncs );
uPhases = ALLOC( char, nFuncs );
uPerms = ALLOC( char, nFuncs );
uMap = ALLOC( unsigned char, nFuncs );
memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
memset( uPhases, 0, sizeof(char) * nFuncs );
memset( uPerms, 0, sizeof(char) * nFuncs );
memset( uMap, 0, sizeof(unsigned char) * nFuncs );
pPerms4 = Dar_Permutations( 4 );
nClasses = 1;
nFuncs = (1 << 15);
for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ )
{
// skip already assigned
if ( uCanons[uTruth] )
{
assert( uTruth > uCanons[uTruth] );
uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]];
continue;
}
uMap[uTruth] = nClasses++;
for ( i = 0; i < 16; i++ )
{
uPhase = Dar_TruthPolarize( uTruth, i, 4 );
for ( k = 0; k < 24; k++ )
{
uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
if ( uCanons[uPerm] == 0 )
{
uCanons[uPerm] = uTruth;
uPhases[uPerm] = i;
uPerms[uPerm] = k;
uPerm = ~uPerm & 0xFFFF;
uCanons[uPerm] = uTruth;
uPhases[uPerm] = i | 16;
uPerms[uPerm] = k;
}
else
assert( uCanons[uPerm] == uTruth );
}
uPhase = Dar_TruthPolarize( ~uTruth & 0xFFFF, i, 4 );
for ( k = 0; k < 24; k++ )
{
uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
if ( uCanons[uPerm] == 0 )
{
uCanons[uPerm] = uTruth;
uPhases[uPerm] = i;
uPerms[uPerm] = k;
uPerm = ~uPerm & 0xFFFF;
uCanons[uPerm] = uTruth;
uPhases[uPerm] = i | 16;
uPerms[uPerm] = k;
}
else
assert( uCanons[uPerm] == uTruth );
}
}
}
uPhases[(1<<16)-1] = 16;
assert( nClasses == 222 );
free( pPerms4 );
if ( puCanons )
*puCanons = uCanons;
else
free( uCanons );
if ( puPhases )
*puPhases = uPhases;
else
free( uPhases );
if ( puPerms )
*puPerms = uPerms;
else
free( uPerms );
if ( puMap )
*puMap = uMap;
else
free( uMap );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -309,7 +309,7 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_
if ( Kit_GraphIsVar(pGraph) )
return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
// build the AIG nodes corresponding to the AND gates of the graph
//printf( "Building (current number %d):\n", Aig_ManObjIdMax(pAig) );
//printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
Kit_GraphForEachNode( pGraph, pNode, i )
{
pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );

245
src/aig/dar/darScript.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "darInt.h"
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -62,6 +63,128 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
//alias rwsat "st; rw -l; b -l; rw -l; rf -l"
{
Aig_Man_t * pTemp;
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
pParsRwr->fUpdateLevel = 0;
pParsRef->fUpdateLevel = 0;
pParsRwr->fVerbose = fVerbose;
pParsRef->fVerbose = fVerbose;
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
}
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
return pAig;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
//alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
{
Aig_Man_t * pTemp;
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
pParsRwr->fUpdateLevel = fUpdateLevel;
pParsRef->fUpdateLevel = fUpdateLevel;
pParsRwr->fVerbose = fVerbose;
pParsRef->fVerbose = fVerbose;
pAig = Aig_ManDup( pAig, 0 );
// balance
if ( fBalance )
{
// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
// Aig_ManStop( pTemp );
}
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
Aig_ManStop( pTemp );
}
pParsRwr->fUseZeros = 1;
pParsRef->fUseZeros = 1;
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
return pAig;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress2".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
@ -80,6 +203,8 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
pParsRwr->fVerbose = fVerbose;
pParsRef->fVerbose = fVerbose;
pAig = Aig_ManDup( pAig, 0 );
// balance
if ( fBalance )
{
@ -149,53 +274,93 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
Description []
SideEffects [This procedure does not tighten level during restructuring.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
//alias rwsat "st; rw -l; b -l; rw -l; rf -l"
Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
//alias resyn "b; rw; rwz; b; rwz; b"
//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
{
Aig_Man_t * pTemp;
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
Dar_ManDefaultRwrParams( pParsRwr );
Dar_ManDefaultRefParams( pParsRef );
pParsRwr->fUpdateLevel = 0;
pParsRef->fUpdateLevel = 0;
pParsRwr->fVerbose = fVerbose;
pParsRef->fVerbose = fVerbose;
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
// refactor
Dar_ManRefactor( pAig, pParsRef );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
// balance
if ( fBalance )
{
pAig = Dar_ManBalance( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
}
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
pAig = Aig_ManDup( pTemp = pAig, 0 );
Aig_ManStop( pTemp );
return pAig;
Vec_Ptr_t * vAigs;
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, fVerbose);
Vec_PtrPush( vAigs, pAig );
return vAigs;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 );
return vAigs;
}
/**Function*************************************************************
Synopsis [Reproduces script "compress2".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Vec_Ptr_t * vAigs;
int i, clk;
clk = clock();
// vAigs = Dar_ManChoiceSynthesisExt();
vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, fVerbose );
// 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 ( fVerbose )
{
PRT( "Synthesis time", clock() - clk );
}
clk = clock();
pMan = Aig_ManChoicePartitioned( vAigs, 300 );
Vec_PtrForEachEntry( vAigs, pTemp, i )
Aig_ManStop( pTemp );
Vec_PtrFree( vAigs );
if ( fVerbose )
{
PRT( "Choicing time ", clock() - clk );
}
return pMan;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

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

@ -4,6 +4,7 @@ SRC += src/aig/dar/darBalance.c \
src/aig/dar/darData.c \
src/aig/dar/darLib.c \
src/aig/dar/darMan.c \
src/aig/dar/darPrec.c \
src/aig/dar/darRefact.c \
src/aig/dar/darResub.c \
src/aig/dar/darScript.c \

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

@ -1 +0,0 @@
SRC +=

8
src/aig/fra/fra.h
View File

@ -39,6 +39,7 @@ extern "C" {
#include "aig.h"
#include "dar.h"
#include "satSolver.h"
#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -126,6 +127,7 @@ struct Fra_Man_t_
// mapping AIG into FRAIG
int nFramesAll; // the number of timeframes used
Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
int nSizeAlloc; // allocated size of the arrays for timeframe nodes
// equivalence classes
Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes
// simulation info
@ -144,7 +146,7 @@ struct Fra_Man_t_
sint64 nInsLimitGlobal; // resource limit
Vec_Ptr_t ** pMemFanins; // the arrays of fanins for some FRAIG nodes
int * pMemSatNums; // the array of SAT numbers for some FRAIG nodes
int nSizeAlloc; // allocated size of the arrays
int nMemAlloc; // allocated size of the arrays for FRAIG varnums and fanins
Vec_Ptr_t * vTimeouts; // the nodes, for which equivalence checking timed out
// statistics
int nSimRounds;
@ -240,7 +242,7 @@ extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pO
extern void Fra_FraigSweep( Fra_Man_t * pManAig );
extern int Fra_FraigMiterStatus( Aig_Man_t * p );
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
@ -259,7 +261,7 @@ extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int n
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
extern void Fra_ManClean( Fra_Man_t * p );
extern void Fra_ManClean( Fra_Man_t * p, int nNodesMax );
extern Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p );
extern void Fra_ManFinalizeComb( Fra_Man_t * p );
extern void Fra_ManStop( Fra_Man_t * p );

7
src/aig/fra/fraBmc.c
View File

@ -187,8 +187,8 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
p->nPref = nPref;
p->nDepth = nDepth;
p->nFramesAll = nPref + nDepth;
p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
return p;
}
@ -231,7 +231,8 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
int i, k, f;
// start the fraig package
pAigFrames = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * p->nFramesAll );
pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName );
// create PI nodes for the frames
for ( f = 0; f < p->nFramesAll; f++ )
Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );

19
src/aig/fra/fraClass.c
View File

@ -60,8 +60,8 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
p = ALLOC( Fra_Cla_t, 1 );
memset( p, 0, sizeof(Fra_Cla_t) );
p->pAig = pAig;
p->pMemRepr = ALLOC( Aig_Obj_t *, (Aig_ManObjIdMax(pAig) + 1) );
memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pAig) + 1) );
p->pMemRepr = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
p->vClasses = Vec_PtrAlloc( 100 );
p->vClasses1 = Vec_PtrAlloc( 100 );
p->vClassesTemp = Vec_PtrAlloc( 100 );
@ -112,8 +112,8 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
{
Aig_Obj_t * pObj;
int i;
Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 );
memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) );
Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
{
Aig_ManForEachObj( p->pAig, pObj, i )
@ -277,7 +277,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
int i, k, nTableSize, nEntries, nNodes, iEntry;
// allocate the hash table hashing simulation info into nodes
nTableSize = Aig_PrimeCudd( Aig_ManObjIdMax(p->pAig) + 1 );
nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
ppTable = ALLOC( Aig_Obj_t *, nTableSize );
ppNexts = ALLOC( Aig_Obj_t *, nTableSize );
memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
@ -643,8 +643,8 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
// perform combinational simulation
pComb = Fra_SmlSimulateComb( p->pAig, 32 );
// compute the weight of each node in the classes
pWeights = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
memset( pWeights, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
{
pRepr = Fra_ClassObjRepr( pObj );
@ -798,9 +798,10 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
assert( nFramesK > 0 );
// start the fraig package
pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll );
pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
// allocate place for the node mapping
ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 );
ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
// create latches for the first frame
Aig_ManForEachLoSeq( p->pAig, pObj, i )

44
src/aig/fra/fraCore.c
View File

@ -267,7 +267,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
***********************************************************************/
void Fra_FraigSweep( Fra_Man_t * p )
{
ProgressBar * pProgress;
Bar_Progress_t * pProgress;
Aig_Obj_t * pObj, * pObjNew;
int i, k = 0, Pos = 0;
// fraig latch outputs
@ -280,10 +280,10 @@ void Fra_FraigSweep( Fra_Man_t * p )
if ( p->pPars->fLatchCorr )
return;
// fraig internal nodes
pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
Aig_ManForEachNode( p->pManAig, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
Bar_ProgressUpdate( pProgress, i, NULL );
// derive and remember the new fraig node
pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
@ -296,7 +296,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
if ( p->pPars->fUseImps )
Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
}
Extra_ProgressBarStop( pProgress );
Bar_ProgressStop( pProgress );
// try to prove the outputs of the miter
p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
// Fra_MiterStatus( p->pManFraig );
@ -331,8 +331,8 @@ clk = clock();
p->pManFraig = Fra_ManPrepareComb( p );
p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
Fra_SmlSimulate( p, 0 );
if ( p->pPars->fChoicing )
Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
// if ( p->pPars->fChoicing )
// Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) );
// collect initial states
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = Aig_ManNodeNum(pManAig);
@ -346,10 +346,12 @@ clk = clock();
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )
{
int clk2 = clock();
int clk2 = clock();
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( p->pManAig );
Aig_ManCreateChoices( pManAigNew );
pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
Aig_ManTransferRepr( pManAigNew, p->pManAig );
Aig_ManMarkValidChoices( pManAigNew );
Aig_ManStop( p->pManFraig );
p->pManFraig = NULL;
p->timeTrav += clock() - clk2;
@ -359,14 +361,6 @@ p->timeTrav += clock() - clk2;
Aig_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig;
p->pManFraig = NULL;
/*
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( p->pManAig );
// Aig_ManCreateChoices( pManAigNew );
Aig_ManCleanup( pManAigNew );
Aig_ManStop( p->pManFraig );
p->pManFraig = NULL;
*/
}
p->timeTotal = clock() - clk;
// collect final stats
@ -388,16 +382,16 @@ p->timeTotal = clock() - clk;
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig )
Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
{
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
pPars->nBTLimitNode = 1000;
pPars->fVerbose = 0;
pPars->fProve = 0;
pPars->nBTLimitNode = nConfMax;
pPars->fChoicing = 1;
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
pPars->fChoicing = 1;
pPars->fProve = 0;
pPars->fVerbose = 0;
return Fra_FraigPerform( pManAig, pPars );
}
@ -418,11 +412,11 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
pPars->nBTLimitNode = nConfMax;
pPars->fVerbose = 0;
pPars->fProve = 0;
pPars->fChoicing = 0;
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
pPars->fChoicing = 0;
pPars->fProve = 0;
pPars->fVerbose = 0;
pFraig = Fra_FraigPerform( pManAig, pPars );
return pFraig;
}

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

@ -64,8 +64,8 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
{
Aig_Obj_t * pObj;
int i, * pnBits;
pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
memset( pnBits, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
pnBits[i] = Fra_SmlCountOnesOne( p, i );
return pnBits;
@ -325,7 +325,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
int CostMin = AIG_INFINITY, CostMax = 0;
int i, k, Imp, CostRange, clk = clock();
assert( Aig_ManObjIdMax(p->pManAig) + 1 < (1 << 15) );
assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
// normalize both managers
pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );

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

@ -133,7 +133,8 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
// start the fraig package
pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFramesAll );
pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
pManFraig->nRegs = p->pManAig->nRegs;
// create PI nodes for the frames
for ( f = 0; f < p->nFramesAll; f++ )
@ -194,7 +195,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
Aig_ManForEachObj( p, pObj, i )
pObj->pData = pObj;
// iterate and add objects
nNodesOld = Aig_ManObjIdMax(p);
nNodesOld = Aig_ManObjNumMax(p);
pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
for ( f = 0; f < nFrames; f++ )
{
@ -372,11 +373,14 @@ PRT( "Time", clock() - clk );
if ( p->pSat == NULL )
printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
}
// set the pointers to the manager
Aig_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
// prepare solver for fraiging the last timeframe
Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
// transfer PI/LO variable numbers
Aig_ManForEachObj( p->pManFraig, pObj, i )
{
@ -402,12 +406,14 @@ PRT( "Time", clock() - clk );
p->nSatCallsRecent = 0;
p->nSatCallsSkipped = 0;
Fra_FraigSweep( p );
// remove FRAIG and SAT solver
Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
sat_solver_delete( p->pSat ); p->pSat = NULL;
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
// printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
assert( p->vTimeouts == NULL );
if ( p->vTimeouts )
printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
// cleanup
Fra_ManClean( p );
// check if refinement has happened
// p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
if ( p->pCla->fRefinement &&
@ -435,7 +441,7 @@ clk2 = clock();
// Fra_ClassesPrint( p->pCla, 1 );
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( pManAig );
pManAigNew = Aig_ManDupRepr( pManAig, 0 );
// add implications to the manager
if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
Fra_ImpRecordInManager( p, pManAigNew );

4
src/aig/fra/fraLcr.c
View File

@ -509,7 +509,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
Fra_Man_t * pTemp;
Aig_Man_t * pAigPart, * pAigNew = NULL;
Vec_Int_t * vPart;
Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
// Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
int i, nIter, clk = clock(), clk2, clk3;
if ( Aig_ManNodeNum(pAig) == 0 )
{
@ -622,7 +622,7 @@ clk2 = clock();
if ( fReprSelect )
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, NULL );
pAigNew = Aig_ManDupRepr( p->pAig );
pAigNew = Aig_ManDupRepr( p->pAig, 0 );
Aig_ManSeqCleanup( pAigNew );
// Aig_ManCountMergeRegs( pAigNew );
p->timeUpdate += clock() - clk2;

112
src/aig/fra/fraMan.c
View File

@ -42,20 +42,20 @@
void Fra_ParamsDefault( Fra_Par_t * pPars )
{
memset( pPars, 0, sizeof(Fra_Par_t) );
pPars->nSimWords = 32; // the number of words in the simulation info
pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pPars->fPatScores = 0; // enables simulation pattern scoring
pPars->MaxScore = 25; // max score after which resimulation is used
pPars->fDoSparse = 1; // skips sparse functions
// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped
// pPars->dActConeBumpMax = 5.0; // the largest bump of activity
pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode = 100; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output
pPars->nFramesK = 0; // the number of timeframes to unroll
pPars->fConeBias = 1;
pPars->fRewrite = 0;
pPars->nSimWords = 32; // the number of words in the simulation info
pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pPars->fPatScores = 0; // enables simulation pattern scoring
pPars->MaxScore = 25; // max score after which resimulation is used
pPars->fDoSparse = 1; // skips sparse functions
// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped
// pPars->dActConeBumpMax = 5.0; // the largest bump of activity
pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode = 100; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output
pPars->nFramesK = 0; // the number of timeframes to unroll
pPars->fConeBias = 1;
pPars->fRewrite = 0;
}
/**Function*************************************************************
@ -72,20 +72,20 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
{
memset( pPars, 0, sizeof(Fra_Par_t) );
pPars->nSimWords = 1; // the number of words in the simulation info
pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pPars->fPatScores = 0; // enables simulation pattern scoring
pPars->MaxScore = 25; // max score after which resimulation is used
pPars->fDoSparse = 1; // skips sparse functions
pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode =10000000; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output
pPars->nFramesK = 1; // the number of timeframes to unroll
pPars->fConeBias = 0;
pPars->fRewrite = 0;
pPars->fLatchCorr = 0;
}
pPars->nSimWords = 1; // the number of words in the simulation info
pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pPars->fPatScores = 0; // enables simulation pattern scoring
pPars->MaxScore = 25; // max score after which resimulation is used
pPars->fDoSparse = 1; // skips sparse functions
pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode = 10000000; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output
pPars->nFramesK = 1; // the number of timeframes to unroll
pPars->fConeBias = 0;
pPars->fRewrite = 0;
pPars->fLatchCorr = 0;
}
/**Function*************************************************************
@ -108,7 +108,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
memset( p, 0, sizeof(Fra_Man_t) );
p->pPars = pPars;
p->pManAig = pManAig;
p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
p->nFramesAll = pPars->nFramesK + 1;
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
@ -119,10 +119,6 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
// allocate other members
p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFramesAll + 10000 );
memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFramesAll + 10000 );
p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFramesAll + 10000 );
memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFramesAll + 10000 );
// set random number generator
srand( 0xABCABC );
// set the pointer to the manager
@ -142,24 +138,24 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
SeeAlso []
***********************************************************************/
void Fra_ManClean( Fra_Man_t * p )
void Fra_ManClean( Fra_Man_t * p, int nNodesMax )
{
int i, Limit;
Limit = Aig_ManObjIdMax(p->pManFraig) + 1;
for ( i = 0; i < Limit; i++ )
int i;
// remove old arrays
for ( i = 0; i < p->nMemAlloc; i++ )
if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
Vec_PtrFree( p->pMemFanins[i] );
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * Limit );
memset( p->pMemSatNums, 0, sizeof(int) * Limit );
Aig_ManStop( p->pManFraig );
p->pManFraig = NULL;
sat_solver_delete( p->pSat );
p->pSat = NULL;
// realloc for the new size
if ( p->nMemAlloc < nNodesMax )
{
int nMemAllocNew = nNodesMax + 5000;
p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew );
p->nMemAlloc = nMemAllocNew;
}
// prepare for the new run
memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
}
/**Function*************************************************************
@ -180,7 +176,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
int i;
assert( p->pManFraig == NULL );
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
pManFraig->nRegs = p->pManAig->nRegs;
pManFraig->nAsserts = p->pManAig->nAsserts;
// set the pointers to the available fraig nodes
@ -190,6 +187,12 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
// set the pointers to the manager
Aig_ManForEachObj( pManFraig, pObj, i )
pObj->pData = p;
// allocate memory for mapping FRAIG nodes into SAT numbers and fanins
p->nMemAlloc = p->nSizeAlloc;
p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc );
memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
p->pMemSatNums = ALLOC( int, p->nMemAlloc );
memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
// make sure the satisfying assignment is node assigned
assert( pManFraig->pData == NULL );
return pManFraig;
@ -231,7 +234,6 @@ void Fra_ManFinalizeComb( Fra_Man_t * p )
***********************************************************************/
void Fra_ManStop( Fra_Man_t * p )
{
int i;
if ( p->pPars->fVerbose )
Fra_ManPrint( p );
// save mapping from original nodes into FRAIG nodes
@ -242,9 +244,7 @@ void Fra_ManStop( Fra_Man_t * p )
p->pManAig->pObjCopies = p->pMemFraig;
p->pMemFraig = NULL;
}
for ( i = 0; i < p->nSizeAlloc; i++ )
if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
Vec_PtrFree( p->pMemFanins[i] );
Fra_ManClean( p, 0 );
if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
if ( p->pSat ) sat_solver_delete( p->pSat );
@ -271,14 +271,14 @@ void Fra_ManStop( Fra_Man_t * p )
***********************************************************************/
void Fra_ManPrint( Fra_Man_t * p )
{
double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n",
p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg,
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
PRT( "AIG simulation ", p->pSml->timeSim );
PRT( "AIG traversal ", p->timeTrav );

8
src/aig/fra/fraPart.c
View File

@ -41,7 +41,7 @@
***********************************************************************/
void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
{
ProgressBar * pProgress;
Bar_Progress_t * pProgress;
Vec_Vec_t * vSupps, * vSuppsIn;
Vec_Ptr_t * vSuppsNew;
Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
@ -86,10 +86,10 @@ clk = clock();
vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
vOverNew = Vec_IntAlloc( Aig_ManPoNum(p) );
vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
pProgress = Extra_ProgressBarStart( stdout, Aig_ManPoNum(p) );
pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
Aig_ManForEachPo( p, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
Bar_ProgressUpdate( pProgress, i, NULL );
// get old supports
vSup = Vec_VecEntry( vSupps, i );
if ( Vec_IntSize(vSup) < 2 )
@ -152,7 +152,7 @@ clk = clock();
printf( "\n" );
*/
}
Extra_ProgressBarStop( pProgress );
Bar_ProgressStop( pProgress );
PRT( "Scanning", clock() - clk );
// print cumulative statistics

1
src/aig/fra/fraSat.c
View File

@ -18,6 +18,7 @@
***********************************************************************/
#include <math.h>
#include "fra.h"
////////////////////////////////////////////////////////////////////////

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

@ -19,6 +19,7 @@
***********************************************************************/
#include "fra.h"
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -100,7 +101,7 @@ PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, int fVeryVerbose )
int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
@ -116,7 +117,9 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose,
// perform sequential cleanup
clk = clock();
if ( pNew->nRegs )
pNew = Aig_ManReduceLaches( pNew, 0 );
if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );
if ( fVerbose )
{
@ -126,7 +129,7 @@ PRT( "Time", clock() - clk );
}
// perform forward retiming
if ( fRetimeFirst )
if ( fRetimeFirst && pNew->nRegs )
{
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@ -141,6 +144,8 @@ PRT( "Time", clock() - clk );
// run latch correspondence
clk = clock();
if ( pNew->nRegs )
{
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
@ -151,6 +156,7 @@ clk = clock();
nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
}
// perform fraiging
clk = clock();
@ -166,7 +172,7 @@ PRT( "Time", clock() - clk );
// perform seq sweeping while increasing the number of frames
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue == -1 )
for ( nFrames = 1; ; nFrames *= 2 )
for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
{
clk = clock();
pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
@ -203,19 +209,35 @@ clk = clock();
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );
}
// get the miter status
RetValue = Fra_FraigMiterStatus( pNew );
Aig_ManStop( pNew );
// report the miter
if ( RetValue == 1 )
{
printf( "Networks are equivalent. " );
PRT( "Time", clock() - clkTotal );
}
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT. " );
PRT( "Time", clock() - clkTotal );
}
else
{
static int Counter = 1;
char pFileName[1000];
printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal );
sprintf( pFileName, "sm%03d.aig", Counter++ );
Ioa_WriteAiger( pNew, pFileName, 0 );
printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
}
Aig_ManStop( pNew );
return RetValue;
}

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

@ -703,7 +703,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
{
Fra_Sml_t * p;
p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame );
p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
p->pAig = pAig;
p->nPref = nPref;

20
src/aig/hop/hop.h
View File

@ -121,6 +121,8 @@ static inline int Hop_TruthWordNum( int nVars ) { return nVars
static inline int Hop_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Hop_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Hop_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline int Hop_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
static inline int Hop_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
static inline Hop_Obj_t * Hop_Regular( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) & ~01); }
static inline Hop_Obj_t * Hop_Not( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) ^ 01); }
@ -268,12 +270,12 @@ static inline void Hop_ManRecycleMemory( Hop_Man_t * p, Hop_Obj_t * pEntry )
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== aigBalance.c ========================================================*/
/*=== hopBalance.c ========================================================*/
extern Hop_Man_t * Hop_ManBalance( Hop_Man_t * p, int fUpdateLevel );
extern Hop_Obj_t * Hop_NodeBalanceBuildSuper( Hop_Man_t * p, Vec_Ptr_t * vSuper, Hop_Type_t Type, int fUpdateLevel );
/*=== aigCheck.c ========================================================*/
/*=== hopCheck.c ========================================================*/
extern int Hop_ManCheck( Hop_Man_t * p );
/*=== aigDfs.c ==========================================================*/
/*=== hopDfs.c ==========================================================*/
extern Vec_Ptr_t * Hop_ManDfs( Hop_Man_t * p );
extern Vec_Ptr_t * Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode );
extern int Hop_ManCountLevels( Hop_Man_t * p );
@ -282,16 +284,16 @@ extern int Hop_DagSize( Hop_Obj_t * pObj );
extern void Hop_ConeUnmark_rec( Hop_Obj_t * pObj );
extern Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars );
extern Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar );
/*=== aigMan.c ==========================================================*/
/*=== hopMan.c ==========================================================*/
extern Hop_Man_t * Hop_ManStart();
extern Hop_Man_t * Hop_ManDup( Hop_Man_t * p );
extern void Hop_ManStop( Hop_Man_t * p );
extern int Hop_ManCleanup( Hop_Man_t * p );
extern void Hop_ManPrintStats( Hop_Man_t * p );
/*=== aigMem.c ==========================================================*/
/*=== hopMem.c ==========================================================*/
extern void Hop_ManStartMemory( Hop_Man_t * p );
extern void Hop_ManStopMemory( Hop_Man_t * p );
/*=== aigObj.c ==========================================================*/
/*=== hopObj.c ==========================================================*/
extern Hop_Obj_t * Hop_ObjCreatePi( Hop_Man_t * p );
extern Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver );
extern Hop_Obj_t * Hop_ObjCreate( Hop_Man_t * p, Hop_Obj_t * pGhost );
@ -301,7 +303,7 @@ extern void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj );
extern void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj );
extern Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj );
extern void Hop_ObjCreateChoice( Hop_Obj_t * pOld, Hop_Obj_t * pNew );
/*=== aigOper.c =========================================================*/
/*=== hopOper.c =========================================================*/
extern Hop_Obj_t * Hop_IthVar( Hop_Man_t * p, int i );
extern Hop_Obj_t * Hop_Oper( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type );
extern Hop_Obj_t * Hop_And( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 );
@ -313,13 +315,13 @@ extern Hop_Obj_t * Hop_Miter( Hop_Man_t * p, Vec_Ptr_t * vPairs );
extern Hop_Obj_t * Hop_CreateAnd( Hop_Man_t * p, int nVars );
extern Hop_Obj_t * Hop_CreateOr( Hop_Man_t * p, int nVars );
extern Hop_Obj_t * Hop_CreateExor( Hop_Man_t * p, int nVars );
/*=== aigTable.c ========================================================*/
/*=== hopTable.c ========================================================*/
extern Hop_Obj_t * Hop_TableLookup( Hop_Man_t * p, Hop_Obj_t * pGhost );
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 );
/*=== aigUtil.c =========================================================*/
/*=== hopUtil.c =========================================================*/
extern void Hop_ManIncrementTravId( Hop_Man_t * p );
extern void Hop_ManCleanData( Hop_Man_t * p );
extern void Hop_ObjCleanData_rec( Hop_Obj_t * pObj );

4
src/aig/hop/hopTable.c
View File

@ -28,8 +28,8 @@
static unsigned long Hop_Hash( Hop_Obj_t * pObj, int TableSize )
{
unsigned long Key = Hop_ObjIsExor(pObj) * 1699;
Key ^= (long)Hop_ObjFanin0(pObj) * 7937;
Key ^= (long)Hop_ObjFanin1(pObj) * 2971;
Key ^= Hop_ObjFanin0(pObj)->Id * 7937;
Key ^= Hop_ObjFanin1(pObj)->Id * 2971;
Key ^= Hop_ObjFaninC0(pObj) * 911;
Key ^= Hop_ObjFaninC1(pObj) * 353;
return Key % TableSize;

2
src/aig/hop/hopUtil.c
View File

@ -523,7 +523,7 @@ void Hop_ManDumpBlif( Hop_Man_t * p, char * pFileName )
pObj->pData = (void *)Counter++;
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pData = (void *)Counter++;
nDigits = Extra_Base10Log( Counter );
nDigits = Hop_Base10Log( Counter );
// write the file
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# BLIF file written by procedure Hop_ManDumpBlif() in ABC\n" );

80
src/aig/ioa/ioa.h Normal file
View File

@ -0,0 +1,80 @@
/**CFile****************************************************************
FileName [ioa.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [AIG package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: ioa.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __IOA_H__
#define __IOA_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "bar.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== ioaReadAig.c ========================================================*/
extern Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck );
/*=== ioaWriteAig.c =======================================================*/
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols );
/*=== ioaUtil.c =======================================================*/
extern int Ioa_FileSize( char * pFileName );
extern char * Ioa_FileNameGeneric( char * FileName );
extern char * Ioa_TimeStamp();
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

312
src/aig/ioa/ioaReadAig.c Normal file
View File

@ -0,0 +1,312 @@
/**CFile****************************************************************
FileName [ioaReadAiger.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to read binary AIGER format developed by
Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - December 16, 2006.]
Revision [$Id: ioaReadAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
unsigned Ioa_ReadAigerDecode( char ** ppPos );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Reads the AIG in the binary AIGER format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
{
Bar_Progress_t * pProgress;
FILE * pFile;
Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
Aig_Obj_t * pObj, * pNode0, * pNode1;
Aig_Man_t * pManNew;
int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType;
unsigned uLit0, uLit1, uLit;
// read the file into the buffer
nFileSize = Ioa_FileSize( pFileName );
pFile = fopen( pFileName, "rb" );
pContents = ALLOC( char, nFileSize );
fread( pContents, nFileSize, 1, pFile );
fclose( pFile );
// check if the input file format is correct
if ( strncmp(pContents, "aig", 3) != 0 )
{
fprintf( stdout, "Wrong input file format.\n" );
return NULL;
}
// read the file type
pCur = pContents; while ( *pCur++ != ' ' );
// read the number of objects
nTotal = atoi( pCur ); while ( *pCur++ != ' ' );
// read the number of inputs
nInputs = atoi( pCur ); while ( *pCur++ != ' ' );
// read the number of latches
nLatches = atoi( pCur ); while ( *pCur++ != ' ' );
// read the number of outputs
nOutputs = atoi( pCur ); while ( *pCur++ != ' ' );
// read the number of nodes
nAnds = atoi( pCur ); while ( *pCur++ != '\n' );
// check the parameters
if ( nTotal != nInputs + nLatches + nAnds )
{
fprintf( stdout, "The paramters are wrong.\n" );
return NULL;
}
// allocate the empty AIG
pManNew = Aig_ManStart( nAnds );
pName = Ioa_FileNameGeneric( pFileName );
pManNew->pName = Aig_UtilStrsav( pName );
// pManNew->pSpec = Ioa_UtilStrsav( pFileName );
free( pName );
// prepare the array of nodes
vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
Vec_PtrPush( vNodes, Aig_ManConst0(pManNew) );
// create the PIs
for ( i = 0; i < nInputs + nLatches; i++ )
{
pObj = Aig_ObjCreatePi(pManNew);
Vec_PtrPush( vNodes, pObj );
}
/*
// create the POs
for ( i = 0; i < nOutputs + nLatches; i++ )
{
pObj = Aig_ObjCreatePo(pManNew);
}
*/
// create the latches
pManNew->nRegs = nLatches;
/*
nDigits = Ioa_Base10Log( nLatches );
for ( i = 0; i < nLatches; i++ )
{
pObj = Aig_ObjCreateLatch(pManNew);
Aig_LatchSetInit0( pObj );
pNode0 = Aig_ObjCreateBi(pManNew);
pNode1 = Aig_ObjCreateBo(pManNew);
Aig_ObjAddFanin( pObj, pNode0 );
Aig_ObjAddFanin( pNode1, pObj );
Vec_PtrPush( vNodes, pNode1 );
// assign names to latch and its input
// Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL );
// printf( "Creating latch %s with input %d and output %d.\n", Aig_ObjName(pObj), pNode0->Id, pNode1->Id );
}
*/
// remember the beginning of latch/PO literals
pDrivers = pCur;
// scroll to the beginning of the binary data
for ( i = 0; i < nLatches + nOutputs; )
if ( *pCur++ == '\n' )
i++;
// create the AND gates
pProgress = Bar_ProgressStart( stdout, nAnds );
for ( i = 0; i < nAnds; i++ )
{
Bar_ProgressUpdate( pProgress, i, NULL );
uLit = ((i + 1 + nInputs + nLatches) << 1);
uLit1 = uLit - Ioa_ReadAigerDecode( &pCur );
uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur );
// assert( uLit1 > uLit0 );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
pNode1 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) );
}
Bar_ProgressStop( pProgress );
// remember the place where symbols begin
pSymbols = pCur;
// read the latch driver literals
vDrivers = Vec_PtrAlloc( nLatches + nOutputs );
pCur = pDrivers;
// Aig_ManForEachLatchInput( pManNew, pObj, i )
for ( i = 0; i < nLatches; i++ )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
// Aig_ObjAddFanin( pObj, pNode0 );
Vec_PtrPush( vDrivers, pNode0 );
}
// read the PO driver literals
// Aig_ManForEachPo( pManNew, pObj, i )
for ( i = 0; i < nOutputs; i++ )
{
uLit0 = atoi( pCur ); while ( *pCur++ != '\n' );
pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
// Aig_ObjAddFanin( pObj, pNode0 );
Vec_PtrPush( vDrivers, pNode0 );
}
// create the POs
for ( i = 0; i < nOutputs; i++ )
Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) );
for ( i = 0; i < nLatches; i++ )
Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, i) );
Vec_PtrFree( vDrivers );
/*
// read the names if present
pCur = pSymbols;
if ( *pCur != 'c' )
{
int Counter = 0;
while ( pCur < pContents + nFileSize && *pCur != 'c' )
{
// get the terminal type
pType = pCur;
if ( *pCur == 'i' )
vTerms = pManNew->vPis;
else if ( *pCur == 'l' )
vTerms = pManNew->vBoxes;
else if ( *pCur == 'o' )
vTerms = pManNew->vPos;
else
{
fprintf( stdout, "Wrong terminal type.\n" );
return NULL;
}
// get the terminal number
iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' );
// get the node
if ( iTerm >= Vec_PtrSize(vTerms) )
{
fprintf( stdout, "The number of terminal is out of bound.\n" );
return NULL;
}
pObj = Vec_PtrEntry( vTerms, iTerm );
if ( *pType == 'l' )
pObj = Aig_ObjFanout0(pObj);
// assign the name
pName = pCur; while ( *pCur++ != '\n' );
// assign this name
*(pCur-1) = 0;
Aig_ObjAssignName( pObj, pName, NULL );
if ( *pType == 'l' )
{
Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
}
// mark the node as named
pObj->pCopy = (Aig_Obj_t *)Aig_ObjName(pObj);
}
// assign the remaining names
Aig_ManForEachPi( pManNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
Counter++;
}
Aig_ManForEachLatchOutput( pManNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" );
Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" );
Counter++;
}
Aig_ManForEachPo( pManNew, pObj, i )
{
if ( pObj->pCopy ) continue;
Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL );
Counter++;
}
if ( Counter )
printf( "Ioa_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter );
}
else
{
// printf( "Ioa_ReadAiger(): I/O/register names are not given. Generating short names.\n" );
Aig_ManShortNames( pManNew );
}
*/
// skipping the comments
free( pContents );
Vec_PtrFree( vNodes );
// remove the extra nodes
Aig_ManCleanup( pManNew );
// check the result
if ( fCheck && !Aig_ManCheck( pManNew ) )
{
printf( "Ioa_ReadAiger: The network check has failed.\n" );
Aig_ManStop( pManNew );
return NULL;
}
return pManNew;
}
/**Function*************************************************************
Synopsis [Extracts one unsigned AIG edge from the input buffer.]
Description [This procedure is a slightly modified version of Armin Biere's
procedure "unsigned decode (FILE * file)". ]
SideEffects [Updates the current reading position.]
SeeAlso []
***********************************************************************/
unsigned Ioa_ReadAigerDecode( char ** ppPos )
{
unsigned x = 0, i = 0;
unsigned char ch;
// while ((ch = getnoneofch (file)) & 0x80)
while ((ch = *(*ppPos)++) & 0x80)
x |= (ch & 0x7f) << (7 * i++);
return x | (ch << (7 * i));
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

117
src/aig/ioa/ioaUtil.c Normal file
View File

@ -0,0 +1,117 @@
/**CFile****************************************************************
FileName [ioaUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to read binary AIGER format developed by
Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - December 16, 2006.]
Revision [$Id: ioaUtil.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the file size.]
Description [The file should be closed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ioa_FileSize( char * pFileName )
{
FILE * pFile;
int nFileSize;
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
printf( "Ioa_FileSize(): The file is unavailable (absent or open).\n" );
return 0;
}
fseek( pFile, 0, SEEK_END );
nFileSize = ftell( pFile );
fclose( pFile );
return nFileSize;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Ioa_FileNameGeneric( char * FileName )
{
char * pDot;
char * pUnd;
char * pRes;
// find the generic name of the file
pRes = Aig_UtilStrsav( FileName );
// find the pointer to the "." symbol in the file name
// pUnd = strstr( FileName, "_" );
pUnd = NULL;
pDot = strstr( FileName, "." );
if ( pUnd )
pRes[pUnd - FileName] = 0;
else if ( pDot )
pRes[pDot - FileName] = 0;
return pRes;
}
/**Function*************************************************************
Synopsis [Returns the time stamp.]
Description [The file should be closed.]
SideEffects []
SeeAlso []
***********************************************************************/
char * Ioa_TimeStamp()
{
static char Buffer[100];
char * TimeStamp;
time_t ltime;
// get the current time
time( &ltime );
TimeStamp = asctime( localtime( &ltime ) );
TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
strcpy( Buffer, TimeStamp );
return Buffer;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

291
src/aig/ioa/ioaWriteAig.c Normal file
View File

@ -0,0 +1,291 @@
/**CFile****************************************************************
FileName [ioaWriteAiger.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Command processing package.]
Synopsis [Procedures to write binary AIGER format developed by
Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - December 16, 2006.]
Revision [$Id: ioaWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
***********************************************************************/
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*
The following is taken from the AIGER format description,
which can be found at http://fmv.jku.at/aiger
*/
/*
The AIGER And-Inverter Graph (AIG) Format Version 20061129
----------------------------------------------------------
Armin Biere, Johannes Kepler University, 2006
This report describes the AIG file format as used by the AIGER library.
The purpose of this report is not only to motivate and document the
format, but also to allow independent implementations of writers and
readers by giving precise and unambiguous definitions.
...
Introduction
The name AIGER contains as one part the acronym AIG of And-Inverter
Graphs and also if pronounced in German sounds like the name of the
'Eiger', a mountain in the Swiss alps. This choice should emphasize the
origin of this format. It was first openly discussed at the Alpine
Verification Meeting 2006 in Ascona as a way to provide a simple, compact
file format for a model checking competition affiliated to CAV 2007.
...
Binary Format Definition
The binary format is semantically a subset of the ASCII format with a
slightly different syntax. The binary format may need to reencode
literals, but translating a file in binary format into ASCII format and
then back in to binary format will result in the same file.
The main differences of the binary format to the ASCII format are as
follows. After the header the list of input literals and all the
current state literals of a latch can be omitted. Furthermore the
definitions of the AND gates are binary encoded. However, the symbol
table and the comment section are as in the ASCII format.
The header of an AIGER file in binary format has 'aig' as format
identifier, but otherwise is identical to the ASCII header. The standard
file extension for the binary format is therefore '.aig'.
A header for the binary format is still in ASCII encoding:
aig M I L O A
Constants, variables and literals are handled in the same way as in the
ASCII format. The first simplifying restriction is on the variable
indices of inputs and latches. The variable indices of inputs come first,
followed by the pseudo-primary inputs of the latches and then the variable
indices of all LHS of AND gates:
input variable indices 1, 2, ... , I
latch variable indices I+1, I+2, ... , (I+L)
AND variable indices I+L+1, I+L+2, ... , (I+L+A) == M
The corresponding unsigned literals are
input literals 2, 4, ... , 2*I
latch literals 2*I+2, 2*I+4, ... , 2*(I+L)
AND literals 2*(I+L)+2, 2*(I+L)+4, ... , 2*(I+L+A) == 2*M
All literals have to be defined, and therefore 'M = I + L + A'. With this
restriction it becomes possible that the inputs and the current state
literals of the latches do not have to be listed explicitly. Therefore,
after the header only the list of 'L' next state literals follows, one per
latch on a single line, and then the 'O' outputs, again one per line.
In the binary format we assume that the AND gates are ordered and respect
the child parent relation. AND gates with smaller literals on the LHS
come first. Therefore we can assume that the literals on the right-hand
side of a definition of an AND gate are smaller than the LHS literal.
Furthermore we can sort the literals on the RHS, such that the larger
literal comes first. A definition thus consists of three literals
lhs rhs0 rhs1
with 'lhs' even and 'lhs > rhs0 >= rhs1'. Also the variable indices are
pairwise different to avoid combinational self loops. Since the LHS
indices of the definitions are all consecutive (as even integers),
the binary format does not have to keep 'lhs'. In addition, we can use
the order restriction and only write the differences 'delta0' and 'delta1'
instead of 'rhs0' and 'rhs1', with
delta0 = lhs - rhs0, delta1 = rhs0 - rhs1
The differences will all be strictly positive, and in practice often very
small. We can take advantage of this fact by the simple little-endian
encoding of unsigned integers of the next section. After the binary delta
encoding of the RHSs of all AND gates, the optional symbol table and
optional comment section start in the same format as in the ASCII case.
...
*/
static unsigned Ioa_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; }
static unsigned Ioa_ObjAigerNum( Aig_Obj_t * pObj ) { return (unsigned)pObj->pData; }
static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->pData = (void *)Num; }
int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Writes the AIG in the binary AIGER format.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols )
{
Bar_Progress_t * pProgress;
FILE * pFile;
Aig_Obj_t * pObj, * pDriver;
int i, nNodes, Pos, nBufferSize;
unsigned char * pBuffer;
unsigned uLit0, uLit1, uLit;
// assert( Aig_ManIsStrash(pMan) );
// start the output stream
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName );
return;
}
/*
Aig_ManForEachLatch( pMan, pObj, i )
if ( !Aig_LatchIsInit0(pObj) )
{
fprintf( stdout, "Ioa_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
return;
}
*/
// set the node numbers to be used in the output file
nNodes = 0;
Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ );
Aig_ManForEachPi( pMan, pObj, i )
Ioa_ObjSetAigerNum( pObj, nNodes++ );
Aig_ManForEachNode( pMan, pObj, i )
Ioa_ObjSetAigerNum( pObj, nNodes++ );
// write the header "M I L O A" where M = I + L + A
fprintf( pFile, "aig %u %u %u %u %u\n",
Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan),
Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
Aig_ManRegNum(pMan),
Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
Aig_ManNodeNum(pMan) );
// if the driver node is a constant, we need to complement the literal below
// because, in the AIGER format, literal 0/1 is represented as number 0/1
// while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
// write latch drivers
Aig_ManForEachLiSeq( pMan, pObj, i )
{
pDriver = Aig_ObjFanin0(pObj);
fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
}
// write PO drivers
Aig_ManForEachPoSeq( pMan, pObj, i )
{
pDriver = Aig_ObjFanin0(pObj);
fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) );
}
// write the nodes into the buffer
Pos = 0;
nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge
pBuffer = ALLOC( char, nBufferSize );
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) );
Aig_ManForEachNode( pMan, pObj, i )
{
Bar_ProgressUpdate( pProgress, i, NULL );
uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 );
uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) );
uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) );
assert( uLit0 < uLit1 );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 );
Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
if ( Pos > nBufferSize - 10 )
{
printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
fclose( pFile );
return;
}
}
assert( Pos < nBufferSize );
Bar_ProgressStop( pProgress );
// write the buffer
fwrite( pBuffer, 1, Pos, pFile );
free( pBuffer );
/*
// write the symbol table
if ( fWriteSymbols )
{
// write PIs
Aig_ManForEachPi( pMan, pObj, i )
fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) );
// write latches
Aig_ManForEachLatch( pMan, pObj, i )
fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) );
// write POs
Aig_ManForEachPo( pMan, pObj, i )
fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) );
}
*/
// write the comment
fprintf( pFile, "c\n" );
fprintf( pFile, "%s\n", pMan->pName );
fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() );
fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Adds one unsigned AIG edge to the output buffer.]
Description [This procedure is a slightly modified version of Armin Biere's
procedure "void encode (FILE * file, unsigned x)" ]
SideEffects [Returns the current writing position.]
SeeAlso []
***********************************************************************/
int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x )
{
unsigned char ch;
while (x & ~0x7f)
{
ch = (x & 0x7f) | 0x80;
// putc (ch, file);
pBuffer[Pos++] = ch;
x >>= 7;
}
ch = x;
// putc (ch, file);
pBuffer[Pos++] = ch;
return Pos;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

3
src/aig/ioa/module.make Normal file
View File

@ -0,0 +1,3 @@
SRC += src/aig/ioa/ioaReadAig.c \
src/aig/ioa/ioaWriteAig.c \
src/aig/ioa/ioaUtil.c

1
src/aig/ivy/ivy.h
View File

@ -30,6 +30,7 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include "extra.h"
#include "vec.h"
////////////////////////////////////////////////////////////////////////

6
src/aig/kit/kit.h
View File

@ -35,6 +35,7 @@ extern "C" {
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "extra.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -488,7 +489,7 @@ extern Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nD
extern void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
extern void Kit_DsdGetSupports( Kit_DsdNtk_t * p );
extern unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p );
extern Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p );
extern Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
extern void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] );
@ -510,6 +511,9 @@ extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph );
extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf );
/*=== kitHop.c ==========================================================*/
//extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
//extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
//extern Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
/*=== kitIsop.c ==========================================================*/
extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
/*=== kitSop.c ==========================================================*/

250
src/aig/kit/kitDsd.c
View File

@ -319,7 +319,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
{
Kit_DsdObj_t * pObj;
unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
unsigned i, m, iLit, nMints, fCompl, fPartial = 0;
unsigned i, m, iLit, nMints, fCompl, nPartial = 0;
// get the node with this ID
pObj = Kit_DsdNtkObj( pNtk, Id );
@ -364,7 +364,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
else
{
pTruthFans[i] = NULL;
fPartial = 1;
nPartial = 1;
}
}
else
@ -401,7 +401,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
}
assert( pObj->Type == KIT_DSD_PRIME );
if ( uSupp && fPartial )
if ( uSupp && nPartial )
{
// find the only non-empty component
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
@ -461,6 +461,169 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
return pTruthRes;
}
/**Function*************************************************************
Synopsis [Derives the truth table of the DSD node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp, int iVar, unsigned * pTruthDec )
{
Kit_DsdObj_t * pObj;
unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
unsigned i, m, iLit, nMints, fCompl, uSuppCur, uSuppFan, nPartial;
int pfBoundSet[16];
assert( uSupp > 0 );
// get the node with this ID
pObj = Kit_DsdNtkObj( pNtk, Id );
pTruthRes = Vec_PtrEntry( p->vTtNodes, Id );
if ( pObj == NULL )
{
assert( Id < pNtk->nVars );
return pTruthRes;
}
assert( pObj->Type != KIT_DSD_CONST1 );
assert( pObj->Type != KIT_DSD_VAR );
// count the number of intersecting fanins
// collect the total support of the intersecting fanins
nPartial = 0;
uSuppFan = 0;
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{
uSuppCur = Kit_DsdLitSupport(pNtk, iLit);
if ( uSupp & uSuppCur )
{
nPartial++;
uSuppFan |= uSuppCur;
}
}
// if there is no intersection, or full intersection, use simple procedure
if ( nPartial == 0 || nPartial == pObj->nFans )
return Kit_DsdTruthComputeNode_rec( p, pNtk, Id, 0 );
// if support of the component includes some other variables
// we need to continue constructing it as usual by the two-function procedure
if ( uSuppFan != (uSuppFan & uSupp) )
{
assert( nPartial == 1 );
// return Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Id, uSupp, iVar, pTruthDec );
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{
if ( uSupp & Kit_DsdLitSupport(pNtk, iLit) )
pTruthFans[i] = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp, iVar, pTruthDec );
else
pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
}
// create composition/decomposition functions
if ( pObj->Type == KIT_DSD_AND )
{
Kit_TruthFill( pTruthRes, pNtk->nVars );
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
return pTruthRes;
}
if ( pObj->Type == KIT_DSD_XOR )
{
Kit_TruthClear( pTruthRes, pNtk->nVars );
fCompl = 0;
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{
fCompl ^= Kit_DsdLitIsCompl(iLit);
Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
}
if ( fCompl )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
return pTruthRes;
}
assert( pObj->Type == KIT_DSD_PRIME );
}
else
{
assert( uSuppFan == (uSuppFan & uSupp) );
assert( nPartial < pObj->nFans );
// the support of the insecting component(s) is contained in the bound-set
// and yet there are components that are not contained in the bound set
// solve the fanins and collect info, which components belong to the bound set
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{
pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 );
pfBoundSet[i] = (int)((uSupp & Kit_DsdLitSupport(pNtk, iLit)) > 0);
}
// create composition/decomposition functions
if ( pObj->Type == KIT_DSD_AND )
{
Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
Kit_TruthFill( pTruthDec, pNtk->nVars );
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
if ( pfBoundSet[i] )
Kit_TruthAndPhase( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
else
Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
return pTruthRes;
}
if ( pObj->Type == KIT_DSD_XOR )
{
Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
Kit_TruthClear( pTruthDec, pNtk->nVars );
fCompl = 0;
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{
fCompl ^= Kit_DsdLitIsCompl(iLit);
if ( pfBoundSet[i] )
Kit_TruthXor( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars );
else
Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
}
if ( fCompl )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
return pTruthRes;
}
assert( pObj->Type == KIT_DSD_PRIME );
assert( nPartial == 1 );
// find the only non-empty component
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
if ( pfBoundSet[i] )
break;
assert( i < pObj->nFans );
// save this component as the decomposed function
Kit_TruthCopy( pTruthDec, pTruthFans[i], pNtk->nVars );
// set the corresponding component to be the new variable
Kit_TruthIthVar( pTruthFans[i], pNtk->nVars, iVar );
}
// get the truth table of the prime node
pTruthPrime = Kit_DsdObjTruth( pObj );
// get storage for the temporary minterm
pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes);
// go through the minterms
nMints = (1 << pObj->nFans);
Kit_TruthClear( pTruthRes, pNtk->nVars );
for ( m = 0; m < nMints; m++ )
{
if ( !Kit_TruthHasBit(pTruthPrime, m) )
continue;
Kit_TruthFill( pTruthMint, pNtk->nVars );
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
}
return pTruthRes;
}
/**Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
@ -472,22 +635,37 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
SeeAlso []
***********************************************************************/
void Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar )
unsigned * Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthDec )
{
unsigned * pTruthRes;
unsigned * pTruthRes, uSuppAll;
int i;
// if support is specified, request that supports are available
if ( uSupp )
Kit_DsdGetSupports( pNtk );
// assign elementary truth tables
assert( uSupp > 0 );
assert( pNtk->nVars <= p->nVars );
// compute support of all nodes
uSuppAll = Kit_DsdGetSupports( pNtk );
// consider special case - there is no overlap
if ( (uSupp & uSuppAll) == 0 )
{
Kit_TruthClear( pTruthDec, pNtk->nVars );
return Kit_DsdTruthCompute( p, pNtk, 0 );
}
// consider special case - support is fully contained
if ( (uSupp & uSuppAll) == uSuppAll )
{
pTruthRes = Kit_DsdTruthCompute( p, pNtk, 0 );
Kit_TruthCopy( pTruthDec, pTruthRes, pNtk->nVars );
Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar );
return pTruthRes;
}
// assign elementary truth tables
for ( i = 0; i < (int)pNtk->nVars; i++ )
Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
// compute truth table for each node
pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
pTruthRes = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp, iVar, pTruthDec );
// complement the truth table if needed
if ( Kit_DsdLitIsCompl(pNtk->Root) )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
return pTruthRes;
}
/**Function*************************************************************
@ -522,10 +700,11 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
SeeAlso []
***********************************************************************/
void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec )
{
unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp );
Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
unsigned * pTruth = Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar, pTruthDec );
if ( pTruthCo )
Kit_TruthCopy( pTruthCo, pTruth, pNtk->nVars );
}
/**Function*************************************************************
@ -539,16 +718,29 @@ void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTru
SeeAlso []
***********************************************************************/
void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec )
void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
{
unsigned * pTruth;
Kit_DsdObj_t * pRoot;
Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar );
pRoot = Kit_DsdNtkRoot( pNtk );
pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+0 );
Kit_TruthCopy( pTruthCo, pTruth, p->nVars );
pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+1 );
Kit_TruthCopy( pTruthDec, pTruth, p->nVars );
unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp );
Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
/*
// verification
{
// compute the same function using different procedure
unsigned * pTruthTemp = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes + 1);
pNtk->pSupps = NULL;
Kit_DsdTruthComputeTwo( p, pNtk, uSupp, -1, pTruthTemp );
// if ( !Kit_TruthIsEqual( pTruthTemp, pTruthRes, pNtk->nVars ) )
if ( !Kit_TruthIsEqualWithPhase( pTruthTemp, pTruthRes, pNtk->nVars ) )
{
printf( "Verification FAILED!\n" );
Kit_DsdPrint( stdout, pNtk );
Kit_DsdPrintFromTruth( pTruthRes, pNtk->nVars );
Kit_DsdPrintFromTruth( pTruthTemp, pNtk->nVars );
}
// else
// printf( "Verification successful.\n" );
}
*/
}
/**Function*************************************************************
@ -1090,9 +1282,10 @@ unsigned Kit_DsdGetSupports_rec( Kit_DsdNtk_t * p, int iLit )
SeeAlso []
***********************************************************************/
void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p )
{
Kit_DsdObj_t * pRoot;
unsigned uSupport;
assert( p->pSupps == NULL );
p->pSupps = ALLOC( unsigned, p->nNodes );
// consider simple special cases
@ -1100,16 +1293,17 @@ void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
if ( pRoot->Type == KIT_DSD_CONST1 )
{
assert( p->nNodes == 1 );
p->pSupps[0] = 0;
uSupport = p->pSupps[0] = 0;
}
if ( pRoot->Type == KIT_DSD_VAR )
{
assert( p->nNodes == 1 );
p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
uSupport = p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
}
else
Kit_DsdGetSupports_rec( p, p->Root );
assert( p->pSupps[0] <= 0xFFFF );
uSupport = Kit_DsdGetSupports_rec( p, p->Root );
assert( uSupport <= 0xFFFF );
return uSupport;
}
/**Function*************************************************************
@ -1697,7 +1891,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
{
Kit_DsdMan_t * p;
unsigned * pTruthC;
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );

31
src/aig/kit/kitHop.c
View File

@ -29,7 +29,6 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Transforms the decomposition graph into the AIG.]
@ -85,6 +84,36 @@ Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
return Kit_GraphToHopInternal( pMan, pGraph );
}
/**Function*************************************************************
Synopsis [Strashed onen logic nodes using its truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
{
Hop_Obj_t * pObj;
Kit_Graph_t * pGraph;
// transform truth table into the decomposition tree
if ( vMemory == NULL )
{
vMemory = Vec_IntAlloc( 0 );
pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
Vec_IntFree( vMemory );
}
else
pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
// derive the AIG for the decomposition tree
pObj = Kit_GraphToHop( pMan, pGraph );
Kit_GraphFree( pGraph );
return pObj;
}
/**Function*************************************************************
Synopsis [Strashes one logic node using its SOP.]

2
src/aig/kit/kitTruth.c
View File

@ -845,7 +845,7 @@ void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned
/**Function*************************************************************
Synopsis [Computes negative cofactor of the function.]
Synopsis [Multiplexes two functions with the given variable.]
Description []

1
src/aig/rwt/rwt.h
View File

@ -30,6 +30,7 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
#include "mem.h"
#include "extra.h"
#include "vec.h"
////////////////////////////////////////////////////////////////////////

39
src/base/abc/abcFanio.c
View File

@ -28,6 +28,45 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry )
{
if ( p->nSize == p->nCap )
{
int * pArray;
int i;
if ( p->nSize == 0 )
p->nCap = 1;
if ( pMemMan )
pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
else
pArray = ALLOC( int, p->nCap * 2 );
if ( p->pArray )
{
for ( i = 0; i < p->nSize; i++ )
pArray[i] = p->pArray[i];
if ( pMemMan )
Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
else
free( p->pArray );
}
p->nCap *= 2;
p->pArray = pArray;
}
p->pArray[p->nSize++] = Entry;
}
/**Function*************************************************************
Synopsis [Creates fanout/fanin relationship between the nodes.]

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

@ -115,6 +115,7 @@ static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCompress2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDChoice ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -283,6 +284,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "drw", Abc_CommandDRewrite, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drf", Abc_CommandDRefactor, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dcompress2", Abc_CommandDCompress2, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dchoice", Abc_CommandDChoice, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drwsat", Abc_CommandDrwsat, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 );
@ -2977,8 +2979,8 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
printf("This command will be available soon\n");
return 0;
// printf("This command will be available soon\n");
// return 0;
// set defaults
memset( pPars, 0, sizeof(Lpk_Par_t) );
@ -6177,6 +6179,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int nLevels;
int fVerbose;
// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
// extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
@ -6187,15 +6190,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fVerbose = 0;
nLevels = 1000;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
{
switch ( c )
{
@ -6210,6 +6215,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nLevels < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -6311,7 +6319,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// pNtkRes = Abc_NtkDar( pNtk );
pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@ -6323,6 +6332,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: test [-h]\n" );
fprintf( pErr, "\t testbench for new procedures\n" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -7138,6 +7148,84 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int fBalance, fVerbose, fUpdateLevel, c;
extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fBalance = 1;
fUpdateLevel = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF )
{
switch ( c )
{
case 'b':
fBalance ^= 1;
break;
case 'l':
fUpdateLevel ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: dchoice [-blvh]\n" );
fprintf( pErr, "\t performs partitioned choicing using a new AIG package\n" );
fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -11819,24 +11907,24 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFrames = 0; // if 0, iterates through frames
nFrames =16;
fRetimeFirst = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
case 'K':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames <= 0 )
if ( nFrames < 0 )
goto usage;
break;
case 'r':
@ -11872,9 +11960,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: dsec [-F num] [-rwvh] <file1> <file2>\n" );
fprintf( pErr, "usage: dsec [-K num] [-rwvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
@ -11914,24 +12002,24 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFrames = 0; // if 0, iterates through frames
fRetimeFirst = 1;
fVerbose = 0;
fVeryVerbose = 0;
nFrames = 16;
fRetimeFirst = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
case 'K':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames <= 0 )
if ( nFrames < 0 )
goto usage;
break;
case 'r':
@ -11964,9 +12052,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
fprintf( pErr, "usage: dprove [-K num] [-rwvh]\n" );
fprintf( pErr, "\t performs SEC on the sequential miter\n" );
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );

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

@ -67,6 +67,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
}
// create the manager
pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
pMan->pName = Extra_UtilStrsav( pNtk->pName );
// save the number of registers
if ( fRegisters )
pMan->nRegs = Abc_NtkLatchNum(pNtk);
@ -250,6 +251,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Aig_ManForEachPi( pMan, pObj, i )
pObj->pData = Abc_NtkCi(pNtkNew, i);
// rebuild the AIG
vNodes = Aig_ManDfsChoices( pMan );
Vec_PtrForEachEntry( vNodes, pObj, i )
@ -265,21 +267,8 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
pAbcRepr->pData = pAbcObj;
}
}
printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
//printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
Vec_PtrFree( vNodes );
/*
{
Abc_Obj_t * pNode;
int k, Counter = 0;
Abc_NtkForEachNode( pNtkNew, pNode, k )
if ( pNode->pData != 0 )
{
int x = 0;
Counter++;
}
printf( "Choices = %d.\n", Counter );
}
*/
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
@ -496,11 +485,11 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
return NULL;
Fra_ParamsDefault( pPars );
pPars->nBTLimitNode = nConfLimit;
pPars->fVerbose = fVerbose;
pPars->fProve = fProve;
pPars->fChoicing = fChoicing;
pPars->fDoSparse = fDoSparse;
pPars->fSpeculate = fSpeculate;
pPars->fChoicing = fChoicing;
pPars->fProve = fProve;
pPars->fVerbose = fVerbose;
pMan = Fra_FraigPerform( pTemp = pMan, pPars );
if ( fChoicing )
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
@ -631,7 +620,7 @@ clk = clock();
***********************************************************************/
Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
{
Aig_Man_t * pMan;//, * pTemp;
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
int clk;
assert( Abc_NtkIsStrash(pNtk) );
@ -641,8 +630,8 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
// Aig_ManPrintStats( pMan );
clk = clock();
pMan = Dar_ManCompress2( pMan, fBalance, fUpdateLevel, fVerbose );
// Aig_ManStop( pTemp );
pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
// Aig_ManPrintStats( pMan );
@ -651,6 +640,32 @@ clk = clock();
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0 );
if ( pMan == NULL )
return NULL;
pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@ -664,7 +679,7 @@ clk = clock();
***********************************************************************/
Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
{
Aig_Man_t * pMan;//, * pTemp;
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
int clk;
assert( Abc_NtkIsStrash(pNtk) );
@ -674,8 +689,8 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
// Aig_ManPrintStats( pMan );
clk = clock();
pMan = Dar_ManRwsat( pMan, fBalance, fVerbose );
// Aig_ManStop( pTemp );
pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose );
Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
// Aig_ManPrintStats( pMan );
@ -1118,8 +1133,10 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbos
Aig_ManSeqCleanup( pMan );
if ( fLatchSweep )
{
pMan = Aig_ManReduceLaches( pMan, fVerbose );
pMan = Aig_ManConstReduce( pMan, fVerbose );
if ( pMan->nRegs )
pMan = Aig_ManReduceLaches( pMan, fVerbose );
if ( pMan->nRegs )
pMan = Aig_ManConstReduce( pMan, fVerbose );
}
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );

12
src/base/abci/abcFraig.c
View File

@ -673,7 +673,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
}
}
Vec_PtrPush( vStore, pNtk );
printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
return 1;
}
@ -704,9 +704,15 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
printf( "There are no network currently in storage.\n" );
return NULL;
}
printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
// printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
pNtk = Vec_PtrEntry( vStore, 0 );
// swap the first and last network
// this should lead to the primary choice being "better" because of synthesis
pNtk = Vec_PtrPop( vStore );
Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) );
Vec_PtrWriteEntry( vStore, 0, pNtk );
// to determine the number of simulation patterns
// use the following strategy
// at least 64 words (32 words random and 32 words dynamic)
@ -731,7 +737,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
// perform partitioned computation of structural choices
pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
Abc_NtkFraigStoreClean();
PRT( "Total choicing time", clock() - clk );
//PRT( "Total choicing time", clock() - clk );
return pFraig;
}

8
src/base/abci/abcIf.c
View File

@ -299,12 +299,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
}
else
{
extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
// transform truth table into the decomposition tree
Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
// derive the AIG for the decomposition tree
pNodeNew->pData = Kit_GraphToHop( pNtkNew->pManFunc, pGraph );
Kit_GraphFree( pGraph );
extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
pNodeNew->pData = Kit_TruthToHop( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
}
// complement the node if the cut was complemented
if ( pCutBest->fCompl )

2
src/base/abci/abcQbf.c
View File

@ -140,7 +140,7 @@ clkV = clock() - clkV;
printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
printf( " " );
PRTn( "Syn", clkS );
// PRTn( "Syn", clkS );
PRT( "Ver", clkV );
}
}

4
src/base/io/ioWriteAiger.c
View File

@ -249,8 +249,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
// write the comment
fprintf( pFile, "c\n" );
fprintf( pFile, "%s\n", pNtk->pName );
fprintf( pFile, "This file in the AIGER format was written by ABC on %s\n", Extra_TimeStamp() );
fprintf( pFile, "For information about the format, refer to %s\n", "http://fmv.jku.at/aiger" );
fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
fclose( pFile );
}

2
src/map/fpga/fpgaLib.c
View File

@ -129,7 +129,7 @@ Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose )
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-degreasing order. Technology mapping may not work correctly.\n",
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] );
}

2
src/map/if/ifMan.c
View File

@ -363,7 +363,7 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
if ( p->pPars->fTruth )
{
int i, nTruthWords;
nTruthWords = Extra_TruthWordNum( pCut->nLimit );
nTruthWords = pCut->nLimit <= 5 ? 1 : (1 << (pCut->nLimit - 5));
for ( i = 0; i < nTruthWords; i++ )
If_CutTruth(pCut)[i] = 0xAAAAAAAA;
}

2
src/map/if/ifTime.c
View File

@ -172,7 +172,7 @@ void If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float ObjRequired )
/**Function*************************************************************
Synopsis [Sorts the pins in the degreasing order of delays.]
Synopsis [Sorts the pins in the decreasing order of delays.]
Description []

146
src/map/if/ifTruth.c
View File

@ -28,6 +28,134 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Several simple procedures working with truth tables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int If_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline void If_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~pIn[w];
}
static inline void If_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn[w];
}
static inline void If_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~(pIn0[w] & pIn1[w]);
}
static inline void If_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn0[w] & pIn1[w];
}
/**Function*************************************************************
Synopsis [Swaps two adjacent variables in the truth table.]
Description [Swaps var number Start and var number Start+1 (0-based numbers).
The input truth table is pIn. The output truth table is pOut.]
SideEffects []
SeeAlso []
***********************************************************************/
void If_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
{
static unsigned PMasks[4][3] = {
{ 0x99999999, 0x22222222, 0x44444444 },
{ 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
{ 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
{ 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
};
int nWords = If_TruthWordNum( nVars );
int i, k, Step, Shift;
assert( iVar < nVars - 1 );
if ( iVar < 4 )
{
Shift = (1 << iVar);
for ( i = 0; i < nWords; i++ )
pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
}
else if ( iVar > 4 )
{
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 4*Step )
{
for ( i = 0; i < Step; i++ )
pOut[i] = pIn[i];
for ( i = 0; i < Step; i++ )
pOut[Step+i] = pIn[2*Step+i];
for ( i = 0; i < Step; i++ )
pOut[2*Step+i] = pIn[Step+i];
for ( i = 0; i < Step; i++ )
pOut[3*Step+i] = pIn[3*Step+i];
pIn += 4*Step;
pOut += 4*Step;
}
}
else // if ( iVar == 4 )
{
for ( i = 0; i < nWords; i += 2 )
{
pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
}
}
}
/**Function*************************************************************
Synopsis [Expands the truth table according to the phase.]
Description [The input and output truth tables are in pIn/pOut. The current number
of variables is nVars. The total number of variables in nVarsAll. The last argument
(Phase) contains shows where the variables should go.]
SideEffects []
SeeAlso []
***********************************************************************/
void If_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
{
unsigned * pTemp;
int i, k, Var = nVars - 1, Counter = 0;
for ( i = nVarsAll - 1; i >= 0; i-- )
if ( Phase & (1 << i) )
{
for ( k = Var; k < i; k++ )
{
If_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
pTemp = pIn; pIn = pOut; pOut = pTemp;
Counter++;
}
Var--;
}
assert( Var == -1 );
// swap if it was moved an even number of times
if ( !(Counter & 1) )
If_TruthCopy( pOut, pIn, nVarsAll );
}
/**Function*************************************************************
Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
@ -39,7 +167,7 @@
SeeAlso []
***********************************************************************/
static inline unsigned Cut_TruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
static inline unsigned If_CutTruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
{
unsigned uPhase = 0;
int i, k;
@ -73,22 +201,22 @@ void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
// permute the first table
if ( fCompl0 ^ pCut0->fCompl )
Extra_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
If_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
else
Extra_TruthCopy( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
Extra_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut0) );
If_TruthCopy( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
If_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nLimit, If_CutTruthPhase(pCut, pCut0) );
// permute the second table
if ( fCompl1 ^ pCut1->fCompl )
Extra_TruthNot( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
If_TruthNot( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
else
Extra_TruthCopy( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
Extra_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut1) );
If_TruthCopy( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
If_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nLimit, If_CutTruthPhase(pCut, pCut1) );
// produce the resulting table
assert( pCut->fCompl == 0 );
if ( pCut->fCompl )
Extra_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
If_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
else
Extra_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
If_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
// perform
// Kit_FactorTest( If_CutTruth(pCut), pCut->nLimit );

0
src/map/pcm/module.make Normal file
View File

46
src/misc/vec/vec.h
View File

@ -25,12 +25,50 @@
extern "C" {
#endif
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
// this include should be the first one in the list
// it is used to catch memory leaks on Windows
#include "leaks.h"
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifndef ABS
#define ABS(a) ((a) < 0 ? -(a) : (a))
#endif
#ifndef MAX
#define MAX(a,b) ((a) > (b) ? (a) : (b))
#endif
#ifndef MIN
#define MIN(a,b) ((a) < (b) ? (a) : (b))
#endif
#ifndef ALLOC
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#endif
#ifndef FREE
#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
#endif
#ifndef REALLOC
#define REALLOC(type, obj, num) \
((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
((type *) malloc(sizeof(type) * (num))))
#endif
#ifndef PRT
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
#include "vecInt.h"
@ -48,10 +86,6 @@ extern "C" {
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////

35
src/misc/vec/vecFlt.h
View File

@ -445,41 +445,6 @@ static inline void Vec_FltPush( Vec_Flt_t * p, float Entry )
p->pArray[p->nSize++] = Entry;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_FltPushMem( Extra_MmStep_t * pMemMan, Vec_Flt_t * p, float Entry )
{
if ( p->nSize == p->nCap )
{
float * pArray;
int i;
if ( p->nSize == 0 )
p->nCap = 1;
pArray = (float *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
// pArray = ALLOC( float, p->nCap * 2 );
if ( p->pArray )
{
for ( i = 0; i < p->nSize; i++ )
pArray[i] = p->pArray[i];
Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
// free( p->pArray );
}
p->nCap *= 2;
p->pArray = pArray;
}
p->pArray[p->nSize++] = Entry;
}
/**Function*************************************************************
Synopsis []

40
src/misc/vec/vecInt.h
View File

@ -26,7 +26,6 @@
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include "extra.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -475,45 +474,6 @@ static inline void Vec_IntPushFirst( Vec_Int_t * p, int Entry )
p->pArray[0] = Entry;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry )
{
if ( p->nSize == p->nCap )
{
int * pArray;
int i;
if ( p->nSize == 0 )
p->nCap = 1;
if ( pMemMan )
pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
else
pArray = ALLOC( int, p->nCap * 2 );
if ( p->pArray )
{
for ( i = 0; i < p->nSize; i++ )
pArray[i] = p->pArray[i];
if ( pMemMan )
Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
else
free( p->pArray );
}
p->nCap *= 2;
p->pArray = pArray;
}
p->pArray[p->nSize++] = Entry;
}
/**Function*************************************************************
Synopsis [Inserts the entry while preserving the increasing order.]

23
src/misc/vec/vecStr.h
View File

@ -401,6 +401,27 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
p->pArray[p->nSize++] = Entry;
}
/**Function********************************************************************
Synopsis [Finds the smallest integer larger of equal than the logarithm.]
Description [Returns [Log10(Num)].]
SideEffects []
SeeAlso []
******************************************************************************/
static inline Vec_StrBase10Log( unsigned Num )
{
int Res;
assert( Num >= 0 );
if ( Num == 0 ) return 0;
if ( Num == 1 ) return 1;
for ( Res = 0, Num--; Num; Num /= 10, Res++ );
return Res;
} /* end of Extra_Base2Log */
/**Function*************************************************************
Synopsis []
@ -425,7 +446,7 @@ static inline void Vec_StrPrintNum( Vec_Str_t * p, int Num )
Vec_StrPush( p, (char)('0' + Num) );
return;
}
nDigits = Extra_Base10Log( Num );
nDigits = Vec_StrBase10Log( Num );
Vec_StrGrow( p, p->nSize + nDigits );
for ( i = nDigits - 1; i >= 0; i-- )
{

134
src/opt/lpk/lpkAbcDec.c
View File

@ -17,7 +17,7 @@
Revision [$Id: lpkAbcDec.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
@ -41,24 +41,29 @@
***********************************************************************/
Abc_Obj_t * Lpk_ImplementFun( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
{
extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
unsigned * pTruth;
Abc_Obj_t * pObjNew;
int i;
// create the new node
pObjNew = Abc_NtkCreateNode( pNtk );
for ( i = 0; i < (int)p->nVars; i++ )
Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) );
Abc_ObjLevelNew( pObjNew );
// create the logic function
// assign the node's function
pTruth = Lpk_FunTruth(p, 0);
if ( p->nVars == 0 )
{
extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
// allocate memory for the ISOP
Vec_Int_t * vCover = Vec_IntAlloc( 0 );
// transform truth table into the decomposition tree
Kit_Graph_t * pGraph = Kit_TruthToGraph( Lpk_FunTruth(p, 0), p->nVars, vCover );
// derive the AIG for the decomposition tree
pObjNew->pData = Kit_GraphToHop( pNtk->pManFunc, pGraph );
Kit_GraphFree( pGraph );
Vec_IntFree( vCover );
pObjNew->pData = Hop_NotCond( Hop_ManConst1(pNtk->pManFunc), !(pTruth[0] & 1) );
return pObjNew;
}
if ( p->nVars == 1 )
{
pObjNew->pData = Hop_NotCond( Hop_ManPi(pNtk->pManFunc, 0), (pTruth[0] & 1) );
return pObjNew;
}
// create the logic function
pObjNew->pData = Kit_TruthToHop( pNtk->pManFunc, pTruth, p->nVars, NULL );
return pObjNew;
}
@ -85,6 +90,7 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld
Vec_PtrWriteEntry( vLeaves, i, pRes );
Lpk_FunFree( pFun );
}
Vec_PtrShrink( vLeaves, nLeavesOld );
return pRes;
}
@ -92,7 +98,9 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld
Synopsis [Decomposes the function using recursive MUX decomposition.]
Description []
Description [Returns the ID of the top-most decomposition node
implementing this function, or 0 if there is no decomposition satisfying
the constraints on area and delay.]
SideEffects []
@ -101,22 +109,78 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld
***********************************************************************/
int Lpk_Decompose_rec( Lpk_Fun_t * p )
{
Lpk_Res_t * pResMux, * pResDsd;
Lpk_Fun_t * p2;
int VarPol;
assert( p->nAreaLim > 0 );
if ( p->nVars <= p->nLutK )
// is only called for non-trivial blocks
assert( p->nLutK >= 3 && p->nLutK <= 6 );
assert( p->nVars > p->nLutK );
// skip if area bound is exceeded
if ( Lpk_LutNumLuts(p->nVars, p->nLutK) > (int)p->nAreaLim )
return 0;
// skip if delay bound is exceeded
if ( Lpk_SuppDelay(p->uSupp, p->pDelays) > (int)p->nDelayLim )
return 0;
// check MUX decomposition
pResMux = Lpk_MuxAnalize( p );
assert( !pResMux || (pResMux->DelayEst <= (int)p->nDelayLim && pResMux->AreaEst <= (int)p->nAreaLim) );
// accept MUX decomposition if it is "good"
if ( pResMux && pResMux->nSuppSizeS <= (int)p->nLutK && pResMux->nSuppSizeL <= (int)p->nLutK )
pResDsd = NULL;
else
{
pResDsd = Lpk_DsdAnalize( p );
assert( !pResDsd || (pResDsd->DelayEst <= (int)p->nDelayLim && pResDsd->AreaEst <= (int)p->nAreaLim) );
}
if ( pResMux && pResDsd )
{
// compare two decompositions
if ( pResMux->AreaEst < pResDsd->AreaEst ||
(pResMux->AreaEst == pResDsd->AreaEst && pResMux->nSuppSizeL < pResDsd->nSuppSizeL) ||
(pResMux->AreaEst == pResDsd->AreaEst && pResMux->nSuppSizeL == pResDsd->nSuppSizeL && pResMux->DelayEst < pResDsd->DelayEst) )
pResDsd = NULL;
else
pResMux = NULL;
}
assert( pResMux == NULL || pResDsd == NULL );
if ( pResMux )
{
p2 = Lpk_MuxSplit( p, pResMux->pCofVars[0], pResMux->Polarity );
if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( p2 ) )
return 0;
if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) )
return 0;
return 1;
// check if decomposition exists
VarPol = Lpk_MuxAnalize( p );
if ( VarPol == -1 )
return 0;
// split and call recursively
p2 = Lpk_MuxSplit( p, VarPol );
if ( !Lpk_Decompose_rec( p2 ) )
return 0;
return Lpk_Decompose_rec( p );
}
if ( pResDsd )
{
p2 = Lpk_DsdSplit( p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
assert( p2->nVars <= (int)p->nLutK );
if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) )
return 0;
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis [Removes decomposed nodes from the array of fanins.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Lpk_DecomposeClean( Vec_Ptr_t * vLeaves, int nLeavesOld )
{
Lpk_Fun_t * pFunc;
int i;
Vec_PtrForEachEntryStart( vLeaves, pFunc, i, nLeavesOld )
Lpk_FunFree( pFunc );
Vec_PtrShrink( vLeaves, nLeavesOld );
}
/**Function*************************************************************
@ -131,22 +195,16 @@ int Lpk_Decompose_rec( Lpk_Fun_t * p )
***********************************************************************/
Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
{
Lpk_Fun_t * p;
Lpk_Fun_t * pFun;
Abc_Obj_t * pObjNew = NULL;
int i, nLeaves;
// create the starting function
nLeaves = Vec_PtrSize( vLeaves );
p = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
Lpk_FunSuppMinimize( p );
// decompose the function
if ( Lpk_Decompose_rec(p) )
int nLeaves = Vec_PtrSize( vLeaves );
pFun = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
Lpk_FunSuppMinimize( pFun );
if ( pFun->nVars <= pFun->nLutK )
pObjNew = Lpk_ImplementFun( pNtk, vLeaves, pFun );
else if ( Lpk_Decompose_rec(pFun) )
pObjNew = Lpk_Implement( pNtk, vLeaves, nLeaves );
else
{
for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeaves; i-- )
Lpk_FunFree( Vec_PtrEntry(vLeaves, i) );
}
Vec_PtrShrink( vLeaves, nLeaves );
Lpk_DecomposeClean( vLeaves, nLeaves );
return pObjNew;
}

129
src/opt/lpk/lpkAbcDsd.c
View File

@ -30,9 +30,11 @@
/**Function*************************************************************
Synopsis [Returns the variable whose cofs have min sum of supp sizes.]
Synopsis [Cofactors TTs w.r.t. all vars and finds the best var.]
Description []
Description [The best variable is the variable with the minimum
sum total of the support sizes of all truth tables. This procedure
computes and returns cofactors w.r.t. the best variable.]
SideEffects []
@ -42,6 +44,7 @@
int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs )
{
int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
assert( nTruths > 0 );
VarBest = -1;
Lpk_SuppForEachVar( p->uSupp, Var )
{
@ -85,7 +88,7 @@ int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTrut
SeeAlso []
***********************************************************************/
unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets, int nSizeMax )
{
unsigned i, iLitFanin, uSupport, uSuppCur;
Kit_DsdObj_t * pObj;
@ -99,7 +102,7 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets );
uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax );
uSupport |= uSupps[i];
}
// create all subsets, except empty and full
@ -110,7 +113,8 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets
for ( i = 0; i < pObj->nFans; i++ )
if ( s & (1 << i) )
uSuppCur |= uSupps[i];
Vec_IntPush( vSets, uSuppCur );
if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
Vec_IntPush( vSets, uSuppCur );
}
return uSupport;
}
@ -119,9 +123,10 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets
uSupport = 0;
Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
{
uSuppCur = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets );
uSuppCur = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax );
uSupport |= uSuppCur;
Vec_IntPush( vSets, uSuppCur );
if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax )
Vec_IntPush( vSets, uSuppCur );
}
return uSupport;
}
@ -150,12 +155,15 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
{
uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
Vec_IntPush( vSets, uSupport );
if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
Vec_IntPush( vSets, uSupport );
return vSets;
}
uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets );
uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets, nSizeMax );
assert( (uSupport & 0xFFFF0000) == 0 );
Vec_IntPush( vSets, uSupport );
// add the total support of the network
if ( Kit_WordCountOnes(uSupport) <= nSizeMax )
Vec_IntPush( vSets, uSupport );
// set the remaining variables
Vec_IntForEachEntry( vSets, Number, i )
{
@ -176,7 +184,7 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
SeeAlso []
***********************************************************************/
Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 )
Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSizeMax )
{
Vec_Int_t * vSets;
int Entry0, Entry1, Entry;
@ -188,7 +196,8 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 )
Entry = Entry0 | Entry1;
if ( (Entry & (Entry >> 16)) )
continue;
Vec_IntPush( vSets, Entry );
if ( Kit_WordCountOnes(Entry) <= nSizeMax )
Vec_IntPush( vSets, Entry );
}
return vSets;
}
@ -266,14 +275,15 @@ void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5
SeeAlso []
***********************************************************************/
Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes )
{
static Lpk_Res_t Res, * pRes = &Res;
unsigned * ppTruths[5][16];
Vec_Int_t * pvBSets[4][8];
Kit_DsdNtk_t * pNtkDec, * pTemp;
unsigned uBoundSet;
int i, k, nVarsBS, nVarsRem, Delay, Area;
assert( nCofDepth >= 0 && nCofDepth < 4 );
assert( nCofDepth < (int)p->nLutK - 1 );
Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths );
// find the best cofactors
memset( pRes, 0, sizeof(Lpk_Res_t) );
@ -291,7 +301,7 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
// derive the set of feasible boundsets
for ( i = nCofDepth - 1; i >= 0; i-- )
for ( k = 0; k < (1<<i); k++ )
pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1] );
pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
// compare the resulting boundsets
Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i )
{
@ -299,12 +309,13 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
continue;
assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
assert( nVarsBS <= (int)p->nLutK - nCofDepth );
nVarsRem = p->nVars - nVarsBS + nCofDepth + 1;
Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
if ( Delay > (int)p->nDelayLim || Area > (int)p->nAreaLim )
Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
continue;
if ( uBoundSet == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
if ( pRes->BSVars == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
{
pRes->nBSVars = nVarsBS;
pRes->BSVars = uBoundSet;
@ -316,7 +327,60 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
}
// free cofactor storage
Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths );
return pRes;
}
/**Function*************************************************************
Synopsis [Performs DSD-based decomposition of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p )
{
static Lpk_Res_t Res0, * pRes0 = &Res0;
static Lpk_Res_t Res1, * pRes1 = &Res1;
static Lpk_Res_t Res2, * pRes2 = &Res2;
static Lpk_Res_t Res3, * pRes3 = &Res3;
memset( pRes0, 0, sizeof(Lpk_Res_t) );
memset( pRes1, 0, sizeof(Lpk_Res_t) );
memset( pRes2, 0, sizeof(Lpk_Res_t) );
memset( pRes3, 0, sizeof(Lpk_Res_t) );
assert( p->uSupp == Kit_BitMask(p->nVars) );
// try decomposition without cofactoring
Lpk_DsdAnalizeOne( p, 0, pRes0 );
if ( pRes0->nBSVars == (int)p->nLutK && pRes0->AreaEst <= (int)p->nAreaLim && pRes0->DelayEst <= (int)p->nDelayLim )
return pRes0;
// cofactor 1 time
if ( p->nLutK >= 3 )
Lpk_DsdAnalizeOne( p, 1, pRes1 );
assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
if ( pRes1->nBSVars == (int)p->nLutK - 1 && pRes1->AreaEst <= (int)p->nAreaLim && pRes1->DelayEst <= (int)p->nDelayLim )
return pRes1;
// cofactor 2 times
if ( p->nLutK >= 4 )
Lpk_DsdAnalizeOne( p, 2, pRes2 );
assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
if ( pRes2->nBSVars == (int)p->nLutK - 2 && pRes2->AreaEst <= (int)p->nAreaLim && pRes2->DelayEst <= (int)p->nDelayLim )
return pRes2;
// cofactor 3 times
if ( p->nLutK >= 5 )
Lpk_DsdAnalizeOne( p, 3, pRes3 );
assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
if ( pRes3->nBSVars == (int)p->nLutK - 3 && pRes3->AreaEst <= (int)p->nAreaLim && pRes3->DelayEst <= (int)p->nDelayLim )
return pRes3;
// choose the best under these conditions
return NULL;
}
/**Function*************************************************************
@ -332,19 +396,21 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth )
***********************************************************************/
Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
{
Lpk_Fun_t * pNew;
Kit_DsdMan_t * pDsdMan;
Kit_DsdNtk_t * pNtkDec, * pTemp;
unsigned * pTruth = Lpk_FunTruth( p, 0 );
unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
Lpk_Fun_t * pNew;
unsigned * ppTruths[5][16];
char pBSVars[5];
int i, k, nVars, nCofs;
int i, k, nVars, iVacVar, nCofs;
// get the bound set variables
nVars = Lpk_SuppToVars( uBoundSet, pBSVars );
// get the vacuous variable
iVacVar = pBSVars[0];
// compute the cofactors
Lpk_FunAllocTruthTables( p, nCofVars, ppTruths );
Lpk_FunAllocTruthTables( p, nCofVars + 1, ppTruths );
for ( i = 0; i < nCofVars; i++ )
for ( k = 0; k < (1<<i); k++ )
{
@ -353,38 +419,37 @@ Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned
}
// decompose each cofactor w.r.t. the bound set
nCofs = (1<<nCofVars);
pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 4 );
pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 2 );
for ( k = 0; k < nCofs; k++ )
{
pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars );
pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp );
Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, pBSVars[0], ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] );
Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, iVacVar, ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] );
Kit_DsdNtkFree( pNtkDec );
}
Kit_DsdManFree( pDsdMan );
// compute the composition function
for ( i = nCofVars - 1; i >= 1; i-- )
// compute the composition/decomposition functions (they will be in pTruth0/pTruth1)
for ( i = nCofVars; i >= 1; i-- )
for ( k = 0; k < (1<<i); k++ )
Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i] );
// now the composition/decomposition functions are in pTruth0/pTruth1
Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i-1] );
// derive the new component
pNew = Lpk_FunDup( p, pTruth1 );
// update the old component
Kit_TruthCopy( pTruth, pTruth0, p->nVars );
p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
p->pFanins[pBSVars[0]] = pNew->Id;
p->pDelays[pBSVars[0]] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
p->pFanins[iVacVar] = pNew->Id;
p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
// support minimize both
Lpk_FunSuppMinimize( p );
Lpk_FunSuppMinimize( pNew );
// update delay and area requirements
pNew->nDelayLim = p->nDelayLim - 1;
pNew->nDelayLim = p->pDelays[iVacVar];
pNew->nAreaLim = 1;
p->nAreaLim = p->nAreaLim - 1;
// free cofactor storage
Lpk_FunFreeTruthTables( p, nCofVars, ppTruths );
Lpk_FunFreeTruthTables( p, nCofVars + 1, ppTruths );
return pNew;
}

131
src/opt/lpk/lpkAbcMux.c
View File

@ -48,7 +48,6 @@ void Lpk_FunComputeCofs( Lpk_Fun_t * p, int iVar )
Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, iVar );
}
/**Function*************************************************************
Synopsis [Computes cofactors w.r.t. each variable.]
@ -85,18 +84,18 @@ void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps )
SeeAlso []
***********************************************************************/
int Lpk_MuxAnalize( Lpk_Fun_t * p )
Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p )
{
unsigned puSupps[32] = {0};
int nSuppSize0, nSuppSize1, Delay, Delay0, Delay1, DelayA, DelayB;
int Var, Area, Polarity, VarBest, AreaBest, PolarityBest, nSuppSizeBest;
if ( p->nVars > p->nAreaLim * (p->nLutK - 1) + 1 )
return -1;
static Lpk_Res_t Res, * pRes = &Res;
unsigned puSupps[32];
int nSuppSize0, nSuppSize1, nSuppSizeBest;
int Var, Area, Polarity, Delay, Delay0, Delay1, DelayA, DelayB;
memset( pRes, 0, sizeof(Lpk_Res_t) );
assert( p->uSupp == Kit_BitMask(p->nVars) );
// get cofactor supports for each variable
Lpk_FunComputeCofSupps( p, puSupps );
// derive the delay and area of each MUX-decomposition
VarBest = -1;
// derive the delay and area after MUX-decomp with each var - and find the best var
pRes->Variable = -1;
Lpk_SuppForEachVar( p->uSupp, Var )
{
nSuppSize0 = Kit_WordCountOnes(puSupps[2*Var+0]);
@ -124,14 +123,6 @@ int Lpk_MuxAnalize( Lpk_Fun_t * p )
Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
Polarity = 0;
}
else if ( nSuppSize0 <= (int)p->nLutK )
{
DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
Delay = ABC_MAX( DelayA, DelayB + 1 );
Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK );
Polarity = 1;
}
else if ( nSuppSize1 <= (int)p->nLutK - 2 )
{
DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
@ -140,6 +131,14 @@ int Lpk_MuxAnalize( Lpk_Fun_t * p )
Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
Polarity = 1;
}
else if ( nSuppSize0 <= (int)p->nLutK )
{
DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
Delay = ABC_MAX( DelayA, DelayB + 1 );
Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK );
Polarity = 1;
}
else if ( nSuppSize1 <= (int)p->nLutK )
{
DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
@ -171,15 +170,16 @@ int Lpk_MuxAnalize( Lpk_Fun_t * p )
continue;
if ( Area > (int)p->nAreaLim )
continue;
if ( VarBest == -1 || AreaBest > Area || (AreaBest == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) )
if ( pRes->Variable == -1 || pRes->AreaEst > Area || (pRes->AreaEst == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) )
{
VarBest = Var;
AreaBest = Area;
PolarityBest = Polarity;
nSuppSizeBest = nSuppSize0+nSuppSize1;
pRes->Variable = Var;
pRes->Polarity = Polarity;
pRes->AreaEst = Area;
pRes->DelayEst = Delay;
nSuppSizeBest = nSuppSize0+nSuppSize1;
}
}
return (VarBest == -1)? -1 : (2*VarBest + Polarity);
return pRes->Variable == -1 ? NULL : pRes;
}
/**Function*************************************************************
@ -193,60 +193,61 @@ int Lpk_MuxAnalize( Lpk_Fun_t * p )
SeeAlso []
***********************************************************************/
Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int VarPol )
Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol )
{
Lpk_Fun_t * pNew;
unsigned * pTruth = Lpk_FunTruth( p, 0 );
unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
int Var = VarPol / 2;
int Pol = VarPol % 2;
int iVarVac;
assert( VarPol >= 0 && VarPol < 2 * (int)p->nVars );
assert( Var >= 0 && Var < (int)p->nVars );
assert( p->nAreaLim >= 2 );
Lpk_FunComputeCofs( p, Var );
if ( Pol == 0 )
// derive the new component
pNew = Lpk_FunDup( p, Pol ? pTruth0 : pTruth1 );
// update the support of the old component
p->uSupp = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars );
p->uSupp |= (1 << Var);
// update the truth table of the old component
iVarVac = Kit_WordFindFirstBit( ~p->uSupp );
assert( iVarVac < (int)p->nVars );
Kit_TruthIthVar( pTruth, p->nVars, Var );
if ( Pol )
Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, iVarVac );
else
Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, iVarVac );
// set the decomposed variable
p->pFanins[iVarVac] = pNew->Id;
p->pDelays[iVarVac] = p->nDelayLim - 1;
// support minimize both
Lpk_FunSuppMinimize( p );
Lpk_FunSuppMinimize( pNew );
// update delay and area requirements
pNew->nDelayLim = p->nDelayLim - 1;
if ( p->nVars <= p->nLutK )
{
// derive the new component
pNew = Lpk_FunDup( p, pTruth1 );
// update the old component
p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
iVarVac = Kit_WordFindFirstBit( ~(p->uSupp | (1 << Var)) );
assert( iVarVac < (int)p->nVars );
Kit_TruthIthVar( pTruth, p->nVars, iVarVac );
// update the truth table
Kit_TruthMux( pTruth, pTruth0, pTruth1, pTruth, p->nVars );
p->pFanins[iVarVac] = pNew->Id;
p->pDelays[iVarVac] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
// support minimize both
Lpk_FunSuppMinimize( p );
Lpk_FunSuppMinimize( pNew );
// update delay and area requirements
pNew->nDelayLim = p->nDelayLim - 1;
if ( p->nVars <= p->nLutK )
{
pNew->nAreaLim = p->nAreaLim - 1;
p->nAreaLim = 1;
}
else if ( pNew->nVars <= pNew->nLutK )
{
pNew->nAreaLim = 1;
p->nAreaLim = p->nAreaLim - 1;
}
else if ( p->nVars < pNew->nVars )
{
pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
}
else // if ( pNew->nVars < p->nVars )
{
pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
}
pNew->nAreaLim = p->nAreaLim - 1;
p->nAreaLim = 1;
}
else if ( pNew->nVars <= pNew->nLutK )
{
pNew->nAreaLim = 1;
p->nAreaLim = p->nAreaLim - 1;
}
else if ( p->nVars < pNew->nVars )
{
pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
}
else // if ( pNew->nVars < p->nVars )
{
pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
}
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

16
src/opt/lpk/lpkAbcUtil.c
View File

@ -139,20 +139,20 @@ Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth )
***********************************************************************/
void Lpk_FunSuppMinimize( Lpk_Fun_t * p )
{
int j, k, nVarsNew;
int i, k, nVarsNew;
// compress the truth table
if ( p->uSupp == Kit_BitMask(p->nVars) )
return;
// minimize support
nVarsNew = Kit_WordCountOnes(p->uSupp);
Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
for ( j = k = 0; j < (int)p->nVars; j++ )
if ( p->uSupp & (1 << j) )
{
p->pFanins[k] = p->pFanins[j];
p->pDelays[k] = p->pDelays[j];
k++;
}
k = 0;
Lpk_SuppForEachVar( p->uSupp, i )
{
p->pFanins[k] = p->pFanins[i];
p->pDelays[k] = p->pDelays[i];
k++;
}
assert( k == nVarsNew );
p->nVars = k;
p->uSupp = Kit_BitMask(p->nVars);

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

@ -361,17 +361,10 @@ p->timeTruth += clock() - clk;
if ( p->pPars->fVeryVerbose )
{
// char * pFileName;
int nSuppSize;
Kit_DsdNtk_t * pDsdNtk;
nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
int nSuppSize = Extra_TruthSupportSize( pTruth, pCut->nLeaves );
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves );
// Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves );
Kit_DsdPrint( stdout, pDsdNtk );
Kit_DsdNtkFree( pDsdNtk );
// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
// pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
// printf( "Saved truth table in file \"%s\".\n", pFileName );
}

9
src/opt/lpk/lpkCut.c
View File

@ -30,7 +30,7 @@
/**Function*************************************************************
Synopsis [Computes the truth able of one cut.]
Synopsis [Computes the truth table of one cut.]
Description []
@ -445,10 +445,17 @@ void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
pCutNew->nNodes = pCut->nNodes;
pCutNew->nNodesDup = pCut->nNodesDup;
// check if the node is already there
// if so, move the node to be the last
for ( i = 0; i < (int)pCutNew->nNodes; i++ )
if ( pCutNew->pNodes[i] == Node )
{
for ( k = i; k < (int)pCutNew->nNodes - 1; k++ )
pCutNew->pNodes[k] = pCutNew->pNodes[k+1];
pCutNew->pNodes[k] = Node;
break;
}
if ( i == (int)pCutNew->nNodes ) // new node
{
pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;

16
src/opt/lpk/lpkInt.h
View File

@ -122,14 +122,14 @@ struct Lpk_Man_t_
typedef struct Lpk_Fun_t_ Lpk_Fun_t;
struct Lpk_Fun_t_
{
Vec_Ptr_t * vNodes; // the array of all functions
unsigned int Id : 5; // the ID of this node
Vec_Ptr_t * vNodes; // the array of leaves and decomposition nodes
unsigned int Id : 8; // the ID of this node
unsigned int nVars : 5; // the number of variables
unsigned int nLutK : 4; // the number of LUT inputs
unsigned int nAreaLim : 8; // the area limit (the largest allowed)
unsigned int nAreaLim : 5; // the area limit (the largest allowed)
unsigned int nDelayLim : 10; // the delay limit (the largest allowed)
char pFanins[16]; // the fanins of this function
char pDelays[16]; // the delays of the inputs
char pFanins[16]; // the fanins of this function
unsigned uSupp; // the support of this component
unsigned pTruth[0]; // the truth table (contains room for three truth tables)
};
@ -146,6 +146,8 @@ struct Lpk_Res_t_
int nSuppSizeL; // support size of the larger (composition) function
int DelayEst; // estimated delay of the decomposition
int AreaEst; // estimated area of the decomposition
int Variable; // variable in MUX decomposition
int Polarity; // polarity in MUX decomposition
};
static inline int Lpk_LutNumVars( int nLutsLim, int nLutK ) { return nLutsLim * (nLutK - 1) + 1; }
@ -177,11 +179,11 @@ static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num ) { assert( Num
/*=== lpkAbcDec.c ============================================================*/
extern Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
/*=== lpkAbcDsd.c ============================================================*/
extern Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth );
extern Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p );
extern Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
/*=== lpkAbcMux.c ============================================================*/
extern int Lpk_MuxAnalize( Lpk_Fun_t * p );
extern Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int VarPol );
extern Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p );
extern Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol );
/*=== lpkAbcUtil.c ============================================================*/
extern Lpk_Fun_t * Lpk_FunAlloc( int nVars );
extern void Lpk_FunFree( Lpk_Fun_t * p );

3
src/opt/lpk/lpkMux.c
View File

@ -167,6 +167,8 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I
ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
// Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[0], uSubset0, iVarReused, pCo0, pDec0 );
// Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[1], uSubset1, iVarReused, pCo1, pDec1 );
Kit_DsdNtkFree( ppNtks[0] );
Kit_DsdNtkFree( ppNtks[1] );
//Kit_DsdPrintFromTruth( pDec0, nVars );
@ -218,6 +220,7 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I
Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
//Kit_DsdPrintFromTruth( pCo0, nVars );
//Kit_DsdPrintFromTruth( pCo1, nVars );
// derive the composition function
Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );

202
src/sat/bsat/satSolver.c
View File

@ -27,7 +27,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satSolver.h"
//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
#define WATCHFLAG 1
//=================================================================================================
// Debug:
@ -91,11 +90,9 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[
//=================================================================================================
// Encode literals in clause pointers:
static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
static clause* clause_from_lit2(lit l) { return (clause*)(unsigned long)l; }
static lit clause_read_lit2(clause* c) { return (lit)(unsigned long)c; }
//=================================================================================================
// Simple helpers:
@ -111,15 +108,6 @@ static inline void vecp_remove(vecp* v, void* e)
for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
vecp_resize(v,vecp_size(v)-1);
}
static inline void vecp_remove2(vecp* v, void* e)
{
void** ws = vecp_begin(v);
int j = 0;
for (; ws[j] != e ; j++);
assert(j < vecp_size(v));
for (; j < vecp_size(v)-2; j++) ws[j] = ws[j+2];
vecp_resize(v,vecp_size(v)-2);
}
//=================================================================================================
// Variable order functions:
@ -316,26 +304,8 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
//vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
//vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
if ( WATCHFLAG )
{
if ( size == 2 )
{
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit(begin[1]));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit(begin[0]));
}
else
{
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit2(begin[1]));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit2(begin[0]));
}
}
else
{
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
}
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
return c;
}
@ -351,24 +321,8 @@ static void clause_remove(sat_solver* s, clause* c)
//vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
assert(lits[0] < s->size*2);
if ( WATCHFLAG )
{
if ( clause_size(c) == 2 )
{
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)clause_from_lit(lits[1]));
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)clause_from_lit(lits[0]));
}
else
{
vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
}
}
else
{
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
}
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
if (clause_learnt(c)){
s->stats.learnts--;
@ -749,31 +703,6 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
}
void sat_solver_check(sat_solver* s)
{
int j, k;
lit Lit, First, *lits;
vecp* ws;
clause **begin, **end, **i;
for ( j = 0; j < s->size; j++ )
for ( k = 0; k < 2; k++ )
{
Lit = toLitCond( j, k );
ws = sat_solver_read_wlist(s,Lit);
begin = (clause**)vecp_begin(ws);
end = begin + vecp_size(ws);
for (i = begin; i < end; i++)
{
if (clause_is_lit(*i))
continue;
lits = clause_begin(*i);
First = clause_read_lit2(*(i+1));
assert( First == lits[0] || First == lits[1] );
i++;
}
}
}
clause* sat_solver_propagate(sat_solver* s)
{
lbool* values = s->assigns;
@ -787,19 +716,15 @@ clause* sat_solver_propagate(sat_solver* s)
clause **begin = (clause**)vecp_begin(ws);
clause **end = begin + vecp_size(ws);
clause **i, **j;
// sat_solver_check(s);
s->stats.propagations++;
s->simpdb_props--;
//printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
for (i = j = begin; i < end; i++)
{
if (clause_is_lit(*i))
{
for (i = j = begin; i < end; ){
if (clause_is_lit(*i)){
*j++ = *i;
if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p)))
{
if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
confl = s->binary;
(clause_begin(confl))[1] = lit_neg(p);
(clause_begin(confl))[0] = clause_read_lit(*i++);
@ -808,27 +733,13 @@ clause* sat_solver_propagate(sat_solver* s)
while (i < end)
*j++ = *i++;
}
}
else
{
lit false_lit, first;
}else{
lit false_lit;
lbool sig;
if ( WATCHFLAG )
{
first = clause_read_lit2(*(i+1));
sig = !lit_sign(first); sig += sig - 1;
if (values[lit_var(first)] == sig)
{
*j++ = *i++;
*j++ = *i;
continue;
}
}
lits = clause_begin(*i);
// Make sure the false literal is in data[1]:
// Make sure the false literal is data[1]:
false_lit = lit_neg(p);
if (lits[0] == false_lit){
lits[0] = lits[1];
@ -837,95 +748,35 @@ clause* sat_solver_propagate(sat_solver* s)
assert(lits[1] == false_lit);
//printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
if ( WATCHFLAG )
{
/*
// If 0th watch is true, then clause is already satisfied.
sig = !lit_sign(lits[0]); sig += sig - 1;
if (values[lit_var(lits[0])] == sig)
{
*j++ = *i++;
*j++ = *i;
continue;
}
else
*/
{
// If 0th watch is true, then clause is already satisfied.
sig = !lit_sign(lits[0]); sig += sig - 1;
if (values[lit_var(lits[0])] == sig){
*j++ = *i;
}else{
// Look for new watch:
lit* stop = lits + clause_size(*i);
lit* k;
// assert( lits[0] == first );
for (k = lits + 2; k < stop; k++)
{
for (k = lits + 2; k < stop; k++){
lbool sig = lit_sign(*k); sig += sig - 1;
if (values[lit_var(*k)] != sig)
{
if (values[lit_var(*k)] != sig){
lits[1] = *k;
*k = false_lit;
// vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i++);
vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),clause_from_lit2(lits[0]));
break;
}
vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
goto next; }
}
if ( k < stop )
continue;
*j++ = *i;
// Clause is unit under assignment:
if (!enqueue(s,lits[0], *i))
{
if (!enqueue(s,lits[0], *i)){
confl = *i++;
*j++ = clause_from_lit2(lits[0]); i++; //
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
else
{
*j++ = clause_from_lit2(lits[0]); i++; //
}
}
}
else
{
// If 0th watch is true, then clause is already satisfied.
sig = !lit_sign(lits[0]); sig += sig - 1;
if (values[lit_var(lits[0])] == sig)
{
*j++ = *i;
}
else
{
// Look for new watch:
lit* stop = lits + clause_size(*i);
lit* k;
for (k = lits + 2; k < stop; k++)
{
lbool sig = lit_sign(*k); sig += sig - 1;
if (values[lit_var(*k)] != sig)
{
lits[1] = *k;
*k = false_lit;
vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
break;
}
}
if ( k < stop )
continue;
*j++ = *i;
// Clause is unit under assignment:
if (!enqueue(s,lits[0], *i))
{
confl = *i++;
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
}
}
}
next:
i++;
}
s->stats.inspects += j - (clause**)vecp_begin(ws);
@ -944,7 +795,7 @@ void sat_solver_reducedb(sat_solver* s)
double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
clause** learnts = (clause**)vecp_begin(&s->learnts);
clause** reasons = s->reasons;
//printf( "Trying to reduce DB\n" );
sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
@ -1037,10 +888,8 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
}
if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
{
// Simplify the set of problem clauses:
sat_solver_simplify(s);
}
if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
// Reduce the set of learnt clauses:
@ -1271,7 +1120,6 @@ bool sat_solver_simplify(sat_solver* s)
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
return true;
//printf( "Trying to simplify\n" );
reasons = s->reasons;
for (type = 0; type < 2; type++){