Skip to content

A
abc
Commit 14c01eac by Alan Mishchenko
Options

Version abc71218

parent 126637dd
Showing with 444 additions and 70 deletions
src/aig/aig/aig.h
......@@ -160,6 +160,8 @@ struct Aig_Man_t_
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
static inline int Aig_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Aig_Int2Float( int Num ) { return *((float *)&Num); }
static inline int Aig_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
static inline int Aig_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
static inline char * Aig_UtilStrsav( char * s ) { return s ? strcpy(ALLOC(char, strlen(s)+1), s) : NULL; }
......
src/aig/aig/module.make
SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigDfs.c \
src/aig/aig/aigFanout.c \
src/aig/aig/aigFrames.c \
src/aig/aig/aigHaig.c \
src/aig/aig/aigMan.c \
src/aig/aig/aigMem.c \
src/aig/aig/aigMffc.c \
......@@ -10,8 +12,10 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigPart.c \
src/aig/aig/aigRepr.c \
src/aig/aig/aigRet.c \
src/aig/aig/aigRetF.c \
src/aig/aig/aigScl.c \
src/aig/aig/aigSeq.c \
src/aig/aig/aigShow.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTime.c \
src/aig/aig/aigTiming.c \
......
src/aig/dar/darCut.c
......@@ -479,7 +479,7 @@ static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
int i, k, nLeaves;
assert( pCut->fUsed );
// compute the truth support of the cut's function
// compute the support of the cut's function
nLeaves = pCut->nLeaves;
for ( i = 0; i < (int)pCut->nLeaves; i++ )
if ( (uTruth & uMasks[i][0]) == ((uTruth & uMasks[i][1]) >> (1 << i)) )
......
src/aig/fra/fra.h
......@@ -76,6 +76,7 @@ struct Fra_Par_t_
int nFramesP; // the number of timeframes to in the prefix
int nFramesK; // the number of timeframes to unroll
int nMaxImps; // the maximum number of implications to consider
int nMaxLevs; // the maximum number of levels to consider
int fRewrite; // use rewriting for constraint reduction
int fLatchCorr; // computes latch correspondence only
int fUseImps; // use implications
......@@ -245,7 +246,7 @@ extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
extern void Fra_ClassesStop( Fra_Cla_t * p );
extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs );
extern int Fra_ClassesRefine( Fra_Cla_t * p );
extern int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
extern int Fra_ClassesCountLits( Fra_Cla_t * p );
......@@ -274,7 +275,7 @@ extern double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
extern int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
/*=== fraInd.c ========================================================*/
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
/*=== fraLcr.c ========================================================*/
extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
......
src/aig/fra/fraClass.c
......@@ -270,7 +270,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
SeeAlso []
***********************************************************************/
void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
{
Aig_Obj_t ** ppTable, ** ppNexts;
Aig_Obj_t * pObj, * pTemp;
......@@ -296,8 +296,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
// skip the node with more that the given number of levels
// if ( pObj->Level > 3 )
// continue;
if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
continue;
}
// hash the node by its simulation info
iEntry = p->pFuncNodeHash( pObj, nTableSize );
......
src/aig/fra/fraInd.c
......@@ -243,7 +243,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
......@@ -282,12 +282,13 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
pPars->nFramesP = nFramesP;
pPars->nFramesK = nFramesK;
pPars->nMaxImps = nMaxImps;
pPars->nMaxLevs = nMaxLevs;
pPars->fVerbose = fVerbose;
pPars->fRewrite = fRewrite;
pPars->fLatchCorr = fLatchCorr;
pPars->fUseImps = fUseImps;
pPars->fWriteImps = fWriteImps;
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
// derive and refine e-classes using K initialized frames
......@@ -313,7 +314,7 @@ if ( fVerbose )
{
PRT( "Time", clock() - clk );
}
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
// Fra_ClassesPostprocess( p->pCla );
// allocate new simulation manager for simulating counter-examples
Fra_SmlStop( p->pSml );
......
src/aig/fra/fraLcr.c
......@@ -550,7 +550,7 @@ timeSim = clock() - clk2;
// get preliminary info about equivalence classes
pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
Fra_ClassesPrepare( p->pCla, 1 );
Fra_ClassesPrepare( p->pCla, 1, 0 );
p->pCla->pFuncNodeIsConst = Fra_LcrNodeIsConst;
p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
Fra_SmlStop( pTemp->pSml );
......
src/aig/fra/fraSec.c
......@@ -49,7 +49,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
{
nFrames = nFramesFix;
// perform seq sweeping for one frame number
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
}
else
{
......@@ -57,7 +57,7 @@ int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
for ( nFrames = 1; ; nFrames++ )
{
clk = clock();
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
......@@ -185,7 +185,7 @@ PRT( "Time", clock() - clk );
for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
{
clk = clock();
pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
Aig_ManStop( pTemp );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
......
src/aig/fra/fraSim.c
......@@ -685,7 +685,7 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
Fra_SmlSimulateOne( p->pSml );
if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
return;
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
// Fra_ClassesPrint( p->pCla, 0 );
if ( fVerbose )
printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
......
src/aig/fra/module.make
SRC += src/aig/fra/fraBmc.c \
src/aig/fra/fraCec.c \
src/aig/fra/fraClass.c \
src/aig/fra/fraClau.c \
src/aig/fra/fraClaus.c \
src/aig/fra/fraCnf.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraImp.c \
src/aig/fra/fraInd.c \
src/aig/fra/fraLcr.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraPart.c \
src/aig/fra/fraSat.c \
src/aig/fra/fraSec.c \
src/aig/fra/fraSim.c
src/aig/ntl/module.make 0 → 100644
SRC += src/aig/mem/ntlAig.c \
src/aig/mem/ntlCheck.c \
src/aig/mem/ntlDfs.c \
src/aig/mem/ntlMan.c \
src/aig/mem/ntlMap.c \
src/aig/mem/ntlObj.c \
src/aig/mem/ntlReadBlif.c \
src/aig/mem/ntlTable.c \
src/aig/mem/ntlWriteBlif.c
src/aig/ntl/ntl.h
......@@ -86,6 +86,8 @@ struct Ntl_Mod_t_
Ntl_Net_t ** pTable; // the hash table of names into nets
int nTableSize; // the allocated table size
int nEntries; // the number of entries in the hash table
// delay information
Vec_Int_t * vDelays;
};
struct Ntl_Obj_t_
......@@ -242,6 +244,7 @@ extern char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
extern Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
extern Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
extern int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
/*=== ntlReadBlif.c ==========================================================*/
extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
/*=== ntlWriteBlif.c ==========================================================*/
......
src/aig/ntl/ntlMan.c
......@@ -152,6 +152,7 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
***********************************************************************/
void Ntl_ModelFree( Ntl_Mod_t * p )
{
if ( p->vDelays ) Vec_IntFree( p->vDelays );
Vec_PtrFree( p->vObjs );
Vec_PtrFree( p->vPis );
Vec_PtrFree( p->vPos );
......
src/aig/ntl/ntlReadBlif.c
......@@ -36,6 +36,7 @@ struct Ioa_ReadMod_t_
Vec_Ptr_t * vLatches; // .latch lines
Vec_Ptr_t * vNames; // .names lines
Vec_Ptr_t * vSubckts; // .subckt lines
Vec_Ptr_t * vDelays; // .delay lines
int fBlackBox; // indicates blackbox model
// the resulting network
Ntl_Mod_t * pNtk;
......@@ -79,6 +80,7 @@ static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLin
static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine );
static int Ioa_ReadCharIsSpace( char s ) { return s == ' ' || s == '\t' || s == '\r' || s == '\n'; }
......@@ -245,6 +247,7 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc()
p->vLatches = Vec_PtrAlloc( 512 );
p->vNames = Vec_PtrAlloc( 512 );
p->vSubckts = Vec_PtrAlloc( 512 );
p->vDelays = Vec_PtrAlloc( 512 );
return p;
}
......@@ -266,6 +269,7 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
Vec_PtrFree( p->vLatches );
Vec_PtrFree( p->vNames );
Vec_PtrFree( p->vSubckts );
Vec_PtrFree( p->vDelays );
free( p );
}
......@@ -492,6 +496,8 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
Vec_PtrPush( p->pLatest->vOutputs, pCur );
else if ( !strncmp(pCur, "subckt", 6) )
Vec_PtrPush( p->pLatest->vSubckts, pCur );
else if ( !strncmp(pCur, "delay", 5) )
Vec_PtrPush( p->pLatest->vDelays, pCur );
else if ( !strncmp(pCur, "blackbox", 8) )
p->pLatest->fBlackBox = 1;
else if ( !strncmp(pCur, "model", 5) )
......@@ -551,6 +557,10 @@ static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
return;
// parse the delay info
Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
return;
}
}
......@@ -841,6 +851,82 @@ static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
return 1;
}
/**Function*************************************************************
Synopsis [Parses the subckt line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
{
Vec_Ptr_t * vTokens = p->pMan->vTokens;
int RetValue1, RetValue2, Number1, Number2, Temp;
char * pToken;
float Delay;
assert( sizeof(float) == sizeof(int) );
Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
pToken = Vec_PtrEntry(vTokens,0);
assert( !strcmp(pToken, "delay") );
if ( Vec_PtrSize(vTokens) < 2 && Vec_PtrSize(vTokens) > 4 )
{
sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (1, 2, or 3).", Ioa_ReadGetLine(p->pMan, pToken) );
return 0;
}
// find the delay number
Delay = atof( Vec_PtrEntryLast(vTokens) );
if ( Delay < 0.0 )
{
sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
return 0;
}
// find the PI/PO numbers
RetValue1 = 0; Number1 = -1;
if ( Vec_PtrSize(vTokens) > 2 )
{
RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number1 );
if ( RetValue1 == 0 )
{
sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
return 0;
}
}
RetValue2 = 0; Number2 = -1;
if ( Vec_PtrSize(vTokens) > 3 )
{
RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 2), &Number2 );
if ( RetValue2 == 0 )
{
sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 2) );
return 0;
}
}
if ( RetValue1 == RetValue2 && RetValue1 )
{
sprintf( p->pMan->sError, "Line %d: Both signals \"%s\" and \"%s\" listed appear to be PIs or POs.",
Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), Vec_PtrEntry(vTokens, 2) );
return 0;
}
if ( RetValue2 < RetValue1 )
{
Temp = RetValue2; RetValue2 = RetValue1; RetValue1 = Temp;
Temp = Number2; Number2 = Number1; Number1 = Temp;
}
assert( RetValue1 == 0 || RetValue1 == -1 );
assert( RetValue2 == 0 || RetValue2 == 1 );
// store the values
if ( p->pNtk->vDelays == NULL )
p->pNtk->vDelays = Vec_IntAlloc( 100 );
Vec_IntPush( p->pNtk->vDelays, Number1 );
Vec_IntPush( p->pNtk->vDelays, Number2 );
Vec_IntPush( p->pNtk->vDelays, Aig_Float2Int(Delay) );
return 1;
}
/**Function*************************************************************
......
src/aig/ntl/ntlTable.c
......@@ -171,6 +171,45 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
return 1;
}
/**Function*************************************************************
Synopsis [Returns -1, 0, +1 (when it is PI, not found, or PO).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
{
Ntl_Net_t * pNet;
Ntl_Obj_t * pObj;
int i;
*pNumber = -1;
pNet = Ntl_ModelFindNet( p, pName );
if ( pNet == NULL )
return 0;
Ntl_ModelForEachPo( p, pObj, i )
{
if ( Ntl_ObjFanin0(pObj) == pNet )
{
*pNumber = i;
return 1;
}
}
Ntl_ModelForEachPi( p, pObj, i )
{
if ( Ntl_ObjFanout0(pObj) == pNet )
{
*pNumber = i;
return -1;
}
}
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcDar.c
......@@ -1022,7 +1022,7 @@ PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
{
Fraig_Params_t Params;
Abc_Ntk_t * pNtkAig, * pNtkFraig;
......@@ -1046,7 +1046,7 @@ PRT( "Initial fraiging time", clock() - clk );
if ( pMan == NULL )
return NULL;
pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
Aig_ManStop( pTemp );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
......
src/base/abci/abcPrint.c
......@@ -60,9 +60,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
fprintf( pFile, "%-13s:", pNtk->pName );
if ( Abc_NtkAssertNum(pNtk) )
fprintf( pFile, " i/o/a = %4d/%4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
fprintf( pFile, " i/o/a = %5d/%5d/%5d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
else
fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
fprintf( pFile, " i/o = %5d/%5d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) );
if ( Abc_NtkIsNetlist(pNtk) )
{
......@@ -86,7 +86,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
else
{
fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
fprintf( pFile, " net = %5d", Abc_NtkGetTotalFanins(pNtk) );
fprintf( pFile, " edge = %6d", Abc_NtkGetTotalFanins(pNtk) );
}
if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
......
src/map/if/if.h
......@@ -74,7 +74,7 @@ typedef struct If_Set_t_ If_Set_t;
// parameters
struct If_Par_t_
{
// user-controlable paramters
// user-controlable parameters
int nLutSize; // the LUT size
int nCutsMax; // the max number of cuts
int nFlowIters; // the number of iterations of area recovery
......@@ -85,6 +85,8 @@ struct If_Par_t_
int fFancy; // a fancy feature
int fExpRed; // expand/reduce of the best cuts
int fLatchPaths; // reset timing on latch paths
int fEdge; // uses edge-based cut selection heuristics
int fCutMin; // performs cut minimization by removing functionally reducdant variables
int fSeqMap; // sequential mapping
int fVerbose; // the verbosity flag
// internal parameters
......@@ -158,6 +160,7 @@ struct If_Man_t_
If_Set_t * pMemCi; // memory for CI cutsets
If_Set_t * pMemAnd; // memory for AND cutsets
If_Set_t * pFreeList; // the list of free cutsets
int nSmallSupp; // the small support
};
// priority cut
......@@ -166,6 +169,7 @@ struct If_Cut_t_
float Delay; // delay of the cut
float Area; // area (or area-flow) of the cut
float AveRefs; // the average number of leaf references
float Edge; // the edge flow
unsigned uSign; // cut signature
unsigned Cost : 14; // the user's cost of the cut
unsigned fCompl : 1; // the complemented attribute
......@@ -258,6 +262,7 @@ static inline void If_CutSetData( If_Cut_t * pCut, void * pData ) { *
static inline int If_CutLeaveNum( If_Cut_t * pCut ) { return pCut->nLeaves; }
static inline unsigned * If_CutTruth( If_Cut_t * pCut ) { return pCut->pTruth; }
static inline unsigned If_CutSuppMask( If_Cut_t * pCut ) { return (~(unsigned)0) >> (32-pCut->nLeaves); }
static inline int If_CutTruthWords( int nVarsMax ) { return nVarsMax <= 5 ? 1 : (1 << (nVarsMax - 5)); }
static inline int If_CutPermWords( int nVarsMax ) { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); }
......@@ -320,14 +325,19 @@ static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { r
extern int If_ManPerformMapping( If_Man_t * p );
extern int If_ManPerformMappingComb( If_Man_t * p );
/*=== ifCut.c ============================================================*/
extern float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
extern float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels );
extern float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels );
extern float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels );
extern void If_CutPrint( If_Man_t * p, If_Cut_t * pCut );
extern void If_CutPrintTiming( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutFlow( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutAreaFlow( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutAreaDeref( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutAreaRef( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeDeref( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeRef( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut );
extern int If_CutFilter( If_Set_t * pCutSet, If_Cut_t * pCut );
extern void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut );
extern int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut );
......
src/map/if/ifMan.c
......@@ -124,6 +124,7 @@ void If_ManRestart( If_Man_t * p )
***********************************************************************/
void If_ManStop( If_Man_t * p )
{
// printf( "Small support = %d.\n", p->nSmallSupp );
Vec_PtrFree( p->vCis );
Vec_PtrFree( p->vCos );
Vec_PtrFree( p->vObjs );
......
src/map/if/ifMap.c
......@@ -77,7 +77,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
pObj->EstRefs = (float)((2.0 * pObj->EstRefs + pObj->nRefs) / 3.0);
}
if ( Mode && pObj->nRefs > 0 )
If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY );
If_CutAreaDeref( p, If_ObjCutBest(pObj) );
// prepare the cutset
pCutSet = If_ManSetupNodeCutSet( p, pObj );
......@@ -89,7 +89,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
// recompute the parameters of the best cut
pCut->Delay = If_CutDelay( p, pCut );
assert( pCut->Delay <= pObj->Required + p->fEpsilon );
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
if ( p->pPars->fEdge )
pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
// save the best cut from the previous iteration
if ( !fPreprocess )
If_CutCopy( p, pCutSet->ppCuts[pCutSet->nCuts++], pCut );
......@@ -129,7 +131,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
continue;
// compute area of the cut (this area may depend on the application specific cost)
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
if ( p->pPars->fEdge )
pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
// insert the cut into storage
If_CutSort( p, pCutSet, pCut );
......@@ -147,7 +151,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
// ref the selected cut
if ( Mode && pObj->nRefs > 0 )
If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
If_CutAreaRef( p, If_ObjCutBest(pObj) );
// call the user specified function for each cut
if ( p->pPars->pFuncUser )
......@@ -179,7 +183,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
// prepare
if ( Mode && pObj->nRefs > 0 )
If_CutDeref( p, If_ObjCutBest(pObj), IF_INFINITY );
If_CutAreaDeref( p, If_ObjCutBest(pObj) );
// remove elementary cuts
for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
......@@ -213,7 +217,9 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
assert( pCut->fCompl == 0 );
pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase); // why ^= ?
// compute area of the cut (this area may depend on the application specific cost)
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, IF_INFINITY ) : If_CutFlow( p, pCut );
pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
if ( p->pPars->fEdge )
pCut->Edge = (Mode == 2)? If_CutEdgeDerefed( p, pCut ) : If_CutEdgeFlow( p, pCut );
pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
// insert the cut into storage
If_CutSort( p, pCutSet, pCut );
......@@ -232,7 +238,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
// ref the selected cut
if ( Mode && pObj->nRefs > 0 )
If_CutRef( p, If_ObjCutBest(pObj), IF_INFINITY );
If_CutAreaRef( p, If_ObjCutBest(pObj) );
// free the cuts
If_ManDerefChoiceCutSet( p, pObj );
......
src/map/if/ifReduce.c
......@@ -156,17 +156,17 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
// get the delay
DelayOld = pCut->Delay;
// get the area
AreaBef = If_CutAreaRefed( p, pCut, IF_INFINITY );
AreaBef = If_CutAreaRefed( p, pCut );
// if ( AreaBef == 1 )
// return;
// the cut is non-trivial
If_ManImproveNodePrepare( p, pObj, nLimit, vFront, vFrontOld, vVisited );
// iteratively modify the cut
If_CutDeref( p, pCut, IF_INFINITY );
If_CutAreaDeref( p, pCut );
CostBef = If_ManImproveCutCost( p, vFront );
If_ManImproveNodeFaninCompact( p, pObj, nLimit, vFront, vVisited );
CostAft = If_ManImproveCutCost( p, vFront );
If_CutRef( p, pCut, IF_INFINITY );
If_CutAreaRef( p, pCut );
assert( CostBef >= CostAft );
// clean up
Vec_PtrForEachEntry( vVisited, pFanin, i )
......@@ -175,11 +175,11 @@ void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr
If_ManImproveNodeUpdate( p, pObj, vFront );
pCut->Delay = If_CutDelay( p, pCut );
// get the new area
AreaAft = If_CutAreaRefed( p, pCut, IF_INFINITY );
AreaAft = If_CutAreaRefed( p, pCut );
if ( AreaAft > AreaBef || pCut->Delay > pObj->Required + p->fEpsilon )
{
If_ManImproveNodeUpdate( p, pObj, vFrontOld );
AreaAft = If_CutAreaRefed( p, pCut, IF_INFINITY );
AreaAft = If_CutAreaRefed( p, pCut );
assert( AreaAft == AreaBef );
pCut->Delay = DelayOld;
}
......@@ -257,13 +257,13 @@ void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront
int i;
pCut = If_ObjCutBest(pObj);
// deref node's cut
If_CutDeref( p, pCut, IF_INFINITY );
If_CutAreaDeref( p, pCut );
// update the node's cut
pCut->nLeaves = Vec_PtrSize(vFront);
Vec_PtrForEachEntry( vFront, pFanin, i )
pCut->pLeaves[i] = pFanin->Id;
// ref the new cut
If_CutRef( p, pCut, IF_INFINITY );
If_CutAreaRef( p, pCut );
}
......@@ -507,9 +507,9 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
// deref the cut if the node is refed
if ( pObj->nRefs > 0 )
If_CutDeref( p, pCut, IF_INFINITY );
If_CutAreaDeref( p, pCut );
// get the area
AreaBef = If_CutAreaDerefed( p, pCut, IF_INFINITY );
AreaBef = If_CutAreaDerefed( p, pCut );
// get the fanin support
if ( pFanin0->nRefs > 2 && pCut0->Delay < pObj->Required + p->fEpsilon )
// if ( pSupp0->nRefs > 0 && pSupp0->Delay < pSupp->DelayR ) // this leads to 2% worse results
......@@ -535,7 +535,7 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
if ( RetValue )
{
pCutR->Delay = If_CutDelay( p, pCutR );
AreaAft = If_CutAreaDerefed( p, pCutR, IF_INFINITY );
AreaAft = If_CutAreaDerefed( p, pCutR );
// update the best cut
if ( AreaAft < AreaBef - p->fEpsilon && pCutR->Delay < pObj->Required + p->fEpsilon )
If_CutCopy( p, pCut, pCutR );
......@@ -544,7 +544,7 @@ void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit )
pCut->Delay = If_CutDelay( p, pCut );
// ref the cut if the node is refed
if ( pObj->nRefs > 0 )
If_CutRef( p, pCut, IF_INFINITY );
If_CutRef( p, pCut );
*/
}
......
src/map/if/ifTruth.c
......@@ -24,6 +24,8 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -158,6 +160,123 @@ void If_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
/**Function*************************************************************
Synopsis [Shrinks the truth table according to the phase.]
Description [The input and output truth tables are in pIn/pOut. The current number
of variables is nVars. The total number of variables in nVarsAll. The last argument
(Phase) contains shows what variables should remain.]
SideEffects []
SeeAlso []
***********************************************************************/
void If_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
{
unsigned * pTemp;
int i, k, Var = 0, Counter = 0;
for ( i = 0; i < nVarsAll; i++ )
if ( Phase & (1 << i) )
{
for ( k = i-1; k >= Var; k-- )
{
If_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
pTemp = pIn; pIn = pOut; pOut = pTemp;
Counter++;
}
Var++;
}
assert( Var == nVars );
// swap if it was moved an even number of times
if ( fReturnIn ^ !(Counter & 1) )
If_TruthCopy( pOut, pIn, nVarsAll );
}
/**Function*************************************************************
Synopsis [Returns 1 if TT depends on the given variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_CutTruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
{
int nWords = If_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
return 1;
return 0;
case 1:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
return 1;
return 0;
case 2:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
return 1;
return 0;
case 3:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
return 1;
return 0;
case 4:
for ( i = 0; i < nWords; i++ )
if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
return 1;
return 0;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
if ( pTruth[i] != pTruth[Step+i] )
return 1;
pTruth += 2*Step;
}
return 0;
}
}
/**Function*************************************************************
Synopsis [Returns support of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned If_CutTruthSupport( unsigned * pTruth, int nVars, int * pnSuppSize )
{
int i, Support = 0;
int nSuppSize = 0;
for ( i = 0; i < nVars; i++ )
if ( If_CutTruthVarInSupport( pTruth, nVars, i ) )
{
Support |= (1 << i);
nSuppSize++;
}
*pnSuppSize = nSuppSize;
return Support;
}
/**Function*************************************************************
Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
Description []
......@@ -197,7 +316,7 @@ static inline unsigned If_CutTruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
***********************************************************************/
void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
{
extern void Kit_FactorTest( unsigned * pTruth, int nVars );
extern void If_CutFactorTest( unsigned * pTruth, int nVars );
// permute the first table
if ( fCompl0 ^ pCut0->fCompl )
......@@ -218,11 +337,66 @@ void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
else
If_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
// minimize the support of the cut
if ( p->pPars->fCutMin )
If_CutTruthMinimize( p, pCut );
// perform
// Kit_FactorTest( If_CutTruth(pCut), pCut->nLimit );
// printf( "%d ", If_CutLeaveNum(pCut) - Kit_TruthSupportSize(If_CutTruth(pCut), If_CutLeaveNum(pCut)) );
// If_CutFactorTest( If_CutTruth(pCut), pCut->nLimit );
// printf( "%d ", If_CutLeaveNum(pCut) - If_CutTruthSupportSize(If_CutTruth(pCut), If_CutLeaveNum(pCut)) );
}
/**Function*************************************************************
Synopsis [Minimize support of the cut.]
Description [Returns 1 if the node's support has changed]
SideEffects []
SeeAlso []
***********************************************************************/
int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut )
{
unsigned uSupport;
int nSuppSize, i, k;
// compute the support of the cut's function
uSupport = If_CutTruthSupport( If_CutTruth(pCut), If_CutLeaveNum(pCut), &nSuppSize );
if ( nSuppSize == If_CutLeaveNum(pCut) )
return 0;
// TEMPORARY
if ( nSuppSize < 2 )
{
p->nSmallSupp++;
return 0;
}
// if ( If_CutLeaveNum(pCut) - nSuppSize > 1 )
// return 0;
//printf( "%d %d ", If_CutLeaveNum(pCut), nSuppSize );
// shrink the truth table
If_TruthShrink( p->puTemp[0], If_CutTruth(pCut), nSuppSize, pCut->nLimit, uSupport, 1 );
// update leaves and signature
pCut->uSign = 0;
for ( i = k = 0; i < If_CutLeaveNum(pCut); i++ )
{
if ( !(uSupport & (1 << i)) )
continue;
pCut->pLeaves[k++] = pCut->pLeaves[i];
pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
}
assert( k == nSuppSize );
pCut->nLeaves = nSuppSize;
// verify the result
// uSupport = If_CutTruthSupport( If_CutTruth(pCut), If_CutLeaveNum(pCut), &nSuppSize );
// assert( nSuppSize == If_CutLeaveNum(pCut) );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/opt/lpk/lpkCore.c
......@@ -446,10 +446,6 @@ p->timeTruth3 += clock() - clk;
// pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
// printf( "Saved truth table in file \"%s\".\n", pFileName );
}
if ( p->pObj->Id == 33 && i == 0 )
{
int x = 0;
}
// update the network
nNodesBef = Abc_NtkNodeNum(p->pNtk);
......@@ -512,6 +508,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
// get the number of inputs
pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
if ( pPars->nLutSize > 6 )
pPars->nLutSize = 6;
// adjust the number of crossbars based on LUT size
if ( pPars->nVarsShared > pPars->nLutSize - 2 )
pPars->nVarsShared = pPars->nLutSize - 2;
......
src/opt/lpk/lpkCut.c
......@@ -24,7 +24,7 @@
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -489,7 +489,7 @@ void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
if ( Abc_ObjIsCi(pObj) )
return;
assert( Abc_ObjIsNode(pObj) );
assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
// assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
// if the node is not in the MFFC, check the limit
if ( !Abc_NodeIsTravIdCurrent(pObj) )
......
src/opt/res/resCore.c
......@@ -246,6 +246,8 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( !Abc_ObjIsNode(pObj) )
continue;
if ( Abc_ObjFaninNum(pObj) > 8 )
continue;
if ( pObj->Id > nNodesOld )
break;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment