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

Version abc90408

This commit is contained in:
Alan Mishchenko 2009-04-08 08:01:00 -07:00
parent e3e2918eb8
commit df6fdd1dff
134 changed files with 1315 additions and 413 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -3683,6 +3683,10 @@ SOURCE=.\src\aig\gia\giaAig.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAig.h
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAiger.c
# End Source File
# Begin Source File

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

@ -215,11 +215,6 @@ static inline Aig_Cut_t * Aig_CutNext( Aig_Cut_t * pCut ) { return
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
#define AIG_MAX(a,b) (((a) > (b))? (a) : (b))
#define AIG_ABS(a) (((a) >= 0)? (a) :-(a))
#define AIG_INFINITY (100000000)
static inline int Aig_IntAbs( int n ) { return (n < 0)? -n : n; }
static inline int Aig_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Aig_Int2Float( int Num ) { return *((float *)&Num); }
@ -320,7 +315,7 @@ static inline Aig_Obj_t * Aig_ObjChild1Next( Aig_Obj_t * pObj ) { assert( !Aig
static inline void Aig_ObjChild0Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin0 = Aig_Not(pObj->pFanin0); }
static inline void Aig_ObjChild1Flip( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); pObj->pFanin1 = Aig_Not(pObj->pFanin1); }
static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level; }
static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(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 int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + ABC_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
static inline int Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i; }
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); }
@ -483,6 +478,7 @@ extern Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos );
extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide );

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

@ -407,7 +407,7 @@ int Aig_ManLevelNum( Aig_Man_t * p )
int i, LevelsMax;
LevelsMax = 0;
Aig_ManForEachPo( p, pObj, i )
LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
LevelsMax = ABC_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
return LevelsMax;
}

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

@ -18,7 +18,7 @@
***********************************************************************/
#include "aig.h"
#include "saig.h"
#include "tim.h"
////////////////////////////////////////////////////////////////////////
@ -301,6 +301,52 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
printf( "Aig_ManDupOrdered(): The check has failed.\n" );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description [Assumes topological ordering of the nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjNew;
int i, nNodes;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
// create the PIs
Aig_ManCleanData( p );
// duplicate internal nodes
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjIsNode(pObj) )
pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
else if ( Aig_ObjIsPi(pObj) )
pObjNew = (Aig_ObjRefs(pObj) > 0 || Saig_ObjIsLo(p, pObj)) ? Aig_ObjCreatePi(pNew) : NULL;
else if ( Aig_ObjIsPo(pObj) )
pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
else if ( Aig_ObjIsConst1(pObj) )
pObjNew = Aig_ManConst1(pNew);
else
assert( 0 );
pObj->pData = pObjNew;
}
assert( Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
if ( (nNodes = Aig_ManCleanup( pNew )) )
printf( "Aig_ManDupTrim(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
// check the resulting network
if ( !Aig_ManCheck(pNew) )
printf( "Aig_ManDupTrim(): The check has failed.\n" );
return pNew;
}
/**Function*************************************************************

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

@ -109,7 +109,7 @@ void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
assert( pFanout->Id > 0 );
if ( pObj->Id >= p->nFansAlloc || pFanout->Id >= p->nFansAlloc )
{
int nFansAlloc = 2 * AIG_MAX( pObj->Id, pFanout->Id );
int nFansAlloc = 2 * ABC_MAX( pObj->Id, pFanout->Id );
p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc );
memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
p->nFansAlloc = nFansAlloc;

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

@ -266,13 +266,13 @@ int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
// dereference the current cut
LevelMax = 0;
Vec_PtrForEachEntry( vLeaves, pObj, i )
LevelMax = AIG_MAX( LevelMax, (int)pObj->Level );
LevelMax = ABC_MAX( LevelMax, (int)pObj->Level );
if ( LevelMax == 0 )
return 0;
// dereference the cut
ConeSize1 = Aig_NodeDeref_rec( pNode, 0, NULL, NULL );
// try expanding each node in the boundary
ConeBest = AIG_INFINITY;
ConeBest = ABC_INFINITY;
pLeafBest = NULL;
Vec_PtrForEachEntry( vLeaves, pObj, i )
{

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

@ -529,7 +529,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
if ( p->pFanData && Aig_ObjIsBuf(pObjOld) )
{
Vec_PtrPush( p->vBufs, pObjOld );
p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
p->nBufMax = ABC_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
Aig_ManPropagateBuffers( p, fUpdateLevel );
}
}

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

@ -39,7 +39,7 @@ struct Aig_ManPre_t_
// info about the current partition
Vec_Int_t * vRegs; // registers of this partition
Vec_Int_t * vUniques; // unique registers of this partition
Vec_Int_t * vFreeVars; // ABC_FREE variables of this partition
Vec_Int_t * vFreeVars; // free variables of this partition
Vec_Flt_t * vPartCost; // costs of adding each variable
char * pfPartVars; // input/output registers of the partition
};
@ -153,7 +153,7 @@ int Aig_ManRegFindSeed( Aig_ManPre_t * p )
int Aig_ManRegFindBestVar( Aig_ManPre_t * p )
{
Vec_Int_t * vSupp;
int nNewVars, nNewVarsBest = AIG_INFINITY;
int nNewVars, nNewVarsBest = ABC_INFINITY;
int iVarFree, iVarSupp, iVarBest = -1, i, k;
// go through the ABC_FREE variables
Vec_IntForEachEntry( p->vFreeVars, iVarFree, i )

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

@ -173,7 +173,7 @@ void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
assert( pEdge->nLats == 10 );
if ( p->nExtraCur + 1 > p->nExtraAlloc )
{
int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 );
int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 );
p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew );
p->nExtraAlloc = nExtraAllocNew;
}
@ -199,7 +199,7 @@ void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
nWords = (pEdge->nLats + 1) >> 4;
if ( p->nExtraCur + nWords + 1 > p->nExtraAlloc )
{
int nExtraAllocNew = AIG_MAX( 2 * p->nExtraAlloc, 1024 );
int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 );
p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew );
p->nExtraAlloc = nExtraAllocNew;
}
@ -357,7 +357,7 @@ int Rtm_ManLatchMax( Rtm_Man_t * p )
assert( Val == 1 || Val == 2 );
}
*/
nLatchMax = AIG_MAX( nLatchMax, (int)pEdge->nLats );
nLatchMax = ABC_MAX( nLatchMax, (int)pEdge->nLats );
}
return nLatchMax;
}
@ -474,7 +474,7 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
Rtm_Obj_t * pFanin;
int i, Degree = 0;
Rtm_ObjForEachFanin( pObj, pFanin, i )
Degree = AIG_MAX( Degree, (int)pFanin->Num );
Degree = ABC_MAX( Degree, (int)pFanin->Num );
return Degree + 1;
}
@ -494,7 +494,7 @@ int Rtm_ObjGetDegreeBwd( Rtm_Obj_t * pObj )
Rtm_Obj_t * pFanout;
int i, Degree = 0;
Rtm_ObjForEachFanout( pObj, pFanout, i )
Degree = AIG_MAX( Degree, (int)pFanout->Num );
Degree = ABC_MAX( Degree, (int)pFanout->Num );
return Degree + 1;
}
@ -907,7 +907,7 @@ clk = clock();
if ( !Rtm_ObjCheckRetimeFwd( pNext ) ) // skip non-retimable
continue;
Degree = Rtm_ObjGetDegreeFwd( pNext );
DegreeMax = AIG_MAX( DegreeMax, Degree );
DegreeMax = ABC_MAX( DegreeMax, Degree );
if ( Degree > nStepsMax ) // skip nodes with high degree
continue;
pNext->fMark = 1;
@ -928,7 +928,7 @@ clk = clock();
if ( !Rtm_ObjCheckRetimeBwd( pNext ) ) // skip non-retimable
continue;
Degree = Rtm_ObjGetDegreeBwd( pNext );
DegreeMax = AIG_MAX( DegreeMax, Degree );
DegreeMax = ABC_MAX( DegreeMax, Degree );
if ( Degree > nStepsMax ) // skip nodes with high degree
continue;
pNext->fMark = 1;

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

@ -118,7 +118,7 @@ int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj )
Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
{
LevelCur = Aig_ObjReverseLevel( p, pFanout );
Level = AIG_MAX( Level, LevelCur );
Level = ABC_MAX( Level, LevelCur );
}
return Level + 1;
}

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

