Skip to content

A
abc
Commit f65983c2 by Alan Mishchenko
Options

Version abc80228

parent 7d23cc52
Showing with 600 additions and 167 deletions
abc.dsp
......@@ -2378,6 +2378,10 @@ SOURCE=.\src\misc\espresso\verify.c
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\misc\util\port_type.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\util\util_hack.h
# End Source File
# End Group
......
src/aig/aig/aig.h
......@@ -521,9 +521,14 @@ extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
extern Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose );
extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
/*=== aigPartReg.c =========================================================*/
extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
extern Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
/*=== aigRepr.c =========================================================*/
extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
extern void Aig_ManReprStop( Aig_Man_t * p );
......@@ -532,6 +537,7 @@ extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern void Aig_ManMarkValidChoices( Aig_Man_t * p );
extern int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack );
/*=== aigRet.c ========================================================*/
extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
/*=== aigRetF.c ========================================================*/
......
src/aig/aig/aigPart.c
......@@ -772,6 +772,135 @@ if ( fVerbose )
/**Function*************************************************************
Synopsis [Perform the smart partitioning.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose )
{
Vec_Ptr_t * vPartSuppsBit;
Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
int i, iPart, iOut, clk;
// add output number to each
clk = clock();
vSupports = Aig_ManSupportsRegisters( pAig );
assert( Vec_PtrSize(vSupports) == Aig_ManRegNum(pAig) );
Vec_PtrForEachEntry( vSupports, vOne, i )
Vec_IntPush( vOne, i );
if ( fVerbose )
{
PRT( "Supps", clock() - clk );
}
// start char-based support representation
vPartSuppsBit = Vec_PtrAlloc( 1000 );
// create partitions
clk = clock();
vPartsAll = Vec_PtrAlloc( 256 );
vPartSuppsAll = Vec_PtrAlloc( 256 );
Vec_PtrForEachEntry( vSupports, vOne, i )
{
// get the output number
iOut = Vec_IntPop(vOne);
// find closely matching part
iPart = Aig_ManPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsBit, nSuppSizeLimit, vOne );
if ( iPart == -1 )
{
// create new partition
vPart = Vec_IntAlloc( 32 );
Vec_IntPush( vPart, iOut );
// create new partition support
vPartSupp = Vec_IntDup( vOne );
// add this partition and its support
Vec_PtrPush( vPartsAll, vPart );
Vec_PtrPush( vPartSuppsAll, vPartSupp );
Vec_PtrPush( vPartSuppsBit, Aig_ManSuppCharStart(vOne, Vec_PtrSize(vSupports)) );
}
else
{
// add output to this partition
vPart = Vec_PtrEntry( vPartsAll, iPart );
Vec_IntPush( vPart, iOut );
// merge supports
vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart );
vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
Vec_IntFree( vTemp );
// reinsert new support
Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
Aig_ManSuppCharAdd( Vec_PtrEntry(vPartSuppsBit, iPart), vOne, Vec_PtrSize(vSupports) );
}
}
// stop char-based support representation
Vec_PtrForEachEntry( vPartSuppsBit, vTemp, i )
free( vTemp );
Vec_PtrFree( vPartSuppsBit );
//printf( "\n" );
if ( fVerbose )
{
PRT( "Parts", clock() - clk );
}
clk = clock();
// reorder partitions in the decreasing order of support sizes
// remember partition number in each partition support
Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
Vec_IntPush( vOne, i );
// sort the supports in the decreasing order
Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 );
// reproduce partitions
vPartsAll2 = Vec_PtrAlloc( 256 );
Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) );
Vec_PtrFree( vPartsAll );
vPartsAll = vPartsAll2;
// compact small partitions
// Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll );
Aig_ManPartitionCompact( vPartsAll, vPartSuppsAll, nSuppSizeLimit );
if ( fVerbose )
// Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll );
printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
if ( fVerbose )
{
//PRT( "Comps", clock() - clk );
}
// cleanup
Vec_VecFree( (Vec_Vec_t *)vSupports );
// if ( pvPartSupps == NULL )
Vec_VecFree( (Vec_Vec_t *)vPartSuppsAll );
// else
// *pvPartSupps = vPartSuppsAll;
/*
// converts from intergers to nodes
Vec_PtrForEachEntry( vPartsAll, vPart, iPart )
{
vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) );
Vec_IntForEachEntry( vPart, iOut, i )
Vec_PtrPush( vPartPtr, Aig_ManPo(p, iOut) );
Vec_IntFree( vPart );
Vec_PtrWriteEntry( vPartsAll, iPart, vPartPtr );
}
*/
return vPartsAll;
}
/**Function*************************************************************
Synopsis [Perform the naive partitioning.]
Description []
......@@ -968,16 +1097,21 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
Vec_Ptr_t * vParts;
Aig_Obj_t * pObj;
void ** ppData;
int i, k, m;
int i, k, m, nIdMax;
assert( Vec_PtrSize(vAigs) > 1 );
// compute the total number of IDs
nIdMax = 0;
Vec_PtrForEachEntry( vAigs, pAig, i )
nIdMax += Aig_ManObjNumMax(pAig);
// partition the first AIG in the array
assert( Vec_PtrSize(vAigs) > 1 );
pAig = Vec_PtrEntry( vAigs, 0 );
vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, NULL );
// start the total fraiged AIG
pAigTotal = Aig_ManStartFrom( pAig );
Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) + 10000 );
Aig_ManReprStart( pAigTotal, nIdMax );
vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) );
// set the PI numbers
......
src/aig/aig/aigRepr.c
......@@ -443,6 +443,11 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
}
//printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
// add choice to the choice node
if ( pObj->nRefs > 0 )
{
Aig_ObjClearRepr( p, pObj );
continue;
}
assert( pObj->nRefs == 0 );
p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
p->pEquivs[pRepr->Id] = pObj;
......@@ -450,6 +455,36 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
}
/**Function*************************************************************
Synopsis [Transfers the classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack )
{
Aig_Obj_t * pObj;
int nClasses, k;
nClasses = 0;
if ( pPart->pReprs )
Aig_ManForEachObj( pPart, pObj, k )
{
if ( pPart->pReprs[pObj->Id] == NULL )
continue;
nClasses++;
Aig_ObjSetRepr( pAig,
Aig_ManObj(pAig, pMapBack[pObj->Id]),
Aig_ManObj(pAig, pMapBack[pPart->pReprs[pObj->Id]->Id]) );
}
return nClasses;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/aig/aigScl.c
......@@ -376,10 +376,14 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
printf( "RBeg = %5d. NBeg = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
}
vMap = Aig_ManReduceLachesOnce( p );
//Aig_ManPrintStats( p );
p = Aig_ManRemap( pTemp = p, vMap );
//Aig_ManPrintStats( p );
Aig_ManStop( pTemp );
Vec_PtrFree( vMap );
Aig_ManSeqCleanup( p );
//Aig_ManPrintStats( p );
//printf( "\n" );
if ( fVerbose )
{
printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
......
src/aig/aig/aigTsim.c
......@@ -25,6 +25,7 @@
////////////////////////////////////////////////////////////////////////
#define TSI_MAX_ROUNDS 1000
#define TSI_ONE_SERIES 300
#define AIG_XVS0 1
#define AIG_XVS1 2
......@@ -282,6 +283,51 @@ void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
}
/**Function*************************************************************
Synopsis [Count constant values in the state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_TsiStateCount( Aig_Tsi_t * p, unsigned * pState )
{
Aig_Obj_t * pObjLi, * pObjLo;
int i, Value, nCounter = 0;
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
nCounter += (Value == 1 || Value == 2);
}
return nCounter;
}
/**Function*************************************************************
Synopsis [Count constant values in the state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_TsiStateOrAll( Aig_Tsi_t * pTsi, unsigned * pState )
{
unsigned * pPrev;
int i, k;
Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
{
for ( k = 0; k < pTsi->nWords; k++ )
pState[k] |= pPrev[k];
}
}
/**Function*************************************************************
......@@ -300,8 +346,8 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
Aig_Tsi_t * pTsi;
Vec_Ptr_t * vMap;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
unsigned * pState, * pPrev;
int i, k, f, fConstants, Value, nCounter;
unsigned * pState;//, * pPrev;
int i, f, fConstants, Value, nCounter;
// allocate the simulation manager
pTsi = Aig_TsiStart( p );
// initialize the values
......@@ -323,10 +369,16 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
if ( Value & 2 )
Aig_InfoSetBit( pState, 2 * i + 1 );
}
// printf( "%d ", Aig_TsiStateCount(pTsi, pState) );
// Aig_TsiStatePrint( pTsi, pState );
// check if this state exists
if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
break;
// nCounter = 0;
// Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
// nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
//printf( "%d -> ", nCounter );
// insert this state
Aig_TsiStateInsert( pTsi, pState, pTsi->nWords );
// simulate internal nodes
......@@ -335,9 +387,23 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
// transfer the latch values
Aig_ManForEachLiSeq( p, pObj, i )
Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
nCounter = 0;
Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
{
if ( f < TSI_ONE_SERIES )
Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
else
{
if ( Aig_ObjGetXsim(pObjLi) != Aig_ObjGetXsim(pObjLo) )
Aig_ObjSetXsim( pObjLo, AIG_XVSX );
}
nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
}
// if ( f && (f % 1000 == 0) )
// printf( "%d \n", f );
//printf( "%d ", nCounter );
}
//printf( "\n" );
if ( f == TSI_MAX_ROUNDS )
{
printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS );
......@@ -346,11 +412,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
}
// OR all the states
pState = Vec_PtrEntry( pTsi->vStates, 0 );
Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
{
for ( k = 0; k < pTsi->nWords; k++ )
pState[k] |= pPrev[k];
}
Aig_TsiStateOrAll( pTsi, pState );
// check if there are constants
fConstants = 0;
if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords )
......
src/aig/fra/fra.h
......@@ -50,6 +50,7 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
typedef struct Fra_Par_t_ Fra_Par_t;
typedef struct Fra_Ssw_t_ Fra_Ssw_t;
typedef struct Fra_Man_t_ Fra_Man_t;
typedef struct Fra_Cla_t_ Fra_Cla_t;
typedef struct Fra_Sml_t_ Fra_Sml_t;
......@@ -86,6 +87,25 @@ struct Fra_Par_t_
int fDontShowBar; // does not show progressbar during fraiging
};
// seq SAT sweeping parametesr
struct Fra_Ssw_t_
{
int nPartSize; // size of the partition
int nOverSize; // size of the overlap between partitions
int nFramesP; // number of frames in the prefix
int nFramesK; // number of frames for induction (1=simple)
int nMaxImps; // max implications to consider
int nMaxLevs; // max levels to consider
int fUseImps; // use implications
int fRewrite; // enable rewriting of the specualatively reduced model
int fFraiging; // enable comb SAT sweeping as preprocessing
int fLatchCorr; // perform register correspondence
int fWriteImps; // write implications into a file
int fUse1Hot; // use one-hotness constraints
int fVerbose; // enable verbose output
int nIters; // the number of iterations performed
};
// FRAIG equivalence classes
struct Fra_Cla_t_
{
......@@ -287,7 +307,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 nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter );
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
/*=== fraIndVer.c =====================================================*/
extern int Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
/*=== fraLcr.c ========================================================*/
......
src/aig/fra/fraInd.c
......@@ -234,7 +234,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
/**Function*************************************************************
Synopsis [Performs choicing of the AIG.]
Synopsis [Performs partitioned sequential SAT sweepingG.]
Description []
......@@ -243,7 +243,77 @@ 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 nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter )
Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
{
int fPrintParts = 0;
char Buffer[100];
Aig_Man_t * pTemp, * pNew;
Vec_Ptr_t * vResult;
Vec_Int_t * vPart;
int * pMapBack;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
// generate partitions
vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
if ( fPrintParts )
{
// print partitions
printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Vec_PtrForEachEntry( vResult, vPart, i )
{
sprintf( Buffer, "part%03d.aig", i );
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
Aig_ManStop( pTemp );
}
}
// perform SSW with partitions
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
Vec_PtrForEachEntry( vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
// run SSW
pNew = Fra_FraigInduction( pTemp, pPars );
nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
if ( fVerbose )
printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
Aig_ManStop( pNew );
Aig_ManStop( pTemp );
free( pMapBack );
}
// remap the AIG
pNew = Aig_ManDupRepr( pAig, 0 );
Aig_ManSeqCleanup( pNew );
// Aig_ManPrintStats( pAig );
// Aig_ManPrintStats( pNew );
Vec_VecFree( (Vec_Vec_t *)vResult );
pPars->nPartSize = nPartSize;
pPars->fVerbose = fVerbose;
return pNew;
}
/**Function*************************************************************
Synopsis [Performs sequential SAT sweeping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
{
int fUseSimpleCnf = 0;
int fUseOldSimulation = 0;
......@@ -263,14 +333,23 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
if ( Aig_ManNodeNum(pManAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
pParams->nIters = 0;
return Aig_ManDup(pManAig, 1);
}
assert( Aig_ManLatchNum(pManAig) == 0 );
assert( Aig_ManRegNum(pManAig) > 0 );
assert( nFramesK > 0 );
assert( pParams->nFramesK > 0 );
//Aig_ManShow( pManAig, 0, NULL );
if ( pParams->fWriteImps && pParams->nPartSize > 0 )
{
pParams->nPartSize = 0;
printf( "Partitioning was disabled to allow implication writing.\n" );
}
// perform partitioning
if ( pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig) )
return Fra_FraigInductionPart( pManAig, pParams );
nNodesBeg = Aig_ManNodeNum(pManAig);
nRegsBeg = Aig_ManRegNum(pManAig);
......@@ -279,16 +358,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
// get parameters
Fra_ParamsDefaultSeq( pPars );
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;
pPars->fUse1Hot = fUse1Hot;
pPars->nFramesP = pParams->nFramesP;
pPars->nFramesK = pParams->nFramesK;
pPars->nMaxImps = pParams->nMaxImps;
pPars->nMaxLevs = pParams->nMaxLevs;
pPars->fVerbose = pParams->fVerbose;
pPars->fRewrite = pParams->fRewrite;
pPars->fLatchCorr = pParams->fLatchCorr;
pPars->fUseImps = pParams->fUseImps;
pPars->fWriteImps = pParams->fWriteImps;
pPars->fUse1Hot = pParams->fUse1Hot;
assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
......@@ -311,10 +390,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
// bug: r iscas/blif/s5378.blif ; st; ssw -v
// bug: r iscas/blif/s1238.blif ; st; ssw -v
// refine the classes with more simulation rounds
if ( fVerbose )
if ( pPars->fVerbose )
printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );
if ( fVerbose )
if ( pPars->fVerbose )
{
PRT( "Time", clock() - clk );
}
......@@ -408,7 +487,7 @@ p->timeTrav += clock() - clk2;
Fra_OneHotAssume( p, p->vOneHots );
// report the intermediate results
if ( fVerbose )
if ( pPars->fVerbose )
{
printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. ",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
......@@ -428,7 +507,7 @@ clk2 = clock();
if ( p->pPars->fUse1Hot )
Fra_OneHotCheck( p, p->vOneHots );
Fra_FraigSweep( p );
if ( fVerbose )
if ( pPars->fVerbose )
{
// PRT( "t", clock() - clk2 );
}
......@@ -508,7 +587,7 @@ p->timeTotal = clock() - clk;
// if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
// if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
// printf( "Proved output constant 0.\n" );
if ( pnIter ) *pnIter = nIter;
pParams->nIters = nIter;
return pManAigNew;
}
......
src/aig/fra/fraSec.c
......@@ -40,73 +40,17 @@
SeeAlso []
***********************************************************************/
int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pNew;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
if ( nFramesFix )
{
nFrames = nFramesFix;
// perform seq sweeping for one frame number
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
}
else
{
// perform seq sweeping while increasing the number of frames
for ( nFrames = 1; ; nFrames++ )
{
clk = clock();
pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
if ( RetValue == 1 )
printf( "UNSAT " );
else
printf( "UNDECIDED " );
PRT( "Time", clock() - clk );
}
if ( RetValue != -1 )
break;
Aig_ManStop( pNew );
}
}
// get the miter status
RetValue = Fra_FraigMiterStatus( pNew );
Aig_ManStop( pNew );
// report the miter
if ( RetValue == 1 )
printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
else if ( RetValue == 0 )
printf( "Networks are NOT EQUIVALENT. " );
else
printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
PRT( "Time", clock() - clkTotal );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
Fra_Ssw_t Pars, * pPars = &Pars;
Fra_Sml_t * pSml;
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
// prepare parameters
memset( pPars, 0, sizeof(Fra_Ssw_t) );
pPars->fLatchCorr = fLatchCorr;
pPars->fVerbose = fVeryVerbose;
pNew = Aig_ManDup( p, 1 );
if ( fVerbose )
......@@ -185,13 +129,14 @@ PRT( "Time", clock() - clk );
for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
{
clk = clock();
pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
pPars->nFramesK = nFrames;
pNew = Fra_FraigInduction( pTemp = pNew, pPars );
Aig_ManStop( pTemp );
RetValue = Fra_FraigMiterStatus( pNew );
if ( fVerbose )
{
printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ",
nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
if ( RetValue != -1 )
......
src/base/abc/abc.h
......@@ -567,6 +567,8 @@ extern void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag,
extern void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
extern void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
extern void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
/*=== abcDelay.c ==========================================================*/
extern float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib );
/*=== abcDfs.c ==========================================================*/
extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
......@@ -733,7 +735,7 @@ extern bool Abc_NodeIsBuf( Abc_Obj_t * pNode );
extern bool Abc_NodeIsInv( Abc_Obj_t * pNode );
extern void Abc_NodeComplement( Abc_Obj_t * pNode );
/*=== abcPrint.c ==========================================================*/
extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest );
extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib );
extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
......
src/base/abci/abcDar.c
......@@ -263,6 +263,25 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_NtkAddDummyBoxNames( pNtkNew );
else
{
{
int i, k, iFlop, Counter = 0;
FILE * pFile;
pFile = fopen( "out.txt", "w" );
fprintf( pFile, "The total of %d registers were removed (out of %d):\n",
Abc_NtkLatchNum(pNtkOld)-Vec_IntSize(pMan->vFlopNums), Abc_NtkLatchNum(pNtkOld) );
for ( i = 0; i < Abc_NtkLatchNum(pNtkOld); i++ )
{
Vec_IntForEachEntry( pMan->vFlopNums, iFlop, k )
{
if ( i == iFlop )
break;
}
if ( k == Vec_IntSize(pMan->vFlopNums) )
fprintf( pFile, "%6d (%6d) : %s\n", ++Counter, i, Abc_ObjName( Abc_ObjFanout0(Abc_NtkBox(pNtkOld, i)) ) );
}
fclose( pFile );
//printf( "\n" );
}
assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
......@@ -1034,7 +1053,7 @@ PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose )
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
{
Fraig_Params_t Params;
Abc_Ntk_t * pNtkAig, * pNtkFraig;
......@@ -1046,21 +1065,23 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in
// so fraiging does not reduce the number of functions represented by nodes
Fraig_ParamsSetDefault( &Params );
Params.nBTLimit = 100000;
if ( fFraiging )
if ( pPars->fFraiging && pPars->nPartSize == 0 )
{
pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
else
pNtkFraig = Abc_NtkDup( pNtk );
if ( fVerbose )
if ( pPars->fVerbose )
{
PRT( "Initial fraiging time", clock() - clk );
}
}
else
pNtkFraig = Abc_NtkDup( pNtk );
pMan = Abc_NtkToDar( pNtkFraig, 1 );
Abc_NtkDelete( pNtkFraig );
if ( pMan == NULL )
return NULL;
pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose, NULL );
pMan = Fra_FraigInduction( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
......@@ -1283,7 +1304,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose )
Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan;
......@@ -1291,13 +1312,10 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbos
if ( pMan == NULL )
return NULL;
Aig_ManSeqCleanup( pMan );
if ( fLatchSweep )
{
if ( pMan->nRegs )
pMan = Aig_ManReduceLaches( pMan, fVerbose );
if ( pMan->nRegs )
if ( fLatchConst && pMan->nRegs )
pMan = Aig_ManConstReduce( pMan, fVerbose );
}
if ( fLatchEqual && pMan->nRegs )
pMan = Aig_ManReduceLaches( pMan, fVerbose );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
......@@ -1557,41 +1575,16 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
***********************************************************************/
void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
{
// extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize );
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return;
Aig_ManComputeSccs( pMan );
// Aig_ManRegPartitionLinear( pMan, 1000 );
Aig_ManStop( pMan );
}
/**Function*************************************************************
Synopsis [Performs partitioning.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDarPartition( Abc_Ntk_t * pNtk )
{
extern void Aig_ManRegPartitionRun( Aig_Man_t * pAig );
Aig_Man_t * pMan;
// convert to the AIG manager
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return;
Aig_ManRegPartitionRun( pMan );
Aig_ManStop( pMan );
}
#include "ntl.h"
......
src/base/abci/abcDelay.c
......@@ -74,7 +74,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
pPinPerm[best_i] = temp;
}
// verify
assert( pPinPerm[0] < Abc_ObjFaninNum(pNode) );
assert( Abc_ObjFaninNum(pNode) == 0 || pPinPerm[0] < Abc_ObjFaninNum(pNode) );
for ( i = 1; i < Abc_ObjFaninNum(pNode); i++ )
{
assert( pPinPerm[i] < Abc_ObjFaninNum(pNode) );
......@@ -96,6 +96,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
{
extern void * Abc_FrameReadLibLut();
int fUseSorting = 0;
int pPinPerm[32];
float pPinDelays[32];
If_Lib_t * pLutLib;
......@@ -144,11 +145,20 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
else
{
pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
if ( fUseSorting )
{
Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
Abc_ObjForEachFanin( pNode, pFanin, k )
if ( tArrival < Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] )
tArrival = Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k];
}
else
{
Abc_ObjForEachFanin( pNode, pFanin, k )
if ( tArrival < Abc_ObjArrival(pFanin) + pDelays[k] )
tArrival = Abc_ObjArrival(pFanin) + pDelays[k];
}
}
if ( Abc_ObjFaninNum(pNode) == 0 )
tArrival = 0.0;
Abc_ObjSetArrival( pNode, tArrival );
......@@ -188,6 +198,8 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
else
{
pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
if ( fUseSorting )
{
Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
Abc_ObjForEachFanin( pNode, pFanin, k )
{
......@@ -196,6 +208,16 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
Abc_ObjSetRequired( Abc_ObjFanin(pNode,pPinPerm[k]), tRequired );
}
}
else
{
Abc_ObjForEachFanin( pNode, pFanin, k )
{
tRequired = Abc_ObjRequired(pNode) - pDelays[k];
if ( Abc_ObjRequired(pFanin) > tRequired )
Abc_ObjSetRequired( pFanin, tRequired );
}
}
}
// set slack for this object
tSlack = Abc_ObjRequired(pNode) - Abc_ObjArrival(pNode);
assert( tSlack + 0.001 > 0.0 );
......@@ -265,8 +287,17 @@ unsigned Abc_NtkDelayTraceTCEdges( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, float tD
void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose )
{
Abc_Obj_t * pNode;
If_Lib_t * pLutLib;
int i, Nodes, * pCounters;
float tArrival, tDelta, nSteps, Num;
// get the library
pLutLib = fUseLutLib? Abc_FrameReadLibLut() : NULL;
if ( pLutLib && pLutLib->LutMax < Abc_NtkGetFaninMax(pNtk) )
{
printf( "The max LUT size (%d) is less than the max fanin count (%d).\n",
pLutLib->LutMax, Abc_NtkGetFaninMax(pNtk) );
return;
}
// decide how many steps
nSteps = fUseLutLib ? 20 : Abc_NtkLevel(pNtk);
pCounters = ALLOC( int, nSteps + 1 );
......@@ -277,6 +308,8 @@ void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose )
// count how many nodes have slack in the corresponding intervals
Abc_NtkForEachNode( pNtk, pNode, i )
{
if ( Abc_ObjFaninNum(pNode) == 0 )
continue;
Num = Abc_ObjSlack(pNode) / tDelta;
assert( Num >=0 && Num <= nSteps );
pCounters[(int)Num]++;
......@@ -356,15 +389,20 @@ int Abc_AigCheckTfi( Abc_Obj_t * pNew, Abc_Obj_t * pOld )
SeeAlso []
***********************************************************************/
void Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
int Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
{
if ( Abc_NodeIsTravIdCurrent(pNode) )
return;
return 1;
if ( Abc_ObjIsCi(pNode) )
return 0;
assert( Abc_ObjIsNode(pNode) );
Abc_NodeSetTravIdCurrent( pNode );
Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes );
Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes );
if ( !Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes ) )
return 0;
if ( !Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes ) )
return 0;
Vec_PtrPush( vNodes, pNode );
return 1;
}
/**Function*************************************************************
......@@ -405,7 +443,12 @@ void Abc_NtkSpeedupNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pAig, Abc_Obj_t * pNode,
}
// traverse from the root node
pAnd = pNode->pCopy;
Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes );
if ( !Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes ) )
{
// printf( "Bad node!!!\n" );
Vec_PtrFree( vNodes );
return;
}
// derive cofactors
nCofs = (1 << Vec_PtrSize(vTimes));
......
src/base/abci/abcIf.c
......@@ -252,6 +252,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
// create a new node
pNodeNew = Abc_NtkCreateNode( pNtkNew );
pCutBest = If_ObjCutBest( pIfObj );
if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
If_CutRotatePins( pIfMan, pCutBest );
if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
{
If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
......
src/base/abci/abcPrint.c
......@@ -111,12 +111,20 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest )
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib )
{
int Num;
if ( fSaveBest )
Abc_NtkCompareAndSaveBest( pNtk );
if ( fDumpResult )
{
char Buffer[1000] = {0};
char * pNameGen = pNtk->pSpec? Extra_FileNameGeneric( pNtk->pSpec ) : "nameless_";
sprintf( Buffer, "%s_dump.blif", pNameGen );
Io_Write( pNtk, Buffer, IO_FILE_BLIF );
if ( pNtk->pSpec ) free( pNameGen );
}
// if ( Abc_NtkIsStrash(pNtk) )
// Abc_AigCountNext( pNtk->pManFunc );
......@@ -181,7 +189,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
fprintf( pFile, " lev = %3d", Abc_AigLevel(pNtk) );
else
fprintf( pFile, " lev = %3d", Abc_NtkLevel(pNtk) );
if ( fUseLutLib && Abc_FrameReadLibLut() )
fprintf( pFile, " delay = %5.2f", Abc_NtkDelayTraceLut(pNtk, 1) );
fprintf( pFile, "\n" );
// Abc_NtkCrossCut( pNtk );
......
src/map/if/if.h
......@@ -170,10 +170,10 @@ struct If_Man_t_
// priority cut
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
float Delay; // delay of the cut
unsigned uSign; // cut signature
unsigned Cost : 14; // the user's cost of the cut
unsigned fCompl : 1; // the complemented attribute
......@@ -379,8 +379,10 @@ extern int If_ManPerformMappingSeq( If_Man_t * p );
/*=== ifTime.c ============================================================*/
extern float If_CutDelay( If_Man_t * p, If_Cut_t * pCut );
extern void If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float Required );
extern void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
/*=== ifTruth.c ===========================================================*/
extern 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 If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars );
/*=== ifUtil.c ============================================================*/
extern void If_ManCleanNodeCopy( If_Man_t * p );
extern void If_ManCleanCutData( If_Man_t * p );
......
src/map/if/ifTime.c
......@@ -221,6 +221,30 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
}
}
/**Function*************************************************************
Synopsis [Sorts the pins in the decreasing order of delays.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
{
If_Obj_t * pLeaf;
float PinDelays[32];
// int PinPerm[32];
int i;
assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth );
If_CutForEachLeaf( p, pCut, pLeaf, i )
PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
If_CutTruthPermute( p->puTemp[0], If_CutTruth(pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) );
// If_CutSortInputPins( p, pCut, PinPerm, PinDelays );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/map/if/ifTruth.c
......@@ -126,6 +126,42 @@ void If_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int i
/**Function*************************************************************
Synopsis [Implements given permutation of variables.]
Description [Permutes truth table in-place (returns it in pIn).]
SideEffects []
SeeAlso []
***********************************************************************/
void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars )
{
unsigned * pTemp;
float tTemp;
int i, Temp, Counter = 0, fChange = 1;
while ( fChange )
{
fChange = 0;
for ( i = 0; i < nVars - 1; i++ )
{
if ( pDelays[i] >= pDelays[i+1] )
continue;
tTemp = pDelays[i]; pDelays[i] = pDelays[i+1]; pDelays[i+1] = tTemp;
Temp = pVars[i]; pVars[i] = pVars[i+1]; pVars[i+1] = Temp;
If_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
pTemp = pOut; pOut = pIn; pIn = pTemp;
fChange = 1;
Counter++;
}
}
if ( Counter & 1 )
If_TruthCopy( pOut, pIn, nVars );
}
/**Function*************************************************************
Synopsis [Expands the truth table according to the phase.]
Description [The input and output truth tables are in pIn/pOut. The current number
......
src/opt/fret/fretFlow.c
......@@ -73,6 +73,7 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
#endif
// clear histogram
assert(pManMR->vSinkDistHist);
memset(Vec_IntArray(pManMR->vSinkDistHist), 0, sizeof(int)*Vec_IntSize(pManMR->vSinkDistHist));
// seed queue : latches, PIOs, and blocks
......
src/opt/fret/fretime.h
......@@ -27,7 +27,8 @@
// #define DEBUG_PRINT_FLOWS
// #define DEBUG_VISITED
// #define DEBUG_PREORDER
// #define DEBUG_CHECK
#define DEBUG_CHECK
// #define DEBUG_PRINT_LEVELS
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -36,17 +37,18 @@
#define MAX_DIST 30000
// flags in Flow_Data structure...
#define VISITED_E 0x01
#define VISITED_R 0x02
#define VISITED_E 0x001
#define VISITED_R 0x002
#define VISITED (VISITED_E | VISITED_R)
#define FLOW 0x04
#define CROSS_BOUNDARY 0x08
#define BLOCK 0x10
#define INIT_0 0x20
#define INIT_1 0x40
#define FLOW 0x004
#define CROSS_BOUNDARY 0x008
#define BLOCK 0x010
#define INIT_0 0x020
#define INIT_1 0x040
#define INIT_CARE (INIT_0 | INIT_1)
#define CONSERVATIVE 0x80
#define CONSERVATIVE 0x080
#define BLOCK_OR_CONS (BLOCK | CONSERVATIVE)
#define BIAS_NODE 0x100
typedef struct Flow_Data_t_ {
unsigned int mark : 16;
......@@ -55,6 +57,7 @@ typedef struct Flow_Data_t_ {
Abc_Obj_t *pred;
/* unsigned int var; */
Abc_Obj_t *pInitObj;
Abc_Obj_t *pCopy;
Vec_Ptr_t *vNodes;
};
......@@ -63,26 +66,30 @@ typedef struct Flow_Data_t_ {
} Flow_Data_t;
// useful macros for manipulating Flow_Data structure...
#define FDATA( x ) ((Flow_Data_t *)Abc_ObjCopy(x))
#define FSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark |= y
#define FUNSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark &= ~y
#define FTEST( x, y ) (((Flow_Data_t *)Abc_ObjCopy(x))->mark & y)
#define FDATA( x ) (pManMR->pDataArray+Abc_ObjId(x))
#define FSET( x, y ) FDATA(x)->mark |= y
#define FUNSET( x, y ) FDATA(x)->mark &= ~y
#define FTEST( x, y ) (FDATA(x)->mark & y)
#define FTIMEEDGES( x ) &(pManMR->vTimeEdges[Abc_ObjId( x )])
static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) {
assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage
FDATA(pObj)->pred = pPred;
}
static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) {
return FDATA(pObj)->pred;
}
typedef struct NodeLag_T_ {
int id;
int lag;
} NodeLag_t;
typedef struct InitConstraint_t_ {
Abc_Obj_t *pBiasNode;
Vec_Int_t vNodes;
Vec_Int_t vLags;
} InitConstraint_t;
typedef struct MinRegMan_t_ {
// problem description:
int maxDelay;
bool fComputeInitState, fGuaranteeInitState;
bool fComputeInitState, fGuaranteeInitState, fBlockConst;
int nNodes, nLatches;
bool fForwardOnly, fBackwardOnly;
bool fConservTimingOnly;
......@@ -99,24 +106,38 @@ typedef struct MinRegMan_t_ {
int fSolutionIsDc;
int constraintMask;
int iteration, subIteration;
Vec_Int_t *vLags;
// problem data
Vec_Int_t *vSinkDistHist;
Flow_Data_t *pDataArray;
Vec_Ptr_t *vTimeEdges;
Vec_Ptr_t *vExactNodes;
Vec_Ptr_t *vInitConstraints;
Abc_Ntk_t *pInitNtk;
Vec_Ptr_t *vNodes; // re-useable struct
NodeLag_t *pInitToOrig;
int sizeInitToOrig;
} MinRegMan_t ;
extern MinRegMan_t *pManMR;
#define vprintf if (pManMR->fVerbose) printf
/*=== fretMain.c ==========================================================*/
static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) {
assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage
FDATA(pObj)->pred = pPred;
}
static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) {
return FDATA(pObj)->pred;
}
extern MinRegMan_t *pManMR;
/*=== fretMain.c ==========================================================*/
Abc_Ntk_t * Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
Abc_Ntk_t * Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose,
int fComputeInitState, int fGuaranteeInitState, int fBlockConst,
int fForward, int fBackward, int nMaxIters,
int maxDelay, int fFastButConservative);
......@@ -128,6 +149,15 @@ int Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose );
bool Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pCur, Abc_Obj_t *pNext );
void Abc_FlowRetime_ClearFlows( bool fClearAll );
int Abc_FlowRetime_GetLag( Abc_Obj_t *pObj );
void Abc_FlowRetime_SetLag( Abc_Obj_t *pObj, int lag );
void Abc_FlowRetime_UpdateLags( );
void Abc_ObjPrintNeighborhood( Abc_Obj_t *pObj, int depth );
Abc_Ntk_t * Abc_FlowRetime_NtkSilentRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
/*=== fretFlow.c ==========================================================*/
int dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred );
......@@ -150,6 +180,8 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk );
int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk );
void Abc_FlowRetime_ConstrainInit( );
void Abc_FlowRetime_AddInitBias( );
void Abc_FlowRetime_RemoveInitBias( );
/*=== fretTime.c ==========================================================*/
......
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