Adding resource limit switch -C to 'sop'.

This commit is contained in:
Alan Mishchenko 2015-02-11 12:33:54 -08:00
parent 72dbdee202
commit 8cabdcb55d
23 changed files with 79 additions and 62 deletions

View File

@ -654,14 +654,14 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkFraigRestore();
extern ABC_DLL void Abc_NtkFraigStoreClean();
/*=== abcFunc.c ==========================================================*/
extern ABC_DLL int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
extern ABC_DLL int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit );
extern ABC_DLL void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
extern ABC_DLL void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
extern ABC_DLL Gia_Man_t * Abc_NtkAigToGia( Abc_Ntk_t * p );
extern ABC_DLL int Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
extern ABC_DLL int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit );
extern ABC_DLL int Abc_NtkToBdd( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkToAig( Abc_Ntk_t * pNtk );
/*=== abcHaig.c ==========================================================*/

View File

@ -356,7 +356,7 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn,
SeeAlso []
***********************************************************************/
int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit )
{
extern void Abc_NtkSortSops( Abc_Ntk_t * pNtk );
Abc_Obj_t * pNode;
@ -366,18 +366,21 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
Vec_Str_t * vCube;
int i, fMode, nCubes;
// collect all BDDs into one array
Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
assert( !Cudd_ReorderingStatus(dd, &nCubes) );
Abc_NtkForEachNode( pNtk, pNode, i )
if ( !Abc_ObjIsBarBuf(pNode) )
Vec_PtrPush( vFuncs, pNode->pData );
// estimate the number of cubes in the ISOPs
nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fDirect, ABC_MAX_CUBES );
Vec_PtrFree( vFuncs );
if ( nCubes == -1 )
return 0;
//printf( "The total number of cubes = %d.\n", nCubes );
if ( nCubeLimit < ABC_INFINITY )
{
// collect all BDDs into one array
Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
assert( !Cudd_ReorderingStatus(dd, &nCubes) );
Abc_NtkForEachNode( pNtk, pNode, i )
if ( !Abc_ObjIsBarBuf(pNode) )
Vec_PtrPush( vFuncs, pNode->pData );
// estimate the number of cubes in the ISOPs
nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fDirect, nCubeLimit );
Vec_PtrFree( vFuncs );
if ( nCubes == -1 )
return 0;
//printf( "The total number of cubes = %d.\n", nCubes );
}
if ( fDirect )
fMode = 1;
@ -407,6 +410,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
Vec_StrFree( vCube );
return 0;
}
assert( Abc_ObjFaninNum(pNode) == Abc_SopGetVarNum((char *)pNode->pNext) );
}
Vec_StrFree( vCube );
@ -1134,7 +1138,7 @@ int Abc_NtkSopToBlifMv( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect )
int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit )
{
assert( !Abc_NtkIsStrash(pNtk) );
if ( Abc_NtkHasSop(pNtk) )
@ -1143,17 +1147,17 @@ int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect )
return 1;
if ( !Abc_NtkSopToBdd(pNtk) )
return 0;
return Abc_NtkBddToSop(pNtk, fDirect);
return Abc_NtkBddToSop(pNtk, fDirect, nCubeLimit);
}
if ( Abc_NtkHasMapping(pNtk) )
return Abc_NtkMapToSop(pNtk);
if ( Abc_NtkHasBdd(pNtk) )
return Abc_NtkBddToSop(pNtk, fDirect);
return Abc_NtkBddToSop(pNtk, fDirect, nCubeLimit);
if ( Abc_NtkHasAig(pNtk) )
{
if ( !Abc_NtkAigToBdd(pNtk) )
return 0;
return Abc_NtkBddToSop(pNtk, fDirect);
return Abc_NtkBddToSop(pNtk, fDirect, nCubeLimit);
}
assert( 0 );
return 0;
@ -1214,7 +1218,7 @@ int Abc_NtkToAig( Abc_Ntk_t * pNtk )
}
if ( Abc_NtkHasBdd(pNtk) )
{
if ( !Abc_NtkBddToSop(pNtk,0) )
if ( !Abc_NtkBddToSop(pNtk,0, ABC_INFINITY) )
return 0;
return Abc_NtkSopToAig(pNtk);
}

View File