@ -114,7 +114,7 @@ int Aig_ManLevels( Aig_Man_t * p )
Aig_Obj_t * pObj;
int i, LevelMax = 0;
Aig_ManForEachPo( p, pObj, i )
LevelMax = AIG_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
LevelMax = ABC_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
return LevelMax;
}
@ -1255,7 +1255,7 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
Vec_PtrGrow( vArr, AIG_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
Vec_PtrGrow( vArr, ABC_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
pBeg = (Aig_Obj_t **)vArr->pArray;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{

98
src/aig/bbr/bbrReach.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "bbr.h"
#include "ssw.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -180,7 +181,7 @@ DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder,
bVar = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i );
pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) ); Cudd_Ref( pbParts[i] );
}
// ABC_FREE global BDDs
// free global BDDs
Aig_ManFreeGlobalBdds( p, dd );
// reorder and disable reordering
@ -220,9 +221,6 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
int nThreshold = 10000;
Vec_Ptr_t * vOnionRings;
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
// start the image computation
bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs );
if ( fPartition )
@ -237,6 +235,9 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
return -1;
}
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
// perform reachability analisys
bCurrent = bInitial; Cudd_Ref( bCurrent );
bReached = bInitial; Cudd_Ref( bReached );
@ -256,6 +257,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
Bbr_bddImageTreeDelete( pTree );
else
Bbr_bddImageTreeDelete2( pTree2 );
Vec_PtrFree( vOnionRings );
return -1;
}
Cudd_Ref( bNext );
@ -316,7 +318,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
fprintf( stdout, "\r" );
}
Cudd_RecursiveDeref( dd, bNext );
// ABC_FREE the onion rings
// free the onion rings
Vec_PtrForEachEntry( vOnionRings, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrFree( vOnionRings );
@ -353,7 +355,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
/**Function*************************************************************
Synopsis [Performs reachability to see if any .]
Synopsis [Performs reachability to see if any PO can be asserted.]
Description []
@ -362,7 +364,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
SeeAlso []
***********************************************************************/
int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
{
DdManager * dd;
DdNode ** pbParts, ** pbOutputs;
@ -372,9 +374,6 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
assert( Saig_ManRegNum(p) > 0 );
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
// compute the global BDDs of the latches
dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );
if ( dd == NULL )
@ -386,6 +385,9 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
if ( fVerbose )
printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
// start the onion rings
vOnionRings = Vec_PtrAlloc( 1000 );
// save outputs
pbOutputs = Aig_ManCreateOutputs( dd, p );
@ -413,7 +415,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
break;
}
}
// ABC_FREE the onion rings
// free the onion rings
Vec_PtrForEachEntry( vOnionRings, bTemp, i )
Cudd_RecursiveDeref( dd, bTemp );
Vec_PtrFree( vOnionRings );
@ -443,6 +445,80 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
return RetValue;
}
/**Function*************************************************************
Synopsis [Performs reachability to see if any PO can be asserted.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
{
Ssw_Cex_t * pCexOld, * pCexNew;
Aig_Man_t * p;
Aig_Obj_t * pObj;
Vec_Int_t * vInputMap;
int i, k, Entry, iBitOld, iBitNew, RetValue;
// check if there are PIs without fanout
Saig_ManForEachPi( pInit, pObj, i )
if ( Aig_ObjRefs(pObj) == 0 )
break;
if ( i == Saig_ManPiNum(pInit) )
return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
// create new AIG
p = Aig_ManDupTrim( pInit );
assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) );
assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
if ( RetValue != 0 )
{
Aig_ManStop( p );
return RetValue;
}
// the problem is satisfiable - remap the pattern
pCexOld = p->pSeqModel;
assert( pCexOld != NULL );
// create input map
vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
Saig_ManForEachPi( pInit, pObj, i )
if ( pObj->pData != NULL )
Vec_IntPush( vInputMap, Aig_ObjPioNum(pObj->pData) );
else
Vec_IntPush( vInputMap, -1 );
// create new pattern
pCexNew = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
pCexNew->iFrame = pCexOld->iFrame;
pCexNew->iPo = pCexOld->iPo;
// copy the bit-data
for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ )
if ( Aig_InfoHasBit( pCexOld->pData, iBitOld ) )
Aig_InfoSetBit( pCexNew->pData, iBitOld );
// copy the primary input data
iBitNew = iBitOld;
for ( i = 0; i <= pCexNew->iFrame; i++ )
{
Vec_IntForEachEntry( vInputMap, Entry, k )
{
if ( Entry == -1 )
continue;
if ( Aig_InfoHasBit( pCexOld->pData, iBitOld + Entry ) )
Aig_InfoSetBit( pCexNew->pData, iBitNew + k );
}
iBitOld += Saig_ManPiNum(p);
iBitNew += Saig_ManPiNum(pInit);
}
assert( iBitOld < iBitNew );
assert( iBitOld == pCexOld->nBits );
assert( iBitNew == pCexNew->nBits );
Vec_IntFree( vInputMap );
pInit->pSeqModel = pCexNew;
Aig_ManStop( p );
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

3
src/aig/cec/cecCec.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "cecInt.h"
#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -44,7 +45,7 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
int i;
assert( p->pCexComb == NULL );
p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char,
sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p)) );
sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p)) );
p->pCexComb->iPo = iOut;
p->pCexComb->nPis = Gia_ManCiNum(p);
p->pCexComb->nBits = Gia_ManCiNum(p);

26
src/aig/cec/cecClass.c
View File

@ -111,14 +111,14 @@ int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords )
{
for ( w = 0; w < nWords; w++ )
if ( p[w] != ~0 )
return 32*w + Aig_WordFindFirstBit( ~p[w] );
return 32*w + Gia_WordFindFirstBit( ~p[w] );
return -1;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( p[w] != 0 )
return 32*w + Aig_WordFindFirstBit( p[w] );
return 32*w + Gia_WordFindFirstBit( p[w] );
return -1;
}
}
@ -141,14 +141,14 @@ int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
{
for ( w = 0; w < nWords; w++ )
if ( p0[w] != p1[w] )
return 32*w + Aig_WordFindFirstBit( p0[w] ^ p1[w] );
return 32*w + Gia_WordFindFirstBit( p0[w] ^ p1[w] );
return -1;
}
else
{
for ( w = 0; w < nWords; w++ )
if ( p0[w] != ~p1[w] )
return 32*w + Aig_WordFindFirstBit( p0[w] ^ ~p1[w] );
return 32*w + Gia_WordFindFirstBit( p0[w] ^ ~p1[w] );
return -1;
}
}
@ -467,7 +467,7 @@ void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined )
int * pTable, nTableSize, i, k, Key;
if ( Vec_IntSize(vRefined) == 0 )
return;
nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
nTableSize = Gia_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
pTable = ABC_CALLOC( int, nTableSize );
Vec_IntForEachEntry( vRefined, i, k )
{
@ -519,15 +519,15 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
assert( p->pCexComb == NULL );
assert( iPat >= 0 && iPat < 32 * p->nWords );
p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char,
sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p->pAig)) );
sizeof(Gia_Cex_t) + sizeof(unsigned) * Gia_BitWordNum(Gia_ManCiNum(p->pAig)) );
p->pCexComb->iPo = p->iOut;
p->pCexComb->nPis = Gia_ManCiNum(p->pAig);
p->pCexComb->nBits = Gia_ManCiNum(p->pAig);
for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
{
pInfo = Vec_PtrEntry( p->vCiSimInfo, i );
if ( Aig_InfoHasBit( pInfo, iPat ) )
Aig_InfoSetBit( p->pCexComb->pData, i );
if ( Gia_InfoHasBit( pInfo, iPat ) )
Gia_InfoSetBit( p->pCexComb->pData, i );
}
}
@ -560,8 +560,8 @@ void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
pInfo = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
if ( Aig_InfoHasBit(p->pBestState->pData, i) != Aig_InfoHasBit(pInfo, iPatBest) )
Aig_InfoXorBit( p->pBestState->pData, i );
if ( Gia_InfoHasBit(p->pBestState->pData, i) != Gia_InfoHasBit(pInfo, iPatBest) )
Gia_InfoXorBit( p->pBestState->pData, i );
}
p->pBestState->iPo = ScoreBest;
}
@ -686,7 +686,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
else
{
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = Aig_ManRandom( 0 );
pRes[w] = Gia_ManRandom( 0 );
}
// make sure the first pattern is always zero
pRes[1] ^= (pRes[1] & 1);
@ -798,7 +798,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
{
pRes0 = Vec_PtrEntry( vInfoCis, i );
for ( w = 0; w < p->nWords; w++ )
pRes0[w] = Aig_ManRandom( 0 );
pRes0[w] = Gia_ManRandom( 0 );
}
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
@ -814,7 +814,7 @@ void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * v
{
pRes0 = Vec_PtrEntry( vInfoCis, i );
for ( w = 0; w < p->nWords; w++ )
pRes0[w] = Aig_ManRandom( 0 );
pRes0[w] = Gia_ManRandom( 0 );
}
}
}

12
src/aig/cec/cecCore.c
View File

@ -246,7 +246,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
if ( pPars->fSeqSimulate )
printf( "Performing sequential simulation of %d frames with %d words.\n",
pPars->nRounds, pPars->nWords );
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
pSim = Cec_ManSimStart( pAig, pPars );
if ( pAig->pReprs == NULL )
RetValue = Cec_ManSimClassesPrepare( pSim );
@ -283,7 +283,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
double clkTotal = clock();
// duplicate AIG and transfer equivalence classes
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
pIni = Gia_ManDup(pAig);
pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
@ -420,7 +420,8 @@ p->timeSat += clock() - clk;
printf( "Switching into reduced mode.\n" );
pPars->fColorDiff = 0;
}
if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
// if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) )
{
if ( p->pPars->fVerbose )
printf( "Switching into normal mode.\n" );
@ -431,6 +432,11 @@ p->timeSat += clock() - clk;
finalize:
if ( p->pPars->fVerbose )
{
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig),
100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig),
100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal );
ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal );
ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal );

148
src/aig/cec/cecCorr.c
View File

@ -49,6 +49,11 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f );
return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
}
if ( f == 0 )
{
assert( Gia_ObjIsRo(p, pObj) );
return Gia_ObjCopyF(p, f, pObj);
}
assert( f && Gia_ObjIsRo(p, pObj) );
pObj = Gia_ObjRoToRi( p, pObj );
Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 );
@ -107,7 +112,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
Gia_ManForEachRo( p, pObj, i )
@ -200,6 +205,74 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
}
/**Function*************************************************************
Synopsis [Derives SRM for signal correspondence.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pRepr;
Vec_Int_t * vXorLits;
int f, i, iPrevNew, iObjNew;
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) );
assert( Gia_ManRegNum(p) > 0 );
assert( p->pReprs != NULL );
p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
Gia_ManSetPhase( p );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
{
Gia_ManAppendCi(pNew);
Gia_ObjSetCopyF( p, 0, pObj, 0 );
}
for ( f = 0; f < nFrames+fScorr; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
Gia_ManForEachPi( p, pObj, i )
Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
}
*pvOutputs = Vec_IntAlloc( 1000 );
vXorLits = Vec_IntAlloc( 1000 );
for ( f = 0; f < nFrames; f++ )
{
Gia_ManForEachObj1( p, pObj, i )
{
pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
if ( pRepr == NULL )
continue;
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f );
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f );
iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
if ( iPrevNew != iObjNew )
{
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
}
}
}
Vec_IntForEachEntry( vXorLits, iObjNew, i )
Gia_ManAppendCo( pNew, iObjNew );
Vec_IntFree( vXorLits );
Gia_ManHashStop( pNew );
ABC_FREE( p->pCopies );
//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
pNew = Gia_ManCleanup( pTemp = pNew );
//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
@ -227,7 +300,7 @@ void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Aig_ManRandom( 0 );
pInfo[w] = Gia_ManRandom( 0 );
}
}
@ -351,17 +424,17 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Aig_InfoHasBit( pPres, iBit ) &&
Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
if ( Gia_InfoHasBit( pPres, iBit ) &&
Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
Aig_InfoSetBit( pPres, iBit );
if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Aig_InfoXorBit( pInfo, iBit );
Gia_InfoSetBit( pPres, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Gia_InfoXorBit( pInfo, iBit );
}
return 1;
}
@ -403,7 +476,7 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
for ( k = 1; k < nBits; k++ )
if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
kMax = AIG_MAX( kMax, k );
kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
break;
}
@ -443,8 +516,8 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
{
iLit = Vec_IntEntry( vCexStore, iStart++ );
pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
Aig_InfoXorBit( pInfo, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
Gia_InfoXorBit( pInfo, iBit );
}
if ( ++iBit == nBits )
break;
@ -591,7 +664,11 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
}
CounterX -= Gia_ManCoNum(p);
nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
printf( "%3d : c =%8d cl =%7d lit =%8d ", iIter, Counter0, Counter, nLits );
if ( iIter == -1 )
printf( "BMC : " );
else
printf( "%3d : ", iIter );
printf( "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
if ( vStatus )
Vec_StrForEachEntry( vStatus, Entry, i )
{
@ -638,7 +715,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
return NULL;
}
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
// prepare simulation manager
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nWords = pPars->nWords;
@ -704,14 +781,57 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
}
// check the base case
if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
{
int fChanges = 1;
while ( fChanges )
{
int clkBmc = clock();
fChanges = 0;
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
if ( Gia_ManPoNum(pSrm) == 0 )
{
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
break;
}
pParsSat->nBTLimit *= 10;
if ( pPars->fUseCSat )
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
else
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
// refine classes with these counter-examples
if ( Vec_IntSize(vCexStore) )
{
clk2 = clock();
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
clkSim += clock() - clk2;
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
fChanges = 1;
}
if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, vStatus, -1, clock() - clkBmc );
// recycle
Vec_IntFree( vCexStore );
Vec_StrFree( vStatus );
Gia_ManStop( pSrm );
Vec_IntFree( vOutputs );
}
}
else
{
if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
}
// check the overflow
if ( r == 100000 )
printf( "The refinement was not finished. The result may be incorrect.\n" );
Cec_ManSimStop( pSim );
clkTotal = clock() - clkTotal;
if ( pPars->fVerbose )
Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
// derive reduced AIG
Gia_ManSetProvedNodes( pAig );
Gia_ManEquivImprove( pAig );
pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
pNew = Gia_ManSeqCleanup( pTemp = pNew );

4
src/aig/cec/cecIso.c
View File

@ -125,7 +125,7 @@ static inline void Gia_ManIsoRandom( int Id, unsigned * pStore, int nWords )
unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id );
int w;
for ( w = 0; w < nWords; w++ )
pInfo0[w] = Aig_ManRandom( 0 );
pInfo0[w] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@ -314,7 +314,7 @@ int * Cec_ManDetectIsomorphism( Gia_Man_t * p )
// start simulation info
pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords );
// simulate and create table
nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
nTableSize = Gia_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
pTable = ABC_CALLOC( int, nTableSize );
Gia_ManCleanValue( p );
Gia_ManForEachObj1( p, pObj, i )

22
src/aig/cec/cecPat.c
View File

@ -414,17 +414,17 @@ int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int *
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
if ( Aig_InfoHasBit( pPres, iBit ) &&
Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
if ( Gia_InfoHasBit( pPres, iBit ) &&
Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
return 0;
}
for ( i = 0; i < nLits; i++ )
{
pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
Aig_InfoSetBit( pPres, iBit );
if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Aig_InfoXorBit( pInfo, iBit );
Gia_InfoSetBit( pPres, iBit );
if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
Gia_InfoXorBit( pInfo, iBit );
}
return 1;
}
@ -450,7 +450,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW
int nBits = 32 * nWords;
int clk = clock();
vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
Aig_ManRandomInfo( vInfo, 0, 0, nWords );
Gia_ManRandomInfo( vInfo, 0, 0, nWords );
vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
@ -460,11 +460,11 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nW
for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
break;
kMax = AIG_MAX( kMax, k );
kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
{
Vec_PtrReallocSimInfo( vInfo );
Aig_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
Gia_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
Vec_PtrReallocSimInfo( vPres );
Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
nWords *= 2;
@ -511,7 +511,7 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg
vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vInfo, 0, nWords );
Aig_ManRandomInfo( vInfo, nRegs, 0, nWords );
Gia_ManRandomInfo( vInfo, nRegs, 0, nWords );
vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
Vec_PtrCleanSimInfo( vPres, 0, nWords );
@ -538,12 +538,12 @@ Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nReg
// RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) );
// assert( RetValue == 1 );
kMax = AIG_MAX( kMax, k );
kMax = ABC_MAX( kMax, k );
if ( k == nBits-1 )
{
Vec_PtrReallocSimInfo( vInfo );
Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords );
Aig_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
Gia_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
Vec_PtrReallocSimInfo( vPres );
Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );

16
src/aig/cec/cecSeq.c
View File

@ -51,7 +51,7 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0;
}
*/
for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
@ -65,16 +65,16 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t
{
pInfo = Vec_PtrEntry( vInfo, k++ );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Aig_ManRandom(0);
pInfo[w] = Gia_ManRandom(0);
// set simulation pattern and make sure it is second (first will be erased during simulation)
pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, i );
pInfo[0] = (pInfo[0] << 1) | Gia_InfoHasBit( pCex->pData, i );
pInfo[0] <<= 1;
}
for ( ; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Aig_ManRandom(0);
pInfo[w] = Gia_ManRandom(0);
}
}
@ -100,14 +100,14 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = (pCex && Aig_InfoHasBit(pCex->pData, k))? ~0 : 0;
pInfo[w] = (pCex && Gia_InfoHasBit(pCex->pData, k))? ~0 : 0;
}
for ( ; k < Vec_PtrSize(vInfo); k++ )
{
pInfo = Vec_PtrEntry( vInfo, k );
for ( w = 0; w < nWords; w++ )
pInfo[w] = Aig_ManRandom( 0 );
pInfo[w] = Gia_ManRandom( 0 );
}
}
@ -229,7 +229,7 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
}
if ( pPars->fVerbose )
printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 );
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 );
Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
@ -275,7 +275,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
return -1;
}
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
// prepare starting pattern
pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 );
pState->iFrame = -1;

6
src/aig/cec/cecSolve.c
View File

