Skip to content

A
abc
Commit 5ad773ed by Alan Mishchenko
Options

Changing semantics of switch -C in 'sop' to limit cubes at one node.

parent 874d3940
Showing with 49 additions and 47 deletions
src/base/abc/abcFunc.c
......@@ -356,39 +356,39 @@ char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn,
SeeAlso []
***********************************************************************/
int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit )
int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fMode, int nCubeLimit )
{
extern void Abc_NtkSortSops( Abc_Ntk_t * pNtk );
Vec_Int_t * vGuide;
Vec_Str_t * vCube;
Abc_Obj_t * pNode;
Mem_Flex_t * pManNew;
DdManager * dd = (DdManager *)pNtk->pManFunc;
DdNode * bFunc;
Vec_Str_t * vCube;
int i, fMode, nCubes;
int i, nCubes;
// compute SOP size
vGuide = Vec_IntAlloc( Abc_NtkObjNumMax(pNtk) );
Vec_IntFill( vGuide, Abc_NtkObjNumMax(pNtk), fMode );
if ( nCubeLimit < ABC_INFINITY )
{
// collect all BDDs into one array
Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
Vec_Ptr_t * vFuncs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
assert( !Cudd_ReorderingStatus(dd, (Cudd_ReorderingType *)&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_PtrWriteEntry( vFuncs, i, pNode->pData );
// compute the number of cubes in the ISOPs and detemine polarity
nCubes = Extra_bddCountCubes( dd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs), fMode, nCubeLimit, Vec_IntArray(vGuide) );
Vec_PtrFree( vFuncs );
if ( nCubes == -1 )
{
Vec_IntFree( vGuide );
return 0;
}
//printf( "The total number of cubes = %d.\n", nCubes );
}
if ( fDirect == 2 ) // negative polarity only
fMode = 0;
else if ( fDirect == 1 ) // positive polarity only
fMode = 1;
else // both polarities
fMode = -1;
assert( Abc_NtkHasBdd(pNtk) );
if ( dd->size > 0 )
Cudd_zddVarsFromBddVars( dd, 2 );
......@@ -403,17 +403,19 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect, int nCubeLimit )
continue;
assert( pNode->pData );
bFunc = (DdNode *)pNode->pData;
pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode );
pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, Vec_IntEntry(vGuide, i) );
if ( pNode->pNext == NULL )
{
Mem_FlexStop( pManNew, 0 );
Abc_NtkCleanNext( pNtk );
// printf( "Converting from BDDs to SOPs has failed.\n" );
Vec_IntFree( vGuide );
Vec_StrFree( vCube );
return 0;
}
assert( Abc_ObjFaninNum(pNode) == Abc_SopGetVarNum((char *)pNode->pNext) );
}
Vec_IntFree( vGuide );
Vec_StrFree( vCube );
// update the network type
......
src/base/abci/abc.c
......@@ -7889,8 +7889,7 @@ usage:
int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int fDirect = 0, nCubeLimit = 1000000;
int c;
int c, fMode = -1, nCubeLimit = 1000000;
// set defaults
Extra_UtilGetoptReset();
......@@ -7910,10 +7909,10 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
break;
case 'd':
fDirect = 1;
fMode = 1;
break;
case 'n':
fDirect = 2;
fMode = 0;
break;
case 'h':
goto usage;
......@@ -7931,7 +7930,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, nCubeLimit) )
if ( !Abc_NtkToSop(pNtk, fMode, nCubeLimit) )
{
Abc_Print( -1, "Converting to SOP has failed.\n" );
return 1;
......@@ -7939,10 +7938,11 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: sop [-C num] [-dh]\n" );
Abc_Print( -2, "usage: sop [-C num] [-dnh]\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? (fDirect == 1? "direct":"negated"): "both" );
Abc_Print( -2, "\t-C num : the limit on the number of cubes at a node [default = %d]\n", nCubeLimit );
Abc_Print( -2, "\t-d : toggles using only positive polarity [default = %s]\n", fMode == 1 ? "yes": "no" );
Abc_Print( -2, "\t-n : toggles using only negative polarity [default = %s]\n", fMode == 0 ? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
src/misc/extra/extraBdd.h
......@@ -195,7 +195,7 @@ extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdN
extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
extern int Extra_bddVarIsInCube( DdNode * bCube, int iVar );
extern DdNode * Extra_bddAndPermute( DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute );
extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fDirect, int nLimit );
extern int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide );
#ifndef ABC_PRB
#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
......
src/misc/extra/extraBddMisc.c
......@@ -1479,33 +1479,33 @@ static DdNode * extraBddCountCubes( DdManager * dd, DdNode * L, DdNode * U, st__
Cudd_Deref(r);
return r;
}
int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fDirect, int nLimit )
int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fMode, int nLimit, int * pGuide )
{
int i, CounterAll = 0;
unsigned int saveLimit = dd->maxLive;
DdNode * pF0, * pF1;
int i, Count, Count0, Count1, CounterAll = 0;
st__table *table = st__init_table( st__ptrcmp, st__ptrhash );
if ( table == NULL )
return -1;
unsigned int saveLimit = dd->maxLive;
dd->maxLive = dd->keys - dd->dead + 1000000; // limit on intermediate BDD nodes
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, Count0 ) )
Count1 = Count0;
pFuncs[i] = Cudd_Not( pFuncs[i] );
}
CounterAll += Abc_MinInt( Count0, Count1 );
if ( CounterAll > nLimit )
if ( !pFuncs[i] )
continue;
pF1 = pF0 = NULL;
Count0 = Count1 = nLimit;
if ( fMode == -1 || fMode == 1 ) // both or pos
pF1 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit );
pFuncs[i] = Cudd_Not( pFuncs[i] );
if ( fMode == -1 || fMode == 0 ) // both or neg
pF0 = extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, Count1 );
pFuncs[i] = Cudd_Not( pFuncs[i] );
if ( !pF1 && !pF0 )
break;
//printf( "Output %d has %d cubes\n", i, Abc_MinInt(Count0, Count1) );
if ( !pF0 ) pGuide[i] = 1, Count = Count1; // use pos
else if ( !pF1 ) pGuide[i] = 0, Count = Count0; // use neg
else if ( Count1 <= Count0 ) pGuide[i] = 1, Count = Count1; // use pos
else pGuide[i] = 0, Count = Count0; // use neg
CounterAll += Count;
//printf( "Output %5d has %5d cubes (%d) (%5d and %5d)\n", nOuts++, Count, pGuide[i], Count1, Count0 );
}
dd->maxLive = saveLimit;
st__free_table( table );
......
src/misc/extra/extraUtilMisc.c
......@@ -2547,7 +2547,7 @@ void Extra_NtkPrintBin( word * pT, int nBits )
{
int i;
for ( i = nBits - 1; i >= 0; i-- )
printf( "%d", (*pT >> (word)i) & 1 );
printf( "%d", (int)((*pT >> i) & 1) );
}
void Extra_NtkPowerTest()
{
......
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