@ -446,7 +446,7 @@ Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
iState |= (1 << i);
}
// transfer logic to SOPs
Abc_NtkToSop( pNtk, 0 );
Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
// create new network
pNtkNew = Abc_NtkStartFromNoLatches( pNtk, pNtk->ntkType, pNtk->ntkFunc );
nStates = (1 << nFlops);

View File

@ -740,7 +740,7 @@ int Abc_NtkEliminateSpecial( Abc_Ntk_t * pNtk, int nMaxSize, int fVerbose )
Abc_NtkCleanup( pNtk, 0 );
// convert network to SOPs
if ( !Abc_NtkToSop(pNtk, 0) )
if ( !Abc_NtkToSop(pNtk, 0, ABC_INFINITY) )
{
fprintf( stdout, "Converting to SOP has failed.\n" );
return 0;

View File

@ -209,7 +209,7 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse )
// convert to logic SOP
pNtk = Abc_NtkDup( pNtk0 );
if ( Abc_NtkIsLogic(pNtk) && !Abc_NtkHasMapping(pNtk) )
Abc_NtkToSop( pNtk, 0 );
Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
// collect all nodes in the network
vNodes = Vec_PtrAlloc( 100 );

View File

@ -7889,16 +7889,27 @@ usage:
int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int fDirect;
int fDirect, nCubeLimit = 1000000;
int c;
// set defaults
fDirect = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Cdh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nCubeLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nCubeLimit < 0 )
goto usage;
break;
case 'd':
fDirect ^= 1;
break;
@ -7918,7 +7929,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Converting to SOP is possible only for logic networks.\n" );
return 1;
}
if ( !Abc_NtkToSop(pNtk, fDirect) )
if ( !Abc_NtkToSop(pNtk, fDirect, nCubeLimit) )
{
Abc_Print( -1, "Converting to SOP has failed.\n" );
return 1;
@ -7926,8 +7937,9 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: sop [-dh]\n" );
Abc_Print( -2, "usage: sop [-C num] [-dh]\n" );
Abc_Print( -2, "\t converts node functions to SOP\n" );
Abc_Print( -2, "\t-C num : the limit on the total cube count of all nodes [default = %d]\n", nCubeLimit );
Abc_Print( -2, "\t-d : toggles using both phases or only positive [default = %s]\n", fDirect? "direct": "both" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@ -17226,7 +17238,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the network in the SOP form
if ( !Abc_NtkToSop(pNtk, 0) )
if ( !Abc_NtkToSop(pNtk, 0, ABC_INFINITY) )
{
Abc_Print( -1, "Converting to SOPs has failed.\n" );
return 0;

View File

@ -199,7 +199,7 @@ Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1
Abc_NtkSweep( pNtk, 0 );
Abc_NtkCleanupSeq( pNtk, 0, 0, 0 );
Abc_NtkToSop( pNtk, 0 );
Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
Abc_NtkCycleInitStateSop( pNtk, 50, 0 );
return pNtk;
}

View File

@ -58,7 +58,7 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
Abc_NtkMapToSop(pNtk);
else if ( Abc_NtkHasBdd(pNtk) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
{
printf( "Abc_NtkEspresso(): Converting to SOPs has failed.\n" );
return;

View File

@ -91,7 +91,7 @@ int Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
// Abc_NtkBddToSop(pNtk);
}
// get the network in the SOP form
if ( !Abc_NtkToSop(pNtk, 0) )
if ( !Abc_NtkToSop(pNtk, 0, ABC_INFINITY) )
{
printf( "Abc_NtkFastExtract(): Converting to SOPs has failed.\n" );
return 0;

View File

@ -88,7 +88,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
assert( !Abc_NtkIsNetlist(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
{
printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" );
return NULL;
@ -634,7 +634,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
assert( !Abc_NtkIsNetlist(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
{
Vec_IntFree( vInit );
printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );

View File

@ -561,7 +561,7 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
// duplicate the network
pNtkNew2 = Abc_NtkDup( pNtk );
pNtkNew = Abc_NtkMulti( pNtkNew2, 0, 20, 0, 0, 1, 0 );
if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
if ( !Abc_NtkBddToSop( pNtkNew, 0, ABC_INFINITY ) )
{
printf( "Abc_NtkFromMapSuperChoice(): Converting to SOPs has failed.\n" );
return NULL;

View File

@ -389,7 +389,7 @@ void Abc_NktMffcPrint( char * pFileName, Abc_Obj_t ** pNodes, int nNodes, Vec_Pt
Abc_Obj_t * pObj, * pFanin;
int i, k;
// convert the network
Abc_NtkToSop( pNodes[0]->pNtk, 0 );
Abc_NtkToSop( pNodes[0]->pNtk, 0, ABC_INFINITY );
// write the file
pFile = fopen( pFileName, "wb" );
fprintf( pFile, ".model %s_part\n", pNodes[0]->pNtk->pName );
@ -430,7 +430,7 @@ void Abc_NktMffcPrintInt( char * pFileName, Abc_Ntk_t * pNtk, Vec_Int_t * vRoots
Abc_Obj_t * pObj, * pFanin;
int i, k;
// convert the network
Abc_NtkToSop( pNtk, 0 );
Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
// write the file
pFile = fopen( pFileName, "wb" );
fprintf( pFile, ".model %s_part\n", pNtk->pName );

View File

@ -55,11 +55,7 @@ Vec_Ptr_t * Abc_NtkAssignIDs( Abc_Ntk_t * pNtk )
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->iTemp = i;
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
{
pObj->iTemp = Abc_NtkCiNum(pNtk) + i;
//printf( "%d->%d ", pObj->Id, pObj->iTemp );
}
//printf( "\n" );
Abc_NtkForEachCo( pNtk, pObj, i )
pObj->iTemp = Abc_NtkCiNum(pNtk) + Vec_PtrSize(vNodes) + i;
return vNodes;
@ -265,7 +261,11 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
return 0;
}
if ( !Abc_NtkHasSop(pNtk) )
Abc_NtkToSop( pNtk, 0 );
if ( !Abc_NtkToSop( pNtk, 0, ABC_INFINITY ) )
{
printf( "Conversion to SOP has failed due to low resource limit.\n" );
return 0;
}
// collect information
p = Abc_NtkExtractMfs( pNtk, pPars->nFirstFixed );
// perform optimization
@ -442,7 +442,7 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t
return 0;
}
if ( !Abc_NtkHasSop(p) )
Abc_NtkToSop( p, 0 );
Abc_NtkToSop( p, 0, ABC_INFINITY );
// derive unfolded network
pNtk = Abc_NtkUnrollAndDrop( p, nFrames, nFramesAdd, vFlops, &iPivot );
Io_WriteBlifLogic( pNtk, "unroll_dump.blif", 0 );
@ -466,7 +466,7 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t
// perform final sweep
Abc_NtkSweep( p, 0 );
if ( !Abc_NtkHasSop(p) )
Abc_NtkToSop( p, 0 );
Abc_NtkToSop( p, 0, ABC_INFINITY );
return 1;
}

View File

@ -1119,7 +1119,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
// transform logic functions from BDD to SOP
if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
{
printf( "Abc_NtkPrintGates(): Converting to SOPs has failed.\n" );
return;

View File

@ -337,7 +337,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// transform the network to the SOP representation
if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
if ( !Abc_NtkBddToSop( pNtkNew, 0, ABC_INFINITY ) )
{
printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" );
return NULL;

View File

@ -1907,7 +1907,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
// write out the current network
if ( Abc_NtkIsLogic(pNtk) )
Abc_NtkToSop(pNtk, 0);
Abc_NtkToSop(pNtk, 0, ABC_INFINITY);
pNetlist = Abc_NtkToNetlist(pNtk);
if ( pNetlist == NULL )
{
@ -2049,7 +2049,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
// write out the current network
if ( Abc_NtkIsLogic(pNtk) )
Abc_NtkToSop(pNtk, 0);
Abc_NtkToSop(pNtk, 0, ABC_INFINITY);
pNetlist = Abc_NtkToNetlist(pNtk);
if ( pNetlist == NULL )
{
@ -2263,7 +2263,7 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
// write out the current network
if ( Abc_NtkIsLogic(pNtk) )
Abc_NtkToSop(pNtk, 0);
Abc_NtkToSop(pNtk, 0, ABC_INFINITY);
pNetlist = Abc_NtkToNetlist(pNtk);
if ( pNetlist == NULL )
{

View File

@ -286,7 +286,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
Abc_NtkDelete( pNtk );
return NULL;
}
if ( !Abc_NtkToSop(pNtk, 0) )
if ( !Abc_NtkToSop(pNtk, 0, ABC_INFINITY) )
{
printf( "Io_ReadBenchNetwork(): Converting to SOP has failed.\n" );
Abc_NtkDelete( pNtk );

View File

@ -367,7 +367,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
return;
}
if ( !Abc_NtkHasSop(pNtk) )
Abc_NtkToSop( pNtk, 0 );
Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
Io_WriteBblif( pNtk, pFileName );
return;
}
@ -396,7 +396,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
pNtkTemp = Abc_NtkToNetlist( pNtk );
Abc_NtkDelete( pNtkCopy );
}
if ( !Abc_NtkToSop( pNtkTemp, 1 ) )
if ( !Abc_NtkToSop( pNtkTemp, 1, ABC_INFINITY ) )
return;
}
else if ( FileType == IO_FILE_MOPLA )
@ -433,7 +433,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
if ( FileType == IO_FILE_BLIF )
{
if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
Abc_NtkToSop( pNtkTemp, 0 );
Abc_NtkToSop( pNtkTemp, 0, ABC_INFINITY );
Io_WriteBlif( pNtkTemp, pFileName, 1, 0, 0 );
}
else if ( FileType == IO_FILE_BLIFMV )
@ -568,12 +568,12 @@ void Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName )
{
Vec_PtrForEachEntry( Abc_Ntk_t *, pNtkResult->pDesign->vModules, pNtkTemp, i )
if ( !Abc_NtkHasSop(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
Abc_NtkToSop( pNtkTemp, 0 );
Abc_NtkToSop( pNtkTemp, 0, ABC_INFINITY );
}
else
{
if ( !Abc_NtkHasSop(pNtkResult) && !Abc_NtkHasMapping(pNtkResult) )
Abc_NtkToSop( pNtkResult, 0 );
Abc_NtkToSop( pNtkResult, 0, ABC_INFINITY );
}
Io_WriteBlif( pNtkResult, pFileName, 1, 0, 0 );
}

View File

@ -1388,7 +1388,7 @@ void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName, char * pLutStruct,
{
Abc_Ntk_t * pNtkTemp;
assert( Abc_NtkIsLogic(pNtk) );
Abc_NtkToSop( pNtk, 0 );
Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
// derive the netlist
pNtkTemp = Abc_NtkToNetlist(pNtk);
if ( pNtkTemp == NULL )

View File

@ -100,7 +100,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// transform logic functions from BDD to SOP
if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
{
printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
return;
@ -463,7 +463,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
// transform logic functions from BDD to SOP
if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
if ( !Abc_NtkBddToSop(pNtk, 0, ABC_INFINITY) )
{
printf( "Io_WriteDotNtk(): Converting to SOPs has failed.\n" );
return;

View File

@ -1486,19 +1486,20 @@ int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fDire
st__table *table = st__init_table( st__ptrcmp, st__ptrhash );
if ( table == NULL )
return -1;
dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit;
for ( i = 0; i < nFuncs; i++ )
{
int Count0 = 0, Count1 = 0;
dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit;
if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, nLimit - CounterAll ) )
break;
if ( fDirect )
Count1 = Count0;
else
{
dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit;
pFuncs[i] = Cudd_Not( pFuncs[i] );
if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit - CounterAll ) )
break;
if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, Count0 ) )
Count1 = Count0;
pFuncs[i] = Cudd_Not( pFuncs[i] );
}
CounterAll += Abc_MinInt( Count0, Count1 );

View File

@ -214,7 +214,7 @@ typedef ABC_INT64_T iword;
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define ABC_INFINITY (100000000)
#define ABC_INFINITY (1000000000)
#define ABC_SWAP(Type, a, b) { Type t = a; a = b; b = t; }

View File

@ -120,7 +120,7 @@ int Abc_NtkRetimeDebug( Abc_Ntk_t * pNtk )
extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
Abc_Ntk_t * pNtkRet;
assert( Abc_NtkIsLogic(pNtk) );
Abc_NtkToSop( pNtk, 0 );
Abc_NtkToSop( pNtk, 0, ABC_INFINITY );
// if ( !Abc_NtkCheck( pNtk ) )
// fprintf( stdout, "Abc_NtkRetimeDebug(): Network check has failed.\n" );
// Io_WriteBlifLogic( pNtk, "debug_temp.blif", 1 );