@ -369,7 +369,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
Cec_ObjSetSatNum( p, pObj, 0 );
Vec_PtrClear( p->vUsedNodes );
// memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
// memset( p->pSatVars, 0, sizeof(int) * Gia_ManObjNumMax(p->pAigTotal) );
sat_solver_delete( p->pSat );
}
p->pSat = sat_solver_new();
@ -636,8 +636,8 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb
if ( Gia_ObjIsCi(pObj) )
{
unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) )
Aig_InfoXorBit( pInfo, iPat );
if ( Cec_ObjSatVarValue( pSat, pObj ) != Gia_InfoHasBit( pInfo, iPat ) )
Gia_InfoXorBit( pInfo, iPat );
pSat->nCexLits++;
// Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
return;

6
src/aig/cec/cecSweep.c
View File

@ -50,7 +50,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
if ( p->pPars->nLevelMax )
Gia_ManLevelNum( p->pAig );
pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
pNew->pName = Aig_UtilStrsav( p->pAig->pName );
pNew->pName = Gia_UtilStrsav( p->pAig->pName );
Gia_ManHashAlloc( pNew );
piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
pDepths = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
@ -70,7 +70,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
pDepths[i] = ABC_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) )
continue;
assert( Gia_ObjRepr(p->pAig, i) < i );
@ -109,7 +109,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) );
Vec_IntPush( p->vXorNodes, i );
// add to the depth of this node
pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
pDepths[i] = 1 + ABC_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
piCopies[i] = -1;
}

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

@ -123,7 +123,7 @@ void Cnf_DeriveMapping( Cnf_Man_t * p )
// Aig_ObjCollectSuper( pObj, vSuper );
// get the area flow of this cut
// AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows );
AreaFlow = AIG_INFINITY;
AreaFlow = ABC_INFINITY;
if ( AreaFlow >= (int)pCutBest->uSign )
{
pAreaFlows[pObj->Id] = pCutBest->uSign;

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

@ -151,7 +151,7 @@ p->timeCuts += clock() - clk;
// evaluate the cuts
p->GainBest = -1;
Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
Dar_ObjForEachCut( pObj, pCut, k )
Dar_LibEval( p, pObj, pCut, Required );
// check the best gain
@ -292,7 +292,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose
Dar_ObjCutPrint( pAig, pObj );
*/
}
// ABC_FREE the cuts
// free the cuts
pMemCuts = p->pMemCuts;
p->pMemCuts = NULL;
// Dar_ManCutsFree( p );

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

@ -472,7 +472,7 @@ void Dar_LibPrepare( int nSubgraphs )
if ( i == 1 ) // special classes
p->nSubgr0[i] = p->nSubgr[i];
else
p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs );
p->nSubgr0[i] = ABC_MIN( p->nSubgr[i], nSubgraphs );
p->nSubgr0Total += p->nSubgr0[i];
for ( k = 0; k < p->nSubgr0[i]; k++ )
p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
@ -494,7 +494,7 @@ void Dar_LibPrepare( int nSubgraphs )
for ( k = 0; k < p->nSubgr0[i]; k++ )
Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
p->nNodes0Total += p->nNodes0[i];
p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] );
p->nNodes0Max = ABC_MAX( p->nNodes0Max, p->nNodes0[i] );
}
// clean node counters
@ -799,7 +799,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot )
assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level);
pData->Level = 1 + ABC_MAX(pData0->Level, pData1->Level);
if ( pData0->pFunc == NULL || pData1->pFunc == NULL )
continue;
pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 );

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

@ -267,7 +267,7 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, K
return -1;
}
// count the number of new levels
LevelNew = 1 + AIG_MAX( pNode0->Level, pNode1->Level );
LevelNew = 1 + ABC_MAX( pNode0->Level, pNode1->Level );
if ( pAnd )
{
if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) )
@ -527,7 +527,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
//printf( "\nConsidering node %d.\n", pObj->Id );
// get the bounded MFFC size
clk = clock();
nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 );
nLevelMin = ABC_MAX( 0, Aig_ObjLevel(pObj) - 10 );
nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
{
@ -564,7 +564,7 @@ p->timeCuts += clock() - clk;
// try the cuts
clk = clock();
Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
p->timeEval += clock() - clk;

2
src/aig/dch/dchClass.c
View File

@ -544,7 +544,7 @@ void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes,
{
int i, Limit;
Vec_PtrClear( vRoots );
Limit = AIG_MIN( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) );
Limit = ABC_MIN( pObj->Id + nNodes, Aig_ManObjNumMax(p->pAig) );
for ( i = pObj->Id; i < Limit; i++ )
{
pObj = Aig_ManObj( p->pAig, i );

4
src/aig/dch/dchSimSat.c
View File

@ -183,7 +183,7 @@ void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManResimulateSolved_rec( p, pObj );
Dch_ManResimulateSolved_rec( p, pRepr );
p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis );
// resimulate the cone of influence of the other nodes
Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
Dch_ManResimulateOther_rec( p, pRoot );
@ -233,7 +233,7 @@ void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManResimulateSolved_rec( p, pObj );
Dch_ManResimulateSolved_rec( p, pRepr );
p->nConeMax = AIG_MAX( p->nConeMax, p->nConeThis );
p->nConeMax = ABC_MAX( p->nConeMax, p->nConeThis );
// resimulate the cone of influence of the other nodes
Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
Dch_ManResimulateOther_rec( p, pRoot );

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

@ -360,7 +360,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
printf( "\n" );
}
// ABC_FREE the BMC manager
// free the BMC manager
Fra_BmcStop( p->pBmc );
p->pBmc = NULL;
}

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

@ -136,7 +136,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
{
pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
}
// ABC_FREE the sat_solver
// free the sat_solver
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
//sat_solver_store_write( pSat, "trace.cnf" );
@ -318,7 +318,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi
printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) );
fflush( stdout );
}
// ABC_FREE intermediate results
// free intermediate results
Vec_PtrForEachEntry( vParts, pAig, i )
Aig_ManStop( pAig );
Vec_PtrFree( vParts );

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

@ -652,7 +652,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
if ( pRepr == NULL )
continue;
pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
WeightMax = AIG_MAX( WeightMax, pWeights[i] );
WeightMax = ABC_MAX( WeightMax, pWeights[i] );
}
Fra_SmlStop( pComb );
printf( "Before: Const = %6d. Class = %6d. ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
@ -710,7 +710,7 @@ void Fra_ClassesSelectRepr( Fra_Cla_t * p )
// collect support sizes and find the min-support node
cMinSupp = -1;
pNodeMin = NULL;
nSuppSizeMin = AIG_INFINITY;
nSuppSizeMin = ABC_INFINITY;
for ( c = 0; pClass[c]; c++ )
{
nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );

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

@ -290,8 +290,8 @@ Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax,
***********************************************************************/
int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
{
int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
int Max1 = ABC_MAX( pImp1[0], pImp1[1] );
int Max2 = ABC_MAX( pImp2[0], pImp2[1] );
if ( Max1 < Max2 )
return -1;
if ( Max1 > Max2 )
@ -323,7 +323,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
Vec_Ptr_t * vNodes;
int * pImpCosts, * pNodesI, * pNodesK;
int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
int CostMin = AIG_INFINITY, CostMax = 0;
int CostMin = ABC_INFINITY, CostMax = 0;
int i, k, Imp, CostRange, clk = clock();
assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
@ -364,8 +364,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
nImpsCollected++;
Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
CostMin = ABC_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
CostMax = ABC_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
Vec_IntPush( vImps, Imp );
if ( Vec_IntSize(vImps) == nImpMaxLimit )
goto finish;
@ -508,7 +508,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
continue;
Left = Fra_ImpLeft(Imp);
Right = Fra_ImpRight(Imp);
Max = AIG_MAX( Left, Right );
Max = ABC_MAX( Left, Right );
assert( Max >= pNode->Id );
if ( Max > pNode->Id )
return i;

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

@ -629,7 +629,7 @@ p->timeTotal = clock() - clk;
p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
p->nRegsEnd = Aig_ManRegNum(pManAigNew);
// ABC_FREE the manager
// free the manager
finish:
Fra_ManStop( p );
// check the output

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

@ -539,7 +539,7 @@ clk = clock();
Aig_ManIncrementTravId( p->pManFraig );
// determine the min and max level to visit
assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
LevelMax = ABC_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
// traverse
if ( pOld && !Aig_ObjIsConst1(pOld) )

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

@ -170,7 +170,7 @@ clk = clock();
if ( RetValue == -1 && pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
TimeLeft = ABC_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
@ -240,7 +240,7 @@ ABC_PRT( "Time", clock() - clk );
if ( RetValue == -1 && pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
TimeLeft = ABC_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
@ -275,7 +275,7 @@ ABC_PRT( "Time", clock() - clk );
if ( RetValue == -1 && pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
TimeLeft = ABC_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )
@ -315,7 +315,7 @@ ABC_PRT( "Time", clock() - clk );
if ( RetValue == -1 && pParSec->TimeLimit )
{
TimeLeft = (float)pParSec->TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
TimeLeft = AIG_MAX( TimeLeft, 0.0 );
TimeLeft = ABC_MAX( TimeLeft, 0.0 );
if ( TimeLeft == 0.0 )
{
if ( !pParSec->fSilent )

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

@ -436,7 +436,7 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
Aig_ManForEachPi( p->pAig, pObj, i )
Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// flip one bit
Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
Limit = ABC_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
}
@ -458,7 +458,7 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
// flip one bit of the last frame
if ( fUseDist1 ) //&& p->nFrames == 2 )
{
Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
Limit = ABC_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
}

59
src/aig/gia/gia.h
View File

@ -24,8 +24,14 @@
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -124,6 +130,7 @@ struct Gia_Man_t_
int nFansAlloc; // the size of fanout representation
int * pMapping; // mapping for each node
Gia_Cex_t * pCexComb; // combinational counter-example
Gia_Cex_t * pCexSeq; // sequential counter-example
int * pCopies; // intermediate copies
Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc
unsigned char* pSwitching; // switching activity for each object
@ -174,6 +181,36 @@ extern void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p );
extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
static inline int Gia_IntAbs( int n ) { return (n < 0)? -n : n; }
static inline int Gia_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Gia_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Gia_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 Gia_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 * Gia_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; }
static inline int Gia_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Gia_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline int Gia_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); }
static inline int Gia_WordCountOnes( unsigned uWord )
{
uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
return (uWord & 0x0000FFFF) + (uWord>>16);
}
static inline int Gia_WordFindFirstBit( unsigned uWord )
{
int i;
for ( i = 0; i < 32; i++ )
if ( uWord & (1 << i) )
return i;
return -1;
}
static inline int Gia_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Gia_Lit2Var( int Lit ) { return Lit >> 1; }
@ -265,8 +302,8 @@ static inline int Gia_ObjValue( Gia_Obj_t * pObj ) {
static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pLevels);return p->pLevels[Gia_ObjId(p, pObj)]; }
static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; }
static inline void Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); p->pRefs[Gia_ObjId(p, pObj)]++; }
static inline void Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); p->pRefs[Gia_ObjId(p, pObj)]--; }
static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++; }
static inline int Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)]; }
static inline void Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj)); }
static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj)); }
static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); }
@ -368,6 +405,7 @@ static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { p
static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; }
static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; }
static inline void Gia_ObjUnsetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 0; }
static inline int Gia_ObjFailed( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fFailed; }
static inline void Gia_ObjSetFailed( Gia_Man_t * p, int Id ) { p->pReprs[Id].fFailed = 1; }
@ -451,10 +489,6 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== giaAig.c =============================================================*/
extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
/*=== giaAiger.c ===========================================================*/
extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck );
extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
@ -509,6 +543,7 @@ extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
extern void Gia_ManEquivImprove( Gia_Man_t * p );
/*=== giaFanout.c =========================================================*/
extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
extern void Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@ -530,7 +565,7 @@ extern int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
extern int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 );
extern int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 );
extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 );
extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash );
extern void Gia_ManHashProfile( Gia_Man_t * p );
/*=== giaLogic.c ===========================================================*/
extern void Gia_ManTestDistance( Gia_Man_t * p );
@ -567,6 +602,10 @@ extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames,
/*=== giaTsim.c ============================================================*/
extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
/*=== giaUtil.c ===========================================================*/
extern unsigned Gia_ManRandom( int fReset );
extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
extern unsigned int Gia_PrimeCudd( unsigned int p );
extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix );
extern void Gia_ManSetMark0( Gia_Man_t * p );
extern void Gia_ManCleanMark0( Gia_Man_t * p );
extern void Gia_ManCheckMark0( Gia_Man_t * p );
@ -589,7 +628,7 @@ extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t **
extern Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
extern int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut );
extern void Gia_ManPrintCounterExample( Gia_Cex_t * p );
extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
#ifdef __cplusplus
}

2
src/aig/gia/giaAig.c
View File

@ -18,7 +18,7 @@
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///

62
src/aig/gia/giaAig.h Normal file
View File

@ -0,0 +1,62 @@
/**CFile****************************************************************
FileName [giaAig.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __GIA_AIG_H__
#define __GIA_AIG_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig.h"
#include "gia.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== giaAig.c =============================================================*/
extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p );
extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p );
extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

6
src/aig/gia/giaAiger.c
View File

@ -143,7 +143,7 @@ int Gia_FileSize( char * pFileName )
char * Gia_FileNameGeneric( char * FileName )
{
char * pDot, * pRes;
pRes = Aig_UtilStrsav( FileName );
pRes = Gia_UtilStrsav( FileName );
if ( (pDot = strrchr( pRes, '.' )) )
*pDot = 0;
return pRes;
@ -412,7 +412,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
// allocate the empty AIG
pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
pName = Gia_FileNameGeneric( pFileName );
pNew->pName = Aig_UtilStrsav( pName );
pNew->pName = Gia_UtilStrsav( pName );
// pNew->pSpec = Aig_UtilStrsav( pFileName );
ABC_FREE( pName );
@ -549,7 +549,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
pCur++;
// read model name
ABC_FREE( pNew->pName );
pNew->pName = Aig_UtilStrsav( pCur );
pNew->pName = Gia_UtilStrsav( pCur );
}
}

3
src/aig/gia/giaCSat.c
View File

@ -20,6 +20,9 @@
#include "gia.h"
//#define gia_assert(exp) ((void)0)
//#define gia_assert(exp) (assert(exp))
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////

4
src/aig/gia/giaCof.c
View File

@ -580,7 +580,7 @@ void Cof_ManPrintFanio( Cof_Man_t * p )
}
// allocate storage for fanin/fanout numbers
nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
@ -714,7 +714,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
return NULL;
}
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;

38
src/aig/gia/giaDup.c
View File

@ -168,7 +168,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@ -200,7 +200,7 @@ Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCoReverse( p, pObj, i )
Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@ -232,7 +232,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -265,7 +265,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@ -297,7 +297,7 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i, iCtrl;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@ -337,7 +337,7 @@ Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass )
int i, Counter1 = 0, Counter2 = 0;
assert( p->vFlopClasses != NULL );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
@ -381,7 +381,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
int i, nRos = 0, nRis = 0;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{
@ -426,7 +426,7 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
int i, t, Entry;
assert( nTimes > 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes );
vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes );
@ -536,7 +536,7 @@ Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCo( p, pObj, i )
Gia_ManDupDfs2_rec( pNew, p, pObj );
@ -594,7 +594,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -625,7 +625,7 @@ Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -655,7 +655,7 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
assert( Gia_ObjIsCo(pRoot) );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -682,7 +682,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
int i, iLit, iLitRes;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -712,7 +712,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p )
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -743,7 +743,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos )
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManSetRefs( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -797,7 +797,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
{
@ -847,7 +847,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p )
assert( p->pReprsOld != NULL );
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
@ -1064,7 +1064,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq
}
// start the manager
pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
pNew->pName = Aig_UtilStrsav( "miter" );
pNew->pName = Gia_UtilStrsav( "miter" );
// map combinational inputs
Gia_ManFillValue( p0 );
Gia_ManFillValue( p1 );
@ -1161,7 +1161,7 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
int i, iLit;
assert( (Gia_ManPoNum(p) & 1) == 0 );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManHashAlloc( pNew );
Gia_ManForEachCi( p, pObj, i )

20
src/aig/gia/giaEmbed.c
View File

@ -691,7 +691,7 @@ void Emb_ManPrintFanio( Emb_Man_t * p )
}
// allocate storage for fanin/fanout numbers
nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );
@ -836,14 +836,14 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
int nAttempts = 20;
int i, iNode, Dist, clk;
Emb_Obj_t * pPivot, * pNext;
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
Emb_ManResetTravId( p );
// compute distances from several randomly selected PIs
clk = clock();
printf( "From inputs: " );
for ( i = 0; i < nAttempts; i++ )
{
iNode = Aig_ManRandom( 0 ) % Emb_ManCiNum(p);
iNode = Gia_ManRandom( 0 ) % Emb_ManCiNum(p);
pPivot = Emb_ManCi( p, iNode );
if ( Emb_ObjFanoutNum(pPivot) == 0 )
{ i--; continue; }
@ -859,7 +859,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
printf( "From outputs: " );
for ( i = 0; i < nAttempts; i++ )
{
iNode = Aig_ManRandom( 0 ) % Emb_ManCoNum(p);
iNode = Gia_ManRandom( 0 ) % Emb_ManCoNum(p);
pPivot = Emb_ManCo( p, iNode );
pNext = Emb_ObjFanin( pPivot, 0 );
if ( !Emb_ObjIsNode(pNext) )
@ -873,7 +873,7 @@ void Gia_ManTestDistanceInternal( Emb_Man_t * p )
printf( "From nodes: " );
for ( i = 0; i < nAttempts; i++ )
{
iNode = Aig_ManRandom( 0 ) % Gia_ManObjNum(p->pGia);
iNode = Gia_ManRandom( 0 ) % Gia_ManObjNum(p->pGia);
if ( !~Gia_ManObj(p->pGia, iNode)->Value )
{ i--; continue; }
pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value );
@ -1043,7 +1043,7 @@ Emb_Obj_t * Emb_ManRandomVertex( Emb_Man_t * p )
{
Emb_Obj_t * pPivot;
do {
int iNode = (911 * Aig_ManRandom(0)) % Gia_ManObjNum(p->pGia);
int iNode = (911 * Gia_ManRandom(0)) % Gia_ManObjNum(p->pGia);
if ( ~Gia_ManObj(p->pGia, iNode)->Value )
pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value );
else
@ -1240,7 +1240,7 @@ void Emb_ManVecRandom( float * pVec, int nDims )
{
int i;
for ( i = 0; i < nDims; i++ )
pVec[i] = Aig_ManRandom( 0 );
pVec[i] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@ -1702,7 +1702,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
printf( "Emb_ManDumpGnuplot(): Placement is not available.\n" );
return;
}
sprintf( Buffer, "%s%s", pDirectory, Aig_FileNameGenericAppend(pName, ".plt") );
sprintf( Buffer, "%s%s", pDirectory, Gia_FileNameGenericAppend(pName, ".plt") );
pFile = fopen( Buffer, "w" );
fprintf( pFile, "# This Gnuplot file was produced by ABC on %s\n", Ioa_TimeStamp() );
fprintf( pFile, "\n" );
@ -1712,7 +1712,7 @@ void Emb_ManDumpGnuplot( Emb_Man_t * p, char * pName, int fDumpLarge, int fShowI
{
// fprintf( pFile, "set terminal postscript\n" );
fprintf( pFile, "set terminal gif font \'arial\' 10 size 800,600 xffffff x000000 x000000 x000000\n" );
fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".gif") );
fprintf( pFile, "set output \'%s\'\n", Gia_FileNameGenericAppend(pName, ".gif") );
fprintf( pFile, "\n" );
}
fprintf( pFile, "set title \"%s : PI = %d PO = %d FF = %d Node = %d Obj = %d HPWL = %.2e\\n",
@ -1806,7 +1806,7 @@ clk = clock();
// Emb_ManPrintFanio( p );
// prepare data-structure
Aig_ManRandom( 1 ); // reset random numbers for deterministic behavior
Gia_ManRandom( 1 ); // reset random numbers for deterministic behavior
Emb_ManResetTravId( p );
Emb_ManSetValue( p );
clkSetup = clock() - clk;

6
src/aig/gia/giaEnable.c
View File

@ -362,7 +362,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
ABC_FREE( p->pCopies );
p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, 0 );
@ -437,7 +437,7 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
Gia_Obj_t * pThis, * pNode;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
@ -607,7 +607,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj1( p, pObj, i )
{

68
src/aig/gia/giaEquiv.c
View File

@ -330,7 +330,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -682,7 +682,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
if ( fDualOut )
Gia_ManEquivSetColors( p, fVerbose );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
@ -809,10 +809,10 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
if ( fDualOut )
Gia_ManEquivSetColors( p, 0 );
pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ObjSetCopyF( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) );
Gia_ObjSetCopyF( p, 0, pObj, Gia_InfoHasBit(pInit->pData, i) );
for ( f = 0; f < nFrames; f++ )
{
Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
@ -906,6 +906,66 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
}
/**Function*************************************************************
Synopsis [Transforms equiv classes by setting a good representative.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManEquivImprove( Gia_Man_t * p )
{
Vec_Int_t * vClass;
int i, k, iNode, iRepr;
int iReprBest, iLevelBest, iLevelCur, iMffcBest, iMffcCur;
assert( p->pReprs != NULL && p->pNexts != NULL );
Gia_ManLevelNum( p );
Gia_ManCreateRefs( p );
// iterate over class candidates
vClass = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, i )
{
Vec_IntClear( vClass );
iReprBest = -1;
iLevelBest = iMffcBest = ABC_INFINITY;
Gia_ClassForEachObj( p, i, k )
{
iLevelCur = Gia_ObjLevel( p,Gia_ManObj(p, k) );
iMffcCur = Gia_NodeMffcSize( p, Gia_ManObj(p, k) );
if ( iLevelBest > iLevelCur || (iLevelBest == iLevelCur && iMffcBest > iMffcCur) )
{
iReprBest = k;
iLevelBest = iLevelCur;
iMffcBest = iMffcCur;
}
Vec_IntPush( vClass, k );
}
assert( Vec_IntSize( vClass ) > 1 );
assert( iReprBest > 0 );
if ( i == iReprBest )
continue;
/*
printf( "Repr/Best = %6d/%6d. Lev = %3d/%3d. Mffc = %3d/%3d.\n",
i, iReprBest, Gia_ObjLevel( p,Gia_ManObj(p, i) ), Gia_ObjLevel( p,Gia_ManObj(p, iReprBest) ),
Gia_NodeMffcSize( p, Gia_ManObj(p, i) ), Gia_NodeMffcSize( p, Gia_ManObj(p, iReprBest) ) );
*/
iRepr = iReprBest;
Gia_ObjSetRepr( p, iRepr, GIA_VOID );
Gia_ObjSetProved( p, i );
Gia_ObjUnsetProved( p, iRepr );
Vec_IntForEachEntry( vClass, iNode, k )
if ( iNode != iRepr )
Gia_ObjSetRepr( p, iNode, iRepr );
}
Vec_IntFree( vClass );
ABC_FREE( p->pNexts );
// p->pNexts = Gia_ManDeriveNexts( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/aig/gia/giaFanout.c
View File

@ -117,7 +117,7 @@ void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout )
assert( Gia_ObjId(p, pFanout) > 0 );
if ( Gia_ObjId(p, pObj) >= p->nFansAlloc || Gia_ObjId(p, pFanout) >= p->nFansAlloc )
{
int nFansAlloc = 2 * AIG_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) );
int nFansAlloc = 2 * ABC_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) );
p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc );
memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
p->nFansAlloc = nFansAlloc;

6
src/aig/gia/giaForce.c
View File

@ -747,7 +747,7 @@ void Frc_ManPlaceRandom( Frc_Man_t * p )
pPlacement[i] = i;
for ( i = 0; i < p->nObjs; i++ )
{
iNext = Aig_ManRandom( 0 ) % p->nObjs;
iNext = Gia_ManRandom( 0 ) % p->nObjs;
Temp = pPlacement[i];
pPlacement[i] = pPlacement[iNext];
pPlacement[iNext] = Temp;
@ -774,7 +774,7 @@ void Frc_ManArrayShuffle( Vec_Int_t * vArray )
int i, iNext, Temp;
for ( i = 0; i < vArray->nSize; i++ )
{
iNext = Aig_ManRandom( 0 ) % vArray->nSize;
iNext = Gia_ManRandom( 0 ) % vArray->nSize;
Temp = vArray->pArray[i];
vArray->pArray[i] = vArray->pArray[iNext];
vArray->pArray[iNext] = Temp;
@ -1036,7 +1036,7 @@ void Frc_DumpGraphIntoFile( Frc_Man_t * p )
void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose )
{
Frc_Man_t * p;
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
if ( fClustered )
p = Frc_ManStart( pGia );
else

4
src/aig/gia/giaFrames.c
View File

@ -180,7 +180,7 @@ Gia_Man_t * Gia_ManFramesInit( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
Gia_ManFraSupports( p );
pFrames = Gia_ManStart( Vec_VecSizeSize((Vec_Vec_t*)p->vIns)+
Vec_VecSizeSize((Vec_Vec_t*)p->vAnds)+Vec_VecSizeSize((Vec_Vec_t*)p->vOuts) );
pFrames->pName = Aig_UtilStrsav( pAig->pName );
pFrames->pName = Gia_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; f < pPars->nFrames; f++ )
@ -290,7 +290,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
if ( pPars->fInit )
return Gia_ManFramesInit( pAig, pPars );
pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) );
pFrames->pName = Aig_UtilStrsav( pAig->pName );
pFrames->pName = Gia_UtilStrsav( pAig->pName );
Gia_ManHashAlloc( pFrames );
Gia_ManConst0(pAig)->Value = 0;
for ( f = 0; f < pPars->nFrames; f++ )

2
src/aig/gia/giaFront.c
View File

@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
Gia_ManSetRefs( p );
// start the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit);
// start the frontier
pFront = ABC_CALLOC( char, pNew->nFront );

18
src/aig/gia/giaGlitch.c
View File

@ -330,7 +330,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i);
return Aig_InfoHasBit( pNode->uTruth, Phase );
return Gia_InfoHasBit( pNode->uTruth, Phase );
}
/**Function*************************************************************
@ -349,7 +349,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
int i, Phase = 0;
for ( i = 0; i < (int)pNode->nFanins; i++ )
Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i);
return Aig_InfoHasBit( pNode->uTruth, Phase );
return Gia_InfoHasBit( pNode->uTruth, Phase );
}
/**Function*************************************************************
@ -429,7 +429,7 @@ void Gli_ManSetPiRandom( Gli_Man_t * p, float PiTransProb )
assert( 0.0 < PiTransProb && PiTransProb < 1.0 );
Vec_IntClear( p->vCisChanged );
Gli_ManForEachCi( p, pObj, i )
if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
{
Vec_IntPush( p->vCisChanged, pObj->Handle );
pObj->fPhase ^= 1;
@ -590,7 +590,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
for ( k = 0; k < nFanins; k++ )
if ( (pSimInfos[k] >> i) & 1 )
Phase |= (1 << k);
if ( Aig_InfoHasBit( pNode->uTruth, Phase ) )
if ( Gia_InfoHasBit( pNode->uTruth, Phase ) )
Result |= (1 << i);
}
return Result;
@ -612,9 +612,9 @@ static inline unsigned Gli_ManUpdateRandomInput( unsigned uInfo, float PiTransPr
float Multi = 1.0 / (1 << 16);
int i;
if ( PiTransProb == 0.5 )
return Aig_ManRandom(0);
return Gia_ManRandom(0);
for ( i = 0; i < 32; i++ )
if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
uInfo ^= (1 << i);
return uInfo;
}
@ -703,7 +703,7 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb )
// set changed PIs
Vec_IntClear( p->vCisChanged );
Gli_ManForEachPi( p, pObj, i )
if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
if ( Multi * (Gia_ManRandom(0) & 0xffff) < PiTransProb )
{
Vec_IntPush( p->vCisChanged, pObj->Handle );
pObj->fPhase ^= 1;
@ -738,7 +738,7 @@ void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb )
void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose )
{
int i, k, clk = clock();
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
Gli_ManFinalize( p );
if ( p->nRegs == 0 )
{
@ -752,7 +752,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
}
else
{
int nIters = Aig_BitWordNum(nPatterns);
int nIters = Gia_BitWordNum(nPatterns);
Gli_ManSimulateSeqPref( p, 16 );
for ( i = 0; i < 32; i++ )
{

33
src/aig/gia/giaHash.c
View File

@ -86,7 +86,7 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 )
void Gia_ManHashAlloc( Gia_Man_t * p )
{
assert( p->pHTable == NULL );
p->nHTable = Aig_PrimeCudd( p->nObjsAlloc );
p->nHTable = Gia_PrimeCudd( p->nObjsAlloc );
p->pHTable = ABC_CALLOC( int, p->nHTable );
}
@ -152,7 +152,7 @@ void Gia_ManHashResize( Gia_Man_t * p )
// replace the table
pHTableOld = p->pHTable;
nHTableOld = p->nHTable;
p->nHTable = Aig_PrimeCudd( 2 * Gia_ManAndNum(p) );
p->nHTable = Gia_PrimeCudd( 2 * Gia_ManAndNum(p) );
p->pHTable = ABC_CALLOC( int, p->nHTable );
// rehash the entries from the old table
Counter = 0;
@ -322,14 +322,14 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
{
Gia_Obj_t * pNode0, * pNode1, * pFanA, * pFanB, * pFanC, * pFanD;
assert( p->fAddStrash );
if ( !Gia_ObjIsAnd(Gia_Regular(p0)) && !Gia_ObjIsAnd(Gia_Regular(p1)) )
return NULL;
pNode0 = Gia_Regular(p0);
pNode1 = Gia_Regular(p1);
pFanA = Gia_ObjChild0(pNode0);
pFanB = Gia_ObjChild1(pNode0);
pFanC = Gia_ObjChild0(pNode1);
pFanD = Gia_ObjChild1(pNode1);
if ( !Gia_ObjIsAnd(pNode0) && !Gia_ObjIsAnd(pNode1) )
return NULL;
pFanA = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild0(pNode0) : NULL;
pFanB = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild1(pNode0) : NULL;
pFanC = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild0(pNode1) : NULL;
pFanD = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild1(pNode1) : NULL;
if ( Gia_IsComplement(p0) )
{
if ( pFanA == Gia_Not(p1) || pFanB == Gia_Not(p1) )
@ -404,6 +404,7 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
if ( pFanB == pFanD && pFanA == Gia_Not(pFanC) )
return Gia_Not(pFanB);
}
/*
if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) )
return NULL;
if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) )
@ -424,8 +425,12 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
}
pNode0 = Gia_ManHashAndP( p, Gia_Not(pNodeC), pNodeE );
pNode1 = Gia_ManHashAndP( p, pNodeC, pNodeT );
return Gia_NotCond( Gia_ManHashAndP( p, pNode0, pNode1 ), !fCompl );
p->fAddStrash = 0;
pNodeC = Gia_NotCond( Gia_ManHashAndP( p, Gia_Not(pNode0), Gia_Not(pNode1) ), !fCompl );
p->fAddStrash = 1;
return pNodeC;
}
*/
return NULL;
}
@ -555,13 +560,14 @@ int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManRehash( Gia_Man_t * p )
Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
{
Gia_Man_t * pNew;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
pNew->fAddStrash = fAddStrash;
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObj( p, pObj, i )
@ -574,8 +580,11 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
Gia_ManHashStop( pNew );
pNew->fAddStrash = 0;
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
// printf( "Top gate is %s\n", Gia_ObjFaninC0(Gia_ManCo(pNew, 0))? "OR" : "AND" );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}

1
src/aig/gia/giaMan.c
View File

@ -72,6 +72,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFree( p->vCos );
ABC_FREE( p->pPlacement );
ABC_FREE( p->pSwitching );
ABC_FREE( p->pCexSeq );
ABC_FREE( p->pCexComb );
ABC_FREE( p->pIso );
ABC_FREE( p->pMapping );

2
src/aig/gia/giaRetime.c
View File

@ -122,7 +122,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
int i;
// create the new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pName = Gia_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
// create the true PIs
Gia_ManFillValue( p );

2
src/aig/gia/giaSat.c
View File

@ -262,7 +262,7 @@ int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int *
(*pnLeaves)++;
else
Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj);
return AIG_MAX( Level0, Level1 );
return ABC_MAX( Level0, Level1 );
}
/**Function*************************************************************

112
src/aig/gia/giaSim.c
View File

@ -64,7 +64,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
p->nIters = 32; // the number of timeframes
p->TimeLimit = 60; // time limit in seconds
p->fCheckMiter = 0; // check if miter outputs are non-zero
p->fVerbose = 1; // enables verbose output
p->fVerbose = 0; // enables verbose output
}
/**Function*************************************************************
@ -92,7 +92,7 @@ Gia_ManSim_t * Gia_ManSimCreate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * Gia_ManCoNum(p->pAig) );
p->vCis2Ids = Vec_IntAlloc( Gia_ManCiNum(p->pAig) );
Vec_IntForEachEntry( pAig->vCis, Entry, i )
Vec_IntPush( p->vCis2Ids, Entry );
Vec_IntPush( p->vCis2Ids, i ); // do we need p->vCis2Ids?
printf( "AIG = %7.2f Mb. Front mem = %7.2f Mb. Other mem = %7.2f Mb.\n",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*p->nWords*p->pAig->nFront/(1<<20),
@ -136,7 +136,7 @@ static inline void Gia_ManSimInfoRandom( Gia_ManSim_t * p, unsigned * pInfo )
{
int w;
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = Aig_ManRandom( 0 );
pInfo[w] = Gia_ManRandom( 0 );
}
/**Function*************************************************************
@ -173,7 +173,7 @@ static inline int Gia_ManSimInfoIsZero( Gia_ManSim_t * p, unsigned * pInfo )
int w;
for ( w = p->nWords-1; w >= 0; w-- )
if ( pInfo[w] )
return 32*(w-1) + Aig_WordFindFirstBit( pInfo[w] );
return 32*(w-1) + Gia_WordFindFirstBit( pInfo[w] );
return -1;
}
@ -380,6 +380,71 @@ static inline void Gia_ManSimulateRound( Gia_ManSim_t * p )
assert( Gia_ManCoNum(p->pAig) == iCos );
}
/**Function*************************************************************
Synopsis [Returns index of the PO and pattern that failed it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Gia_ManCheckPos( Gia_ManSim_t * p, int * piPo, int * piPat )
{
int i, iPat;
for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
{
iPat = Gia_ManSimInfoIsZero( p, Gia_SimDataCo(p, i) );
if ( iPat >= 0 )
{
*piPo = i;
*piPat = iPat;
return 1;
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Returns the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
{
Gia_Cex_t * p;
unsigned * pData;
int f, i, w, iPioId, Counter;
p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
p->iFrame = iFrame;
p->iPo = iOut;
// fill in the binary data
Gia_ManRandom( 1 );
Counter = p->nRegs;
pData = ABC_ALLOC( unsigned, nWords );
for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
{
iPioId = Vec_IntEntry( vCis2Ids, i );
if ( iPioId >= p->nPis )
continue;
for ( w = nWords-1; w >= 0; w-- )
pData[w] = Gia_ManRandom( 0 );
if ( Gia_InfoHasBit( pData, iPat ) )
Gia_InfoSetBit( p->pData, Counter + iPioId );
}
ABC_FREE( pData );
return p;
}
/**Function*************************************************************
Synopsis []
@ -394,40 +459,53 @@ static inline void Gia_ManSimulateRound( Gia_ManSim_t * p )
int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
{
Gia_ManSim_t * p;
int i, clk = clock();
int i, clkTotal = clock();
int iOut, iPat, RetValue = 0;
ABC_FREE( pAig->pCexSeq );
p = Gia_ManSimCreate( pAig, pPars );
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
Gia_ManSimInfoInit( p );
for ( i = 0; i < pPars->nIters; i++ )
{
Gia_ManSimulateRound( p );
/*
if ( pPars->fVerbose )
{
printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
printf( "Time = %7.2f sec\r", (1.0*clock()-clk)/CLOCKS_PER_SEC );
printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
}
if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
{
assert( pAig->pSeqModel == NULL );
pAig->pSeqModel = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
if ( pPars->fVerbose )
printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", iOut, i );
if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
{
printf( "\n" );
printf( "Generated counter-example is INVALID \n" );
printf( "\n" );
}
else
{
printf( "\n" );
printf( "Generated counter-example is fine \n" );
printf( "\n" );
}
RetValue = 1;
break;
}
if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
{
printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit );
printf( "No bug detected after %d frames with time limit %d seconds. \n", i+1, pPars->TimeLimit );
break;
}
*/
if ( i < pPars->nIters - 1 )
Gia_ManSimInfoTransfer( p );
}
Gia_ManSimDelete( p );
printf( "Simulated %d frames with %d words. ", pPars->nIters, pPars->nWords );
ABC_PRT( "Time", clock() - clk );
return 0;
printf( "Simulated %d frames with %d words. ", i, pPars->nWords );
ABC_PRT( "Time", clock() - clkTotal );
return RetValue;
}
////////////////////////////////////////////////////////////////////////

29
src/aig/gia/giaSwitch.c
View File

@ -18,7 +18,7 @@
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -146,23 +146,23 @@ static inline void Gia_ManSwiSimInfoRandom( Gia_ManSwi_t * p, unsigned * pInfo,
int w, i;
if ( nProbNum == -1 )
{ // 3/8 = 1/4 + 1/8
Mask = (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )) |
(Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ));
Mask = (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )) |
(Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ));
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] ^= Mask;
}
else if ( nProbNum > 0 )
{
Mask = Aig_ManRandom( 0 );
Mask = Gia_ManRandom( 0 );
for ( i = 0; i < nProbNum; i++ )
Mask &= Aig_ManRandom( 0 );
Mask &= Gia_ManRandom( 0 );
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] ^= Mask;
}
else if ( nProbNum == 0 )
{
for ( w = p->nWords-1; w >= 0; w-- )
pInfo[w] = Aig_ManRandom( 0 );
pInfo[w] = Gia_ManRandom( 0 );
}
else
assert( 0 );
@ -185,14 +185,14 @@ static inline void Gia_ManSwiSimInfoRandomShift( Gia_ManSwi_t * p, unsigned * pI
int w, i;
if ( nProbNum == -1 )
{ // 3/8 = 1/4 + 1/8
Mask = (Aig_ManRandom( 0 ) & Aig_ManRandom( 0 )) |
(Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ) & Aig_ManRandom( 0 ));
Mask = (Gia_ManRandom( 0 ) & Gia_ManRandom( 0 )) |
(Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ) & Gia_ManRandom( 0 ));
}
else if ( nProbNum >= 0 )
{
Mask = Aig_ManRandom( 0 );
Mask = Gia_ManRandom( 0 );
for ( i = 0; i < nProbNum; i++ )
Mask &= Aig_ManRandom( 0 );
Mask &= Gia_ManRandom( 0 );
}
else
assert( 0 );
@ -430,7 +430,7 @@ static inline int Gia_ManSwiSimInfoCountOnes( Gia_ManSwi_t * p, int iPlace )
int w, Counter = 0;
pInfo = Gia_SwiData( p, iPlace );
for ( w = p->nWords-1; w >= 0; w-- )
Counter += Aig_WordCountOnes( pInfo[w] );
Counter += Gia_WordCountOnes( pInfo[w] );
return Counter;
}
@ -451,7 +451,7 @@ static inline int Gia_ManSwiSimInfoCountTrans( Gia_ManSwi_t * p, int iPlace )
int w, Counter = 0;
pInfo = Gia_SwiData( p, iPlace );
for ( w = p->nWords-1; w >= 0; w-- )
Counter += 2*Aig_WordCountOnes( (pInfo[w] ^ (pInfo[w] >> 16)) & 0xffff );
Counter += 2*Gia_WordCountOnes( (pInfo[w] ^ (pInfo[w] >> 16)) & 0xffff );
return Counter;
}
@ -565,7 +565,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
{
printf( "Obj = %8d (%8d). F = %6d. ",
pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront,
4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*p->nWords*p->pAig->nFront/(1<<20),
@ -573,7 +573,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
ABC_PRT( "Time", clock() - clk );
}
// perform simulation
Aig_ManRandom( 1 );
Gia_ManRandom( 1 );
Gia_ManSwiSimInfoInit( p );
for ( i = 0; i < pPars->nIters; i++ )
{
@ -612,7 +612,6 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
return vSwitching;
}
/**Function*************************************************************
Synopsis [Computes probability of switching (or of being 1).]

22
src/aig/gia/giaTsim.c
View File

@ -81,15 +81,15 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig )
p = ABC_CALLOC( Gia_ManTer_t, 1 );
p->pAig = Gia_ManFront( pAig );
p->nIters = 300;
p->pDataSim = ABC_ALLOC( unsigned, Aig_BitWordNum(2*p->pAig->nFront) );
p->pDataSimCis = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
p->pDataSimCos = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
p->pDataSim = ABC_ALLOC( unsigned, Gia_BitWordNum(2*p->pAig->nFront) );
p->pDataSimCis = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
p->pDataSimCos = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
// allocate storage for terminary states
p->nStateWords = Aig_BitWordNum( 2*Gia_ManRegNum(pAig) );
p->nStateWords = Gia_BitWordNum( 2*Gia_ManRegNum(pAig) );
p->vStates = Vec_PtrAlloc( 1000 );
p->pCount0 = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
p->pCountX = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
p->nBins = Aig_PrimeCudd( 500 );
p->nBins = Gia_PrimeCudd( 500 );
p->pBins = ABC_CALLOC( unsigned *, p->nBins );
p->vRetired = Vec_IntAlloc( 100 );
p->pRetired = ABC_CALLOC( char, Gia_ManRegNum(pAig) );
@ -508,7 +508,7 @@ void Gia_ManTerAnalyze2( Vec_Ptr_t * vStates, int nRegs )
unsigned * pTemp, * pStates = Vec_PtrPop( vStates );
int i, w, nZeros, nConsts, nStateWords;
// detect constant zero registers
nStateWords = Aig_BitWordNum( 2*nRegs );
nStateWords = Gia_BitWordNum( 2*nRegs );
memset( pStates, 0, sizeof(int) * nStateWords );
Vec_PtrForEachEntry( vStates, pTemp, i )
for ( w = 0; w < nStateWords; w++ )
@ -576,7 +576,7 @@ Vec_Ptr_t * Gia_ManTerTranspose( Gia_ManTer_t * p )
unsigned * pState, * pFlop;
int i, k, nFlopWords;
vFlops = Vec_PtrAlloc( 100 );
nFlopWords = Aig_BitWordNum( 2*Vec_PtrSize(p->vStates) );
nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
{
if ( p->pCount0[i] == Vec_PtrSize(p->vStates) )
@ -631,7 +631,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose )
Gia_Obj_t * pObj;
Vec_Int_t * vMapKtoI;
int i, iRepr, nFlopWords, Counter0 = 0, CounterE = 0;
nFlopWords = Aig_BitWordNum( 2*Vec_PtrSize(p->vStates) );
nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
p->vFlops = Gia_ManTerTranspose( p );
pCi2Lit = ABC_FALLOC( unsigned, Gia_ManCiNum(p->pAig) );
vMapKtoI = Vec_IntAlloc( 100 );
@ -679,11 +679,11 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
{
printf( "Obj = %8d (%8d). F = %6d. ",
pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront,
4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ",
12.0*Gia_ManObjNum(p->pAig)/(1<<20),
4.0*Aig_BitWordNum(2 * p->pAig->nFront)/(1<<20),
4.0*Aig_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20),
4.0*Gia_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
ABC_PRT( "Time", clock() - clk );
}
// perform simulation

199
src/aig/gia/giaUtil.c
View File

@ -23,11 +23,121 @@
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define NUMBER1 3716960521u
#define NUMBER2 2174103536u
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates a sequence or random numbers.]
Description []
SideEffects []
SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
***********************************************************************/
unsigned Gia_ManRandom( int fReset )
{
static unsigned int m_z = NUMBER1;
static unsigned int m_w = NUMBER2;
if ( fReset )
{
m_z = NUMBER1;
m_w = NUMBER2;
}
m_z = 36969 * (m_z & 65535) + (m_z >> 16);
m_w = 18000 * (m_w & 65535) + (m_w >> 16);
return (m_z << 16) + m_w;
}
/**Function*************************************************************
Synopsis [Creates random info for the primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop )
{
unsigned * pInfo;
int i, w;
Vec_PtrForEachEntryStart( vInfo, pInfo, i, iInputStart )
for ( w = iWordStart; w < iWordStop; w++ )
pInfo[w] = Gia_ManRandom(0);
}
/**Function********************************************************************
Synopsis [Returns the next prime >= p.]
Description [Copied from CUDD, for stand-aloneness.]
SideEffects [None]
SeeAlso []
******************************************************************************/
unsigned int Gia_PrimeCudd( unsigned int p )
{
int i,pn;
p--;
do {
p++;
if (p&1) {
pn = 1;
i = 3;
while ((unsigned) (i * i) <= p) {
if (p % i == 0) {
pn = 0;
break;
}
i += 2;
}
} else {
pn = 0;
}
} while (!pn);
return(p);
} /* end of Cudd_Prime */
/**Function*************************************************************
Synopsis [Returns the composite name of the file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix )
{
static char Buffer[1000];
char * pDot;
strcpy( Buffer, pBase );
if ( (pDot = strrchr( Buffer, '.' )) )
*pDot = 0;
strcat( Buffer, pSuffix );
if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
return pDot+1;
return Buffer;
}
/**Function*************************************************************
Synopsis [Sets phases of the internal nodes.]
@ -592,7 +702,7 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
Gia_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
Gia_Cex_t * pCex;
int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames );
pCex = (Gia_Cex_t *)ABC_ALLOC( char, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
memset( pCex, 0, sizeof(Gia_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
@ -617,11 +727,11 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut )
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++);
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Aig_InfoHasBit(p->pData, iBit++);
pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
@ -657,18 +767,97 @@ void Gia_ManPrintCounterExample( Gia_Cex_t * p )
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
printf( "State : " );
for ( k = 0; k < p->nRegs; k++ )
printf( "%d", Aig_InfoHasBit(p->pData, k) );
printf( "%d", Gia_InfoHasBit(p->pData, k) );
printf( "\n" );
for ( f = 0; f <= p->iFrame; f++ )
{
printf( "Frame %2d : ", f );
for ( i = 0; i < p->nPis; i++ )
printf( "%d", Aig_InfoHasBit(p->pData, k++) );
printf( "%d", Gia_InfoHasBit(p->pData, k++) );
printf( "\n" );
}
assert( k == p->nBits );
}
/**Function*************************************************************
Synopsis [Dereferences the node's MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
{
Gia_Obj_t * pFanin;
int Counter = 0;
if ( Gia_ObjIsCi(pNode) )
return 0;
assert( Gia_ObjIsAnd(pNode) );
pFanin = Gia_ObjFanin0(pNode);
assert( Gia_ObjRefs(p, pFanin) > 0 );
if ( Gia_ObjRefDec(p, pFanin) == 0 )
Counter += Gia_NodeDeref_rec( p, pFanin );
pFanin = Gia_ObjFanin1(pNode);
assert( Gia_ObjRefs(p, pFanin) > 0 );
if ( Gia_ObjRefDec(p, pFanin) == 0 )
Counter += Gia_NodeDeref_rec( p, pFanin );
return Counter + 1;
}
/**Function*************************************************************
Synopsis [References the node's MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode )
{
Gia_Obj_t * pFanin;
int Counter = 0;
if ( Gia_ObjIsCi(pNode) )
return 0;
assert( Gia_ObjIsAnd(pNode) );
pFanin = Gia_ObjFanin0(pNode);
if ( Gia_ObjRefInc(p, pFanin) == 0 )
Counter += Gia_NodeRef_rec( p, pFanin );
pFanin = Gia_ObjFanin1(pNode);
if ( Gia_ObjRefInc(p, pFanin) == 0 )
Counter += Gia_NodeRef_rec( p, pFanin );
return Counter + 1;
}
/**Function*************************************************************
Synopsis [Returns the number of internal nodes in the MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
{
int ConeSize1, ConeSize2;
assert( !Gia_IsComplement(pNode) );
assert( Gia_ObjIsCand(pNode) );
ConeSize1 = Gia_NodeDeref_rec( p, pNode );
ConeSize2 = Gia_NodeRef_rec( p, pNode );
assert( ConeSize1 == ConeSize2 );
assert( ConeSize1 >= 0 );
return ConeSize1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -112,9 +112,6 @@ struct Hop_Man_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
#define AIG_MAX(a,b) (((a) > (b))? (a) : (b))
static inline int Hop_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
static inline int Hop_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline int Hop_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
@ -186,7 +183,7 @@ static inline Hop_Obj_t * Hop_ObjChild1( Hop_Obj_t * pObj ) { return pObj-
static inline Hop_Obj_t * Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL; }
static inline Hop_Obj_t * Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL; }
static inline int Hop_ObjLevel( Hop_Obj_t * pObj ) { return pObj->nRefs; }
static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); }
static inline int Hop_ObjLevelNew( Hop_Obj_t * pObj ) { return 1 + Hop_ObjIsExor(pObj) + ABC_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs); }
static inline int Hop_ObjPhaseCompl( Hop_Obj_t * pObj ) { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
static inline void Hop_ObjClean( Hop_Obj_t * pObj ) { memset( pObj, 0, sizeof(Hop_Obj_t) ); }
static inline int Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin )

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

@ -125,13 +125,13 @@ int Hop_ManCountLevels( Hop_Man_t * p )
{
Level0 = (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData;
Level1 = (int)(ABC_PTRUINT_T)Hop_ObjFanin1(pObj)->pData;
pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + AIG_MAX(Level0, Level1));
pObj->pData = (void *)(ABC_PTRUINT_T)(1 + Hop_ObjIsExor(pObj) + ABC_MAX(Level0, Level1));
}
Vec_PtrFree( vNodes );
// get levels of the POs
LevelsMax = 0;
Hop_ManForEachPo( p, pObj, i )
LevelsMax = AIG_MAX( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData );
LevelsMax = ABC_MAX( LevelsMax, (int)(ABC_PTRUINT_T)Hop_ObjFanin0(pObj)->pData );
return LevelsMax;
}

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

@ -193,7 +193,7 @@ void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj )
// remove PIs/POs from the arrays
if ( Hop_ObjIsPi(pObj) )
Vec_PtrRemove( p->vPis, pObj );
// ABC_FREE the node
// free the node
Hop_ManRecycleMemory( p, pObj );
}

2
src/aig/int/intCtrex.c
View File

@ -138,7 +138,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
Aig_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i );
ABC_FREE( pModel );
}
// ABC_FREE the sat_solver
// free the sat_solver
sat_solver_delete( pSat );
Vec_IntFree( vCiIds );
// verify counter-example

2
src/aig/ivy/ivyFraig.c
View File

@ -1218,7 +1218,7 @@ void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
Ivy_ObjSetClassNodeRepr( pObj, NULL );
Ivy_FraigAddClass( &p->lClasses, pObj );
}
// ABC_FREE the table
// free the table
ABC_FREE( pTable );
}

2
src/aig/ivy/ivyHaig.c
View File

@ -518,7 +518,7 @@ printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
pObj->Init = pObj->Level, pObj->Level = 0;
}
// ABC_FREE arrays
// free arrays
Vec_IntFree( vNodes );
Vec_IntFree( vLatches );
}

4
src/aig/ivy/ivyMan.c
View File

@ -143,7 +143,7 @@ Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
// update the counters of different objects
pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p);
pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p);
// ABC_FREE arrays
// free arrays
Vec_IntFree( vNodes );
Vec_IntFree( vLatches );
// make sure structural hashing did not change anything
@ -346,7 +346,7 @@ int Ivy_ManCleanupSeq( Ivy_Man_t * p )
// delete buffer from the array of buffers
if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
Vec_PtrRemove( p->vBufs, pObj );
// ABC_FREE the node
// free the node
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
Ivy_ManRecycleMemory( p, pObj );
}

2
src/aig/ivy/ivyObj.c
View File

@ -268,7 +268,7 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
// clean and recycle the entry
if ( fFreeTop )
{
// ABC_FREE the node
// free the node
Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
Ivy_ManRecycleMemory( p, pObj );
}

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

@ -2422,7 +2422,7 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit
// compute the sum total of supports
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
// ABC_FREE the networks
// free the networks
Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
}
@ -2460,7 +2460,7 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit
}
}
// ABC_FREE the networks
// free the networks
for ( i = 0; i < 5; i++ )
for ( k = 0; k < 16; k++ )
if ( ppNtks[i][k] )

4
src/aig/mfx/mfxCore.c
View File

@ -86,7 +86,7 @@ p->timeWin += clock() - clk;
// compute the divisors of the window
clk = clock();
p->vDivs = Mfx_ComputeDivisors( p, pNode, Nwk_ObjRequired(pNode) - If_LutLibSlowestPinDelay(pNode->pMan->pLutLib) );
// p->vDivs = Mfx_ComputeDivisors( p, pNode, AIG_INFINITY );
// p->vDivs = Mfx_ComputeDivisors( p, pNode, ABC_INFINITY );
p->nTotalDivs += Vec_PtrSize(p->vDivs);
p->timeDiv += clock() - clk;
// construct AIG for the window
@ -371,7 +371,7 @@ int Mfx_Perform( Nwk_Man_t * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib )
if ( pPars->fPower )
printf( "Total switching after = %7.2f.\n", Nwl_ManComputeTotalSwitching(pNtk) );
// ABC_FREE the manager
// free the manager
p->timeTotal = clock() - clk;
Mfx_ManStop( p );

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

@ -185,7 +185,7 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
Ntl_ObjForEachFanin( pObj, pNetFanin, i )
{
LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pCopy) );
LevelMax = AIG_MAX( LevelMax, LevelCur );
LevelMax = ABC_MAX( LevelMax, LevelCur );
Vec_PtrPush( p->vCos, pNetFanin );
Aig_ObjCreatePo( p->pAig, pNetFanin->pCopy );
}

2
src/aig/nwk/nwkFanio.c
View File

@ -172,7 +172,7 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
pObj->pFanio[i] = pObj->pFanio[i-1];
pObj->pFanio[pObj->nFanins++] = pFanin;
pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj;
pObj->Level = AIG_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
pObj->Level = ABC_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
}
/**Function*************************************************************

2
src/aig/nwk/nwkMan.c
View File

@ -127,7 +127,7 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
int nPis; // the number of primary inputs
int nPos; // the number of primary outputs
} ParsNew, ParsBest = { 0 };
// ABC_FREE storage for the name
// free storage for the name
if ( pNtk == NULL )
{
ABC_FREE( ParsBest.pName );

4
src/aig/nwk/nwkTiming.c
View File

@ -736,7 +736,7 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
for ( i = 0; i < nTerms; i++ )
{
pFanin = Nwk_ManCo(pObj->pMan, iTerm1 + i);
Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) );
Level = ABC_MAX( Level, Nwk_ObjLevel(pFanin) );
}
Level++;
}
@ -745,7 +745,7 @@ int Nwk_ObjLevelNew( Nwk_Obj_t * pObj )
}
assert( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) );
Nwk_ObjForEachFanin( pObj, pFanin, i )
Level = AIG_MAX( Level, Nwk_ObjLevel(pFanin) );
Level = ABC_MAX( Level, Nwk_ObjLevel(pFanin) );
return Level + (Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0);
}

6
src/aig/nwk/nwkUtil.c
View File

@ -368,12 +368,12 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
nFanouts = Nwk_ObjFanoutNum(pNode);
nFaninsAll += nFanins;
nFanoutsAll += nFanouts;
nFaninsMax = AIG_MAX( nFaninsMax, nFanins );
nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts );
nFaninsMax = ABC_MAX( nFaninsMax, nFanins );
nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts );
}
// allocate storage for fanin/fanout numbers
nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
nSizeMax = ABC_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );

2
src/aig/nwk2/nwkFanio.c
View File

@ -172,7 +172,7 @@ void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
pObj->pFanio[i] = pObj->pFanio[i-1];
pObj->pFanio[pObj->nFanins++] = pFanin;
pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj;
pObj->Level = AIG_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
pObj->Level = ABC_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
}
/**Function*************************************************************

6
src/aig/nwk2/nwkUtil.c
View File

@ -368,12 +368,12 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
nFanouts = Nwk_ObjFanoutNum(pNode);
nFaninsAll += nFanins;
nFanoutsAll += nFanouts;
nFaninsMax = AIG_MAX( nFaninsMax, nFanins );
nFanoutsMax = AIG_MAX( nFanoutsMax, nFanouts );
nFaninsMax = ABC_MAX( nFaninsMax, nFanins );
nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts );
}
// allocate storage for fanin/fanout numbers
nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
nSizeMax = ABC_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
vFanins = Vec_IntStart( nSizeMax );
vFanouts = Vec_IntStart( nSizeMax );

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

@ -90,7 +90,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) {
////////////////////////////////////////////////////////////////////////
/*=== sswAbs.c ==========================================================*/
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose );
extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose );
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );

13
src/aig/saig/saigAbs.c
View File

@ -693,15 +693,15 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int fVerbose )
{
Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose )
{
extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose );
Vec_Int_t * vFlopsNew, * vPiToReg;
Aig_Obj_t * pObj;
int i, Entry, iFlop;
Saig_BmcPerform( pAbs, 2000, 2000, 5000, 1000000, fVerbose );
Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose );
if ( pAbs->pSeqModel == NULL )
return NULL;
// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose )
Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
{
Aig_Man_t * pResult, * pTemp;
Cnf_Dat_t * pCnf;
@ -779,11 +779,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
if ( fSkipProof )
{
assert( 0 );
// assert( 0 );
if ( fVerbose )
printf( "Performing counter-example-based refinement.\n" );
// vFlops = Vec_IntStartNatural( 100 );
// Vec_IntPush( vFlops, 0 );
vFlops = Vec_IntStartNatural( 1 );
}
else
{
@ -858,7 +859,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
printf( "Refining abstraction...\n" );
for ( Iter = 0; ; Iter++ )
{
pTemp = Saig_ManProofRefine( p, pResult, vFlops, fVerbose );
pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pTemp == NULL )
break;
Aig_ManStop( pResult );

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

@ -327,7 +327,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) );
assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 );
// start timeframes
p = Aig_ManStart( nFrames * AIG_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) );
p = Aig_ManStart( nFrames * ABC_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) );
p->pName = Aig_UtilStrsav( "frames" );
// create variables for register outputs
pAig = pBot;

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

@ -180,7 +180,7 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 )
pNode->iFan1 = iFan1;
pNode->iNext = 0;
if ( iFan0 || iFan1 )
p->pLevels[p->nObjs] = 1 + AIG_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) );
p->pLevels[p->nObjs] = 1 + ABC_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) );
else
p->pLevels[p->nObjs] = 0, p->nPis++;
return p->nObjs++;

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

@ -616,7 +616,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
return NULL;
}
clk = clock();
vSimInfo = Vec_PtrAllocSimInfo( AIG_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
vSimInfo = Vec_PtrAllocSimInfo( ABC_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 );
// process Design 1
RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 );

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

@ -398,7 +398,7 @@ ABC_PRT( "Fraiging", clock() - clk );
clk = clock();
pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
ABC_PRT( "Mapped", clock() - clk );
// ABC_FREE mapping
// free mapping
Saig_ManStopMap2( pAig );
clk = clock();
pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );

2
src/aig/ssw/sswClass.c
View File

@ -597,7 +597,7 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr,
// int nWords = 4;
// int nIters = 0;
int nFrames = AIG_MAX( nFramesK, 4 );
int nFrames = ABC_MAX( nFramesK, 4 );
int nWords = 2;
int nIters = 16;
Ssw_Cla_t * p;

4
src/aig/ssw/sswCore.c
View File

@ -204,8 +204,8 @@ clk = clock();
nSatFailsReal = p->nSatFailsReal;
nUniques = p->nUniques;
p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars );
p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
Ssw_SatStop( p->pMSat );
p->pMSat = NULL;
Ssw_ManCleanup( p );

4
src/aig/ssw/sswDyn.c
View File

@ -438,8 +438,8 @@ p->timeReduce += clock() - clk;
// replace the solver
if ( p->pMSat )
{
p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars );
p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
Ssw_SatStop( p->pMSat );
p->nRecycles++;
p->nRecyclesTotal++;

4
src/aig/ssw/sswLcorr.c
View File

@ -300,8 +300,8 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
p->pMSat->nSatVars > p->pPars->nSatVarMax &&
p->nRecycleCalls > p->pPars->nRecycleCalls )
{
p->nVarsMax = AIG_MAX( p->nVarsMax, p->pMSat->nSatVars );
p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars );
p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
Ssw_SatStop( p->pMSat );
p->pMSat = Ssw_SatStart( 0 );
p->nRecycles++;

2
src/aig/ssw/sswSemi.c
View File

@ -68,7 +68,7 @@ Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
memset( p, 0, sizeof(Ssw_Sem_t) );
p->nConfMaxStart = nConfMax;
p->nConfMax = nConfMax;
p->nFramesSweep = AIG_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
p->nFramesSweep = ABC_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
p->fVerbose = fVerbose;
// equivalences considered
p->pMan = pMan;

6
src/aig/ssw/sswSim.c
View File

@ -590,7 +590,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
Aig_ManForEachPi( p->pAig, pObj, i )
Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// flip one bit
Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
Limit = ABC_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
}
@ -612,7 +612,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
// flip one bit of the last frame
if ( fUseDist1 ) //&& p->nFrames == 2 )
{
Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
Limit = ABC_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
}
@ -641,7 +641,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// set distance one PIs for the first frame
Limit = AIG_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
Limit = ABC_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );

8
src/aig/tim/tim.c
View File

@ -28,10 +28,6 @@
#include "mem.h"
#include "tim.h"
#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
#define AIG_MAX(a,b) (((a) > (b))? (a) : (b))
#define AIG_ABS(a) (((a) >= 0)? (a) :-(a))
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@ -773,7 +769,7 @@ float Tim_ManGetCiArrival( Tim_Man_t * p, int iCi )
pDelays = pBox->pDelayTable + i * pBox->nInputs;
DelayBest = -TIM_ETERNITY;
Tim_ManBoxForEachInput( p, pBox, pObj, k )
DelayBest = AIG_MAX( DelayBest, pObj->timeArr + pDelays[k] );
DelayBest = ABC_MAX( DelayBest, pObj->timeArr + pDelays[k] );
pObjRes->timeArr = DelayBest;
pObjRes->TravId = p->nTravIds;
}
@ -820,7 +816,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo )
Tim_ManBoxForEachOutput( p, pBox, pObj, k )
{
pDelays = pBox->pDelayTable + k * pBox->nInputs;
DelayBest = AIG_MIN( DelayBest, pObj->timeReq - pDelays[i] );
DelayBest = ABC_MIN( DelayBest, pObj->timeReq - pDelays[i] );
}
pObjRes->timeReq = DelayBest;
pObjRes->TravId = p->nTravIds;

2
src/base/abc/abcAig.c
View File

@ -163,7 +163,7 @@ void Abc_AigFree( Abc_Aig_t * pMan )
{
assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
// ABC_FREE the table
// free the table
if ( pMan->vAddedCells )
Vec_PtrFree( pMan->vAddedCells );
if ( pMan->vUpdatedNets )

110
src/base/abc/abcLatch.c
View File

@ -371,6 +371,116 @@ printf( "Converted %d one-hot registers.\n", Vec_IntSize(vNumbers) );
}
/**Function*************************************************************
Synopsis [Converts registers with DC values into additional PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
{
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObj, * pFanin, * pObjNew, * pObjLiNew, * pObjLoNew;
int i, k, nFlops, nStates, iState, pfCompl[32];
assert( Abc_NtkIsLogic(pNtk) );
nFlops = Abc_NtkLatchNum(pNtk);
if ( nFlops == 0 )
return Abc_NtkDup( pNtk );
if ( nFlops > 16 )
{
printf( "Cannot reencode %d flops because it will lead to 2^%d states.\n", nFlops, nFlops );
return NULL;
}
// check if there are latches with DC values
iState = 0;
Abc_NtkForEachLatch( pNtk, pObj, i )
{
if ( Abc_LatchIsInitDc(pObj) )
{
printf( "Cannot process logic network with don't-care init values. Run \"zero\".\n" );
return NULL;
}
if ( Abc_LatchIsInit1(pObj) )
iState |= (1 << i);
}
// transfer logic to SOPs
Abc_NtkToSop( pNtk, 0 );
// create new network
pNtkNew = Abc_NtkStartFromNoLatches( pNtk, pNtk->ntkType, pNtk->ntkFunc );
nStates = (1 << nFlops);
for ( i = 0; i < nStates; i++ )
{
pObjNew = Abc_NtkCreateLatch( pNtkNew );
pObjLiNew = Abc_NtkCreateBi( pNtkNew );
pObjLoNew = Abc_NtkCreateBo( pNtkNew );
Abc_ObjAddFanin( pObjNew, pObjLiNew );
Abc_ObjAddFanin( pObjLoNew, pObjNew );
if ( i == iState )
Abc_LatchSetInit1( pObjNew );
else
Abc_LatchSetInit0( pObjNew );
}
Abc_NtkAddDummyBoxNames( pNtkNew );
assert( Abc_NtkLatchNum(pNtkNew) == nStates );
assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) );
assert( Abc_NtkPoNum(pNtkNew) == Abc_NtkPoNum(pNtk) );
assert( Abc_NtkCiNum(pNtkNew) == Abc_NtkPiNum(pNtkNew) + nStates );
assert( Abc_NtkCoNum(pNtkNew) == Abc_NtkPoNum(pNtkNew) + nStates );
assert( Abc_NtkCiNum(pNtk) == Abc_NtkPiNum(pNtk) + nFlops );
assert( Abc_NtkCoNum(pNtk) == Abc_NtkPoNum(pNtk) + nFlops );
// create hot-to-log transformers
for ( i = 0; i < nFlops; i++ )
{
pObjNew = Abc_NtkCreateNode( pNtkNew );
for ( k = 0; k < nStates; k++ )
if ( (k >> i) & 1 )
Abc_ObjAddFanin( pObjNew, Abc_NtkCi(pNtkNew, Abc_NtkPiNum(pNtkNew)+k) );
assert( Abc_ObjFaninNum(pObjNew) == nStates/2 );
pObjNew->pData = Abc_SopCreateOr( pNtkNew->pManFunc, nStates/2, NULL );
// save the new flop
pObj = Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i );
pObj->pCopy = pObjNew;
}
// duplicate the nodes
vNodes = Abc_NtkDfs( pNtk, 0 );
Vec_PtrForEachEntry( vNodes, pObj, i )
{
pObj->pCopy = Abc_NtkDupObj( pNtkNew, pObj, 1 );
Abc_ObjForEachFanin( pObj, pFanin, k )
Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
}
Vec_PtrFree( vNodes );
// connect the POs
Abc_NtkForEachPo( pNtk, pObj, i )
Abc_ObjAddFanin( pObj->pCopy, Abc_ObjNotCond(Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj)) );
// write entries into the nodes
Abc_NtkForEachCo( pNtk, pObj, i )
pObj->pCopy = Abc_ObjNotCond(Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj));
// create log-to-hot transformers
for ( k = 0; k < nStates; k++ )
{
pObjNew = Abc_NtkCreateNode( pNtkNew );
for ( i = 0; i < nFlops; i++ )
{
pObj = Abc_NtkCo( pNtk, Abc_NtkPoNum(pNtk) + i );
Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(pObj->pCopy) );
pfCompl[i] = Abc_ObjIsComplement(pObj->pCopy) ^ !((k >> i) & 1);
}
pObjNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, nFlops, pfCompl );
// connect it to the flop input
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, Abc_NtkPoNum(pNtkNew)+k), pObjNew );
}
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkConvertOnehot(): Network check has failed.\n" );
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

18
src/base/abc/abcNtk.c
View File

@ -935,10 +935,10 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// int LargePiece = (4 << ABC_NUM_STEPS);
if ( pNtk == NULL )
return;
// ABC_FREE the HAIG
// free the HAIG
// if ( pNtk->pHaig )
// Abc_NtkHaigStop( pNtk );
// ABC_FREE EXDC Ntk
// free EXDC Ntk
if ( pNtk->pExdc )
Abc_NtkDelete( pNtk->pExdc );
if ( pNtk->pExcare )
@ -952,7 +952,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// make sure all the marks are clean
Abc_NtkForEachObj( pNtk, pObj, i )
{
// ABC_FREE large fanout arrays
// free large fanout arrays
// if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
// ABC_FREE( pObj->vFanouts.pArray );
// these flags should be always zero
@ -961,7 +961,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
assert( pObj->fMarkB == 0 );
assert( pObj->fMarkC == 0 );
}
// ABC_FREE the nodes
// free the nodes
if ( pNtk->pMmStep == NULL )
{
Abc_NtkForEachObj( pNtk, pObj, i )
@ -976,7 +976,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
ABC_FREE( pObj );
}
// ABC_FREE the arrays
// free the arrays
Vec_PtrFree( pNtk->vPios );
Vec_PtrFree( pNtk->vPis );
Vec_PtrFree( pNtk->vPos );
@ -992,14 +992,14 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj) : 0;
TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
// fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
// ABC_FREE the storage
// free the storage
if ( pNtk->pMmObj )
Extra_MmFixedStop( pNtk->pMmObj );
if ( pNtk->pMmStep )
Extra_MmStepStop ( pNtk->pMmStep );
// name manager
Nm_ManFree( pNtk->pManName );
// ABC_FREE the timing manager
// free the timing manager
if ( pNtk->pManTime )
Abc_ManTimeStop( pNtk->pManTime );
// start the functionality manager
@ -1015,7 +1015,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
pNtk->pManFunc = NULL;
else if ( !Abc_NtkHasBlackbox(pNtk) )
assert( 0 );
// ABC_FREE the hierarchy
// free the hierarchy
if ( pNtk->pDesign )
{
Abc_LibFree( pNtk->pDesign, pNtk );
@ -1023,7 +1023,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
}
// if ( pNtk->pBlackBoxes )
// Vec_IntFree( pNtk->pBlackBoxes );
// ABC_FREE node attributes
// free node attributes
Vec_PtrForEachEntry( pNtk->vAttrs, pAttrMan, i )
if ( pAttrMan )
{

4
src/base/abc/abcObj.c
View File

@ -71,9 +71,9 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
{
Abc_Ntk_t * pNtk = pObj->pNtk;
// int LargePiece = (4 << ABC_NUM_STEPS);
// ABC_FREE large fanout arrays
// free large fanout arrays
// if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece )
// ABC_FREE( pObj->vFanouts.pArray );
// free( pObj->vFanouts.pArray );
if ( pNtk->pMmStep == NULL )
{
ABC_FREE( pObj->vFanouts.pArray );

2
src/base/abc/abcUtil.c
View File

@ -1770,7 +1770,7 @@ void Abc_NtkCompareCones( Abc_Ntk_t * pNtk )
printf( "%4d CO %5d : Supp = %5d. Lev = %3d. Cone = %5d. Rev = %5d. COs = %3d (%3d).\n",
Iter, pPerms[i], Vec_PtrSize(vSupp), Abc_ObjLevel(Abc_ObjFanin0(pObj)), Vec_PtrSize(vNodes), Counter, CounterCos, CounterCosNew );
// ABC_FREE arrays
// free arrays
Vec_PtrFree( vSupp );
Vec_PtrFree( vNodes );
Vec_PtrFree( vReverse );

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

@ -27,7 +27,7 @@
#include "if.h"
#include "res.h"
#include "lpk.h"
#include "aig.h"
#include "giaAig.h"
#include "dar.h"
#include "mfs.h"
#include "mfx.h"
@ -39,7 +39,6 @@
#include "ssw.h"
#include "cgt.h"
#include "amap.h"
#include "gia.h"
#include "cec.h"
////////////////////////////////////////////////////////////////////////
@ -194,6 +193,7 @@ static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandOneHot ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -513,6 +513,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "onehot", Abc_CommandOneHot, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "dretime", Abc_CommandDRetime, 1 );
@ -598,7 +599,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "AIG", "&psig", Abc_CommandAbc9PSig, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&status", Abc_CommandAbc9Status, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&show", Abc_CommandAbc9Show, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&hash", Abc_CommandAbc9Hash, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&st", Abc_CommandAbc9Hash, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&topand", Abc_CommandAbc9Topand, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&cof", Abc_CommandAbc9Cof, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&trim", Abc_CommandAbc9Trim, 0 );
@ -11945,7 +11946,7 @@ usage:
fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->fEpsilon );
fprintf( pErr, "\t-m : toggles using MUX matching [default = %s]\n", pPars->fUseMuxes? "yes": "no" );
fprintf( pErr, "\t-x : toggles using XOR matching [default = %s]\n", pPars->fUseXors? "yes": "no" );
fprintf( pErr, "\t-i : toggles assuming inverters are ABC_FREE [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
fprintf( pErr, "\t-i : toggles assuming inverters are free [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@ -13094,7 +13095,74 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: undc [-h]\n" );
fprintf( pErr, "\t converts latches with DC init values into ABC_FREE PIs\n" );
fprintf( pErr, "\t converts latches with DC init values into free PIs\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandOneHot( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
extern Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "The current network is combinational.\n" );
return 0;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( pErr, "This command works only for logic networks.\n" );
return 0;
}
// get the new network
pNtkRes = Abc_NtkConvertOnehot( pNtk );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Converting to one-hot encoding has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: onehot [-h]\n" );
fprintf( pErr, "\t converts natural encoding into one-hot encoding\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -15030,7 +15098,7 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fNew = 1;
fNew = 0;
fComb = 0;
nFrames = 32;
nWords = 8;
@ -18381,22 +18449,28 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConfMax;
int fDynamic;
int fExtend;
int fSkipProof;
int nFramesBmc;
int nConfMaxBmc;
int fVerbose;
int c;
extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
nFramesMax = 10;
nConfMax = 10000;
fDynamic = 1;
fExtend = 0;
fVerbose = 0;
nFramesMax = 10;
nConfMax = 10000;
fDynamic = 1;
fExtend = 0;
fSkipProof = 0;
nFramesBmc = 2000;
nConfMaxBmc = 5000;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF )
{
switch ( c )
{
@ -18422,12 +18496,37 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMax < 0 )
goto usage;
break;
case 'G':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" );
goto usage;
}
nFramesBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFramesBmc < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
nConfMaxBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfMaxBmc < 0 )
goto usage;
break;
case 'd':
fDynamic ^= 1;
break;
case 'e':
fExtend ^= 1;
break;
case 's':
fSkipProof ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -18454,7 +18553,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pNtkRes == NULL )
{
if ( pNtk->pSeqModel == NULL )
@ -18465,12 +18564,16 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: abs [-FC num] [-devh]\n" );
fprintf( pErr, "\t proof-based abstraction from UNSAT core of the BMC instance\n" );
fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" );
fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" );
fprintf( pErr, "\t followed by counter-example-based abstraction\n" );
fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax );
fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc );
fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc );
fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" );
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;
@ -22128,11 +22231,15 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c;
int fAddStrash = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
{
switch ( c )
{
case 'a':
fAddStrash ^= 1;
break;
case 'h':
goto usage;
default:
@ -22144,13 +22251,14 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
return 1;
}
pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig );
pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig, fAddStrash );
Gia_ManStop( pTemp );
return 0;
usage:
fprintf( stdout, "usage: &hash [-h]\n" );
fprintf( stdout, "usage: &st [-ah]\n" );
fprintf( stdout, "\t performs structural hashing\n" );
fprintf( stdout, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@ -22186,7 +22294,7 @@ int Abc_CommandAbc9Topand( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pAig == NULL )
{
printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
printf( "Abc_CommandAbc9Topand(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pAig) > 0 )

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

@ -64,7 +64,7 @@ printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
// report the classes
// if ( fVerbose )
// Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
// ABC_FREE stuff
// free stuff
Vec_PtrFree( vMapping );
Ivy_ManStop( pFraig );
Ivy_ManStop( pFrames );

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

@ -19,7 +19,7 @@
***********************************************************************/
#include "abc.h"
#include "aig.h"
#include "giaAig.h"
#include "saig.h"
#include "dar.h"
#include "cnf.h"
@ -2299,7 +2299,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
RetValue = 1;
}
}
else
{
RetValue = 0;
@ -2375,7 +2375,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
pGia = Gia_ManFromAig( pMan );
if ( Gia_ManSimSimulate( pGia, pPars ) )
{
if ( (pCex = pMan->pSeqModel) )
if ( (pCex = (Fra_Cex_t *)pGia->pCexSeq) )
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
@ -2404,8 +2404,13 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
pCex = Fra_SmlGetCounterExample( pSml );
if ( pCex )
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
if ( status == 0 )
printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
}
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
@ -2557,7 +2562,7 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose )
Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
@ -2567,7 +2572,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, 0, fVerbose );
pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pTemp->pSeqModel )
{
ABC_FREE( pNtk->pModel );
@ -3380,7 +3385,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
return NULL;
/*
Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, 1 );
pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;

4
src/base/abci/abcFxu.c
View File

@ -177,12 +177,12 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
{
int i;
// ABC_FREE the arrays of new fanins
// free the arrays of new fanins
if ( p->vFaninsNew )
for ( i = 0; i < p->vFaninsNew->nSize; i++ )
if ( p->vFaninsNew->pArray[i] )
Vec_IntFree( p->vFaninsNew->pArray[i] );
// ABC_FREE the arrays
// free the arrays
if ( p->vSops ) Vec_PtrFree( p->vSops );
if ( p->vSopsNew ) Vec_PtrFree( p->vSopsNew );
if ( p->vFanins ) Vec_PtrFree( p->vFanins );

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

@ -691,7 +691,7 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
Hop_ManStop( pMan );
// ABC_FREE HAIG
// free HAIG
return pNtkAig;
}

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

@ -349,7 +349,7 @@ void Abc_MvDecompose( Mv_Man_t * p )
printf( "%d ", Vec_PtrSize(vCofs) );
Vec_PtrFree( vCofs );
// ABC_FREE the cofactors
// free the cofactors
for ( v1 = 0; v1 < 4; v1++ )
for ( v2 = 0; v2 < 4; v2++ )
Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );

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

@ -64,7 +64,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
int nPis; // the number of primary inputs
int nPos; // the number of primary outputs
} ParsNew, ParsBest = { 0 };
// ABC_FREE storage for the name
// free storage for the name
if ( pNtk == NULL )
{
ABC_FREE( ParsBest.pName );

Some files were not shown because too many files have changed in this diff Show More