mirror of https://github.com/YosysHQ/abc.git
Better logic cone proprocessor for 'satclp' to reduce runtime.
This commit is contained in:
Alan Mishchenko
parent
0b7734ca99
commit
85b1e1cc93
|
|
@ -20,6 +20,7 @@
|
|||
|
||||
#include "gia.h"
|
||||
#include "misc/tim/tim.h"
|
||||
#include "misc/vec/vecWec.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -3236,6 +3237,260 @@ Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p )
|
|||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes supports for each node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose )
|
||||
{
|
||||
abctime clk = Abc_Clock();
|
||||
Gia_Obj_t * pObj; int i, Id;
|
||||
Vec_Wec_t * vSuppsCo = Vec_WecStart( Gia_ManCoNum(p) );
|
||||
Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
|
||||
Gia_ManForEachCiId( p, Id, i )
|
||||
Vec_IntPush( Vec_WecEntry(vSupps, Id), i );
|
||||
Gia_ManForEachAnd( p, pObj, Id )
|
||||
Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)),
|
||||
Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)),
|
||||
Vec_WecEntry(vSupps, Id) );
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
Vec_IntAppend( Vec_WecEntry(vSuppsCo, i), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
|
||||
Vec_WecFree( vSupps );
|
||||
if ( fVerbose )
|
||||
Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
|
||||
return vSuppsCo;
|
||||
}
|
||||
int Gia_ManCoSuppSizeMax( Gia_Man_t * p, Vec_Wec_t * vSupps )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
Vec_Int_t * vSuppOne;
|
||||
int i, nSuppMax = 1;
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
{
|
||||
vSuppOne = Vec_WecEntry( vSupps, i );
|
||||
nSuppMax = Abc_MaxInt( nSuppMax, Vec_IntSize(vSuppOne) );
|
||||
}
|
||||
return nSuppMax;
|
||||
}
|
||||
int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
Vec_Int_t * vSuppOne;
|
||||
int i, iCoMax = -1, nSuppMax = -1;
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
{
|
||||
vSuppOne = Vec_WecEntry( vSupps, i );
|
||||
if ( nSuppMax < Vec_IntSize(vSuppOne) )
|
||||
{
|
||||
nSuppMax = Vec_IntSize(vSuppOne);
|
||||
iCoMax = i;
|
||||
}
|
||||
}
|
||||
return iCoMax;
|
||||
}
|
||||
Vec_Int_t * Gia_ManSortCoBySuppSize( Gia_Man_t * p, Vec_Wec_t * vSupps )
|
||||
{
|
||||
Vec_Int_t * vOrder = Vec_IntAlloc( Gia_ManCoNum(p) );
|
||||
Vec_Wrd_t * vSortData = Vec_WrdAlloc( Gia_ManCoNum(p) );
|
||||
Vec_Int_t * vSuppOne; word Entry; int i;
|
||||
Vec_WecForEachLevel( vSupps, vSuppOne, i )
|
||||
Vec_WrdPush( vSortData, ((word)i << 32) | Vec_IntSize(vSuppOne) );
|
||||
Abc_QuickSort3( Vec_WrdArray(vSortData), Vec_WrdSize(vSortData), 1 );
|
||||
Vec_WrdForEachEntry( vSortData, Entry, i )
|
||||
Vec_IntPush( vOrder, (int)(Entry >> 32) );
|
||||
Vec_WrdFree( vSortData );
|
||||
return vOrder;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Remaps each CO cone to depend on the first CI variables.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManDupHashDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
|
||||
{
|
||||
if ( ~pObj->Value )
|
||||
return pObj->Value;
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
|
||||
Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
|
||||
return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
}
|
||||
void Gia_ManDupCleanDfs_rec( Gia_Obj_t * pObj )
|
||||
{
|
||||
if ( !~pObj->Value )
|
||||
return;
|
||||
pObj->Value = ~0;
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
return;
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
|
||||
Gia_ManDupCleanDfs_rec( Gia_ObjFanin1(pObj) );
|
||||
}
|
||||
Gia_Man_t * Gia_ManDupStrashReduce( Gia_Man_t * p, Vec_Wec_t * vSupps, Vec_Int_t ** pvCoMap )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
Gia_Man_t * pNew, * pTemp;
|
||||
Vec_Int_t * vSuppOne, * vCoMapLit;
|
||||
int i, k, iCi, iLit, nSuppMax;
|
||||
assert( Gia_ManRegNum(p) == 0 );
|
||||
Gia_ManFillValue( p );
|
||||
vCoMapLit = Vec_IntAlloc( Gia_ManCoNum(p) );
|
||||
pNew = Gia_ManStart( Gia_ManObjNum(p) );
|
||||
pNew->pName = Abc_UtilStrsav( p->pName );
|
||||
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
||||
Gia_ManConst0(p)->Value = 0;
|
||||
nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps );
|
||||
for ( i = 0; i < nSuppMax; i++ )
|
||||
Gia_ManAppendCi(pNew);
|
||||
Gia_ManHashAlloc( pNew );
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
{
|
||||
vSuppOne = Vec_WecEntry( vSupps, i );
|
||||
if ( Vec_IntSize(vSuppOne) == 0 )
|
||||
Vec_IntPush( vCoMapLit, Abc_Var2Lit(0, Gia_ObjFaninC0(pObj)) );
|
||||
else if ( Vec_IntSize(vSuppOne) == 1 )
|
||||
Vec_IntPush( vCoMapLit, Abc_Var2Lit(1, Gia_ObjFaninC0(pObj)) );
|
||||
else
|
||||
{
|
||||
Vec_IntForEachEntry( vSuppOne, iCi, k )
|
||||
Gia_ManCi(p, iCi)->Value = Gia_Obj2Lit(pNew, Gia_ManCi(pNew, k) );
|
||||
Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
|
||||
assert( Gia_ObjFanin0Copy(pObj) < 2 * Gia_ManObjNum(pNew) );
|
||||
Vec_IntPush( vCoMapLit, Gia_ObjFanin0Copy(pObj) );
|
||||
Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
|
||||
}
|
||||
}
|
||||
Gia_ManHashStop( pNew );
|
||||
assert( Vec_IntSize(vCoMapLit) == Gia_ManCoNum(p) );
|
||||
if ( pvCoMap == NULL ) // do not remap
|
||||
{
|
||||
Vec_IntForEachEntry( vCoMapLit, iLit, i )
|
||||
Gia_ManAppendCo( pNew, iLit );
|
||||
}
|
||||
else // remap
|
||||
{
|
||||
Vec_Int_t * vCoMapRes = Vec_IntAlloc( Gia_ManCoNum(p) ); // map old CO into new CO
|
||||
Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(pNew) ); // map new lit into new CO
|
||||
Vec_IntForEachEntry( vCoMapLit, iLit, i )
|
||||
{
|
||||
if ( Vec_IntEntry(vMap, iLit) == -1 )
|
||||
{
|
||||
Vec_IntWriteEntry( vMap, iLit, Gia_ManCoNum(pNew) );
|
||||
Gia_ManAppendCo( pNew, iLit );
|
||||
}
|
||||
Vec_IntPush( vCoMapRes, Vec_IntEntry(vMap, iLit) );
|
||||
}
|
||||
Vec_IntFree( vMap );
|
||||
*pvCoMap = vCoMapRes;
|
||||
}
|
||||
Vec_IntFree( vCoMapLit );
|
||||
pNew = Gia_ManCleanup( pTemp = pNew );
|
||||
Gia_ManStop( pTemp );
|
||||
return pNew;
|
||||
}
|
||||
Gia_Man_t * Gia_ManIsoStrashReduce2( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
|
||||
{
|
||||
Vec_Int_t * vCoMap;
|
||||
Vec_Wec_t * vSupps = Gia_ManCreateCoSupps( p, fVerbose );
|
||||
Gia_Man_t * pNew = Gia_ManDupStrashReduce( p, vSupps, &vCoMap );
|
||||
Vec_IntFree( vCoMap );
|
||||
Vec_WecFree( vSupps );
|
||||
*pvPosEquivs = NULL;
|
||||
return pNew;
|
||||
}
|
||||
|
||||
int Gia_ManIsoStrashReduceOne( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp )
|
||||
{
|
||||
int k, iCi, iLit;
|
||||
assert( Gia_ObjIsCo(pObj) );
|
||||
if ( Vec_IntSize(vSupp) == 0 )
|
||||
return Abc_Var2Lit(0, Gia_ObjFaninC0(pObj));
|
||||
if ( Vec_IntSize(vSupp) == 1 )
|
||||
return Abc_Var2Lit(1, Gia_ObjFaninC0(pObj));
|
||||
Vec_IntForEachEntry( vSupp, iCi, k )
|
||||
Gia_ManCi(p, iCi)->Value = Gia_Obj2Lit(pNew, Gia_ManCi(pNew, k) );
|
||||
Gia_ManDupHashDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
|
||||
iLit = Gia_ObjFanin0Copy(pObj);
|
||||
Gia_ManDupCleanDfs_rec( Gia_ObjFanin0(pObj) );
|
||||
return iLit;
|
||||
}
|
||||
Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose )
|
||||
{
|
||||
Gia_Man_t * pNew;
|
||||
Gia_Obj_t * pObj;
|
||||
Vec_Wec_t * vPosEquivs = Vec_WecAlloc( 100 );
|
||||
Vec_Int_t * vSuppOne, * vMap = Vec_IntAlloc( 10000 );
|
||||
int i, iLit, nSuppMax = Gia_ManCoSuppSizeMax( p, vSupps );
|
||||
// count how many times each support size appears
|
||||
Vec_Int_t * vSizeCount = Vec_IntStart( nSuppMax + 1 );
|
||||
Vec_WecForEachLevel( vSupps, vSuppOne, i )
|
||||
Vec_IntAddToEntry( vSizeCount, Vec_IntSize(vSuppOne), 1 );
|
||||
// create array of unique outputs
|
||||
Gia_ManFillValue( p );
|
||||
pNew = Gia_ManStart( Gia_ManObjNum(p) );
|
||||
Gia_ManConst0(p)->Value = 0;
|
||||
for ( i = 0; i < nSuppMax; i++ )
|
||||
Gia_ManAppendCi(pNew);
|
||||
Gia_ManHashAlloc( pNew );
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
{
|
||||
vSuppOne = Vec_WecEntry( vSupps, i );
|
||||
if ( Vec_IntEntry(vSizeCount, Vec_IntSize(vSuppOne)) == 1 )
|
||||
{
|
||||
Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
|
||||
continue;
|
||||
}
|
||||
iLit = Gia_ManIsoStrashReduceOne( pNew, p, pObj, vSuppOne );
|
||||
Vec_IntFillExtra( vMap, iLit + 1, -1 );
|
||||
if ( Vec_IntEntry(vMap, iLit) == -1 )
|
||||
{
|
||||
Vec_IntWriteEntry( vMap, iLit, Vec_WecSize(vPosEquivs) );
|
||||
Vec_IntPush( Vec_WecPushLevel(vPosEquivs), i );
|
||||
continue;
|
||||
}
|
||||
Vec_IntPush( Vec_WecEntry(vPosEquivs, Vec_IntEntry(vMap, iLit)), i );
|
||||
}
|
||||
Gia_ManHashStop( pNew );
|
||||
Gia_ManStop( pNew );
|
||||
Vec_IntFree( vSizeCount );
|
||||
Vec_IntFree( vMap );
|
||||
return vPosEquivs;
|
||||
}
|
||||
Gia_Man_t * Gia_ManIsoStrashReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose )
|
||||
{
|
||||
Vec_Wec_t * vSupps = Gia_ManCreateCoSupps( p, fVerbose );
|
||||
Vec_Wec_t * vPosEquivs = Gia_ManIsoStrashReduceInt( p, vSupps, fVerbose );
|
||||
// find the first outputs and derive GIA
|
||||
Vec_Int_t * vFirsts = Vec_WecCollectFirsts( vPosEquivs );
|
||||
Gia_Man_t * pNew = Gia_ManDupCones( p, Vec_IntArray(vFirsts), Vec_IntSize(vFirsts), 0 );
|
||||
Vec_IntFree( vFirsts );
|
||||
Vec_WecFree( vSupps );
|
||||
// report and return
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "Nontrivial classes:\n" );
|
||||
Vec_WecPrint( vPosEquivs, 1 );
|
||||
}
|
||||
if ( pvPosEquivs )
|
||||
*pvPosEquivs = Vec_WecConvertToVecPtr( vPosEquivs );
|
||||
Vec_WecFree( vPosEquivs );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -242,6 +242,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
|
|||
#endif
|
||||
|
||||
|
||||
#if 0
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
|
|
@ -526,6 +527,233 @@ Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
|
|||
return pNtkNew;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
||||
|
||||
extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose );
|
||||
extern int Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps );
|
||||
extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose );
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives GIA for the network.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_NtkClpGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
|
||||
{
|
||||
int iLit0, iLit1;
|
||||
if ( pNode->iTemp >= 0 )
|
||||
return pNode->iTemp;
|
||||
assert( Abc_ObjIsNode( pNode ) );
|
||||
iLit0 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) );
|
||||
iLit1 = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin1(pNode) );
|
||||
iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) );
|
||||
iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) );
|
||||
return (pNode->iTemp = Gia_ManAppendAnd(pNew, iLit0, iLit1));
|
||||
}
|
||||
Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk )
|
||||
{
|
||||
int i, iLit;
|
||||
Gia_Man_t * pNew;
|
||||
Abc_Obj_t * pNode;
|
||||
assert( Abc_NtkIsStrash(pNtk) );
|
||||
pNew = Gia_ManStart( 1000 );
|
||||
pNew->pName = Abc_UtilStrsav( pNtk->pName );
|
||||
pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec );
|
||||
Abc_NtkForEachObj( pNtk, pNode, i )
|
||||
pNode->iTemp = -1;
|
||||
Abc_AigConst1(pNtk)->iTemp = 1;
|
||||
Abc_NtkForEachCi( pNtk, pNode, i )
|
||||
pNode->iTemp = Gia_ManAppendCi(pNew);
|
||||
Abc_NtkForEachCo( pNtk, pNode, i )
|
||||
{
|
||||
iLit = Abc_NtkClpGia_rec( pNew, Abc_ObjFanin0(pNode) );
|
||||
iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) );
|
||||
Gia_ManAppendCo( pNew, iLit );
|
||||
}
|
||||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes SOPs for each output.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp )
|
||||
{
|
||||
Vec_Str_t * vSop;
|
||||
abctime clk = Abc_Clock();
|
||||
extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
|
||||
Gia_Man_t * pGia = Gia_ManDupCones( p, &iCo, 1, 1 );
|
||||
if ( fVerbose )
|
||||
printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) );
|
||||
vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
|
||||
Gia_ManStop( pGia );
|
||||
if ( vSop == NULL )
|
||||
return NULL;
|
||||
if ( Vec_StrSize(vSop) == 4 ) // constant
|
||||
Vec_IntClear(vSupp);
|
||||
if ( fVerbose )
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
return vSop;
|
||||
}
|
||||
Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
|
||||
{
|
||||
ProgressBar * pProgress;
|
||||
Vec_Ptr_t * vSops = NULL, * vSopsRepr;
|
||||
Vec_Int_t * vReprs, * vClass, * vReprSuppSizes;
|
||||
int i, k, Entry, iCo, * pOrder;
|
||||
Vec_Wec_t * vClasses;
|
||||
// check the largest output
|
||||
if ( nCubeLim > 0 && nCostMax > 0 )
|
||||
{
|
||||
int iCoMax = Gia_ManCoLargestSupp( p, vSupps );
|
||||
int iObjMax = Gia_ObjId( p, Gia_ManCo(p, iCoMax) );
|
||||
int nSuppMax = Vec_IntSize( Vec_WecEntry(vSupps, iCoMax) );
|
||||
int nNodeMax = Gia_ManConeSize( p, &iObjMax, 1 );
|
||||
word Cost = (word)nNodeMax * (word)nSuppMax * (word)nCubeLim;
|
||||
if ( Cost > (word)nCostMax )
|
||||
{
|
||||
printf( "Cost of the largest output cone exceeded the limit (%d * %d * %d > %d).\n",
|
||||
nNodeMax, nSuppMax, nCubeLim, nCostMax );
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
// derive classes of outputs
|
||||
vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
|
||||
// derive representatives
|
||||
vReprs = Vec_WecCollectFirsts( vClasses );
|
||||
vReprSuppSizes = Vec_IntAlloc( Vec_IntSize(vReprs) );
|
||||
Vec_IntForEachEntry( vReprs, Entry, i )
|
||||
Vec_IntPush( vReprSuppSizes, Vec_IntSize(Vec_WecEntry(vSupps, Entry)) );
|
||||
pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) );
|
||||
Vec_IntFree( vReprSuppSizes );
|
||||
// consider SOPs for representatives
|
||||
vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) );
|
||||
pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) );
|
||||
Extra_ProgressBarUpdate( pProgress, 0, NULL );
|
||||
for ( i = 0; i < Vec_IntSize(vReprs); i++ )
|
||||
{
|
||||
int iEntry = pOrder[Vec_IntSize(vReprs) - 1 - i];
|
||||
int iCoThis = Vec_IntEntry( vReprs, iEntry );
|
||||
Vec_Int_t * vSupp = Vec_WecEntry( vSupps, iCoThis );
|
||||
Vec_Str_t * vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp );
|
||||
if ( vSop == NULL )
|
||||
goto finish;
|
||||
assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );
|
||||
Extra_ProgressBarUpdate( pProgress, i, NULL );
|
||||
Vec_PtrWriteEntry( vSopsRepr, iEntry, Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) ) );
|
||||
Vec_StrFree( vSop );
|
||||
}
|
||||
Extra_ProgressBarStop( pProgress );
|
||||
// derive SOPs for each output
|
||||
vSops = Vec_PtrStart( Gia_ManCoNum(p) );
|
||||
Vec_WecForEachLevel ( vClasses, vClass, i )
|
||||
Vec_IntForEachEntry( vClass, iCo, k )
|
||||
Vec_PtrWriteEntry( vSops, iCo, Vec_PtrEntry(vSopsRepr, i) );
|
||||
assert( Vec_PtrCountZero(vSops) == 0 );
|
||||
/*
|
||||
// verify
|
||||
for ( i = 0; i < Gia_ManCoNum(p); i++ )
|
||||
{
|
||||
Vec_Int_t * vSupp = Vec_WecEntry( vSupps, i );
|
||||
char * pSop = (char *)Vec_PtrEntry( vSops, i );
|
||||
assert( Vec_IntSize(vSupp) == Abc_SopGetVarNum(pSop) );
|
||||
}
|
||||
*/
|
||||
// cleanup
|
||||
finish:
|
||||
ABC_FREE( pOrder );
|
||||
Vec_IntFree( vReprs );
|
||||
Vec_WecFree( vClasses );
|
||||
Vec_PtrFree( vSopsRepr );
|
||||
return vSops;
|
||||
}
|
||||
Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
|
||||
{
|
||||
Abc_Ntk_t * pNtkNew;
|
||||
Gia_Man_t * pGia;
|
||||
Vec_Wec_t * vSupps;
|
||||
Vec_Int_t * vSupp;
|
||||
Vec_Ptr_t * vSops;
|
||||
Abc_Obj_t * pNode, * pNodeNew, * pDriver;
|
||||
int i, k, iCi;
|
||||
pGia = Abc_NtkClpGia( pNtk );
|
||||
vSupps = Gia_ManCreateCoSupps( pGia, fVerbose );
|
||||
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
|
||||
vSops = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
|
||||
Gia_ManStop( pGia );
|
||||
if ( vSops == NULL )
|
||||
{
|
||||
Vec_WecFree( vSupps );
|
||||
Abc_NtkDelete( pNtkNew );
|
||||
return NULL;
|
||||
}
|
||||
Abc_NtkForEachCo( pNtk, pNode, i )
|
||||
{
|
||||
pDriver = Abc_ObjFanin0(pNode);
|
||||
if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) )
|
||||
{
|
||||
Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy );
|
||||
continue;
|
||||
}
|
||||
if ( Abc_ObjIsCi(pDriver) )
|
||||
{
|
||||
pNodeNew = Abc_NtkCreateNode( pNtkNew );
|
||||
Abc_ObjAddFanin( pNodeNew, pDriver->pCopy );
|
||||
pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" );
|
||||
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
|
||||
continue;
|
||||
}
|
||||
if ( pDriver == Abc_AigConst1(pNtk) )
|
||||
{
|
||||
pNodeNew = Abc_NtkCreateNode( pNtkNew );
|
||||
pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? " 0\n" : " 1\n" );
|
||||
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
|
||||
continue;
|
||||
}
|
||||
pNodeNew = Abc_NtkCreateNode( pNtkNew );
|
||||
vSupp = Vec_WecEntry( vSupps, i );
|
||||
Vec_IntForEachEntry( vSupp, iCi, k )
|
||||
Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) );
|
||||
pNodeNew->pData = Vec_PtrEntry( vSops, i );
|
||||
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
|
||||
}
|
||||
Vec_WecFree( vSupps );
|
||||
Vec_PtrFree( vSops );
|
||||
return pNtkNew;
|
||||
}
|
||||
Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
|
||||
{
|
||||
Abc_Ntk_t * pNtkNew;
|
||||
assert( Abc_NtkIsStrash(pNtk) );
|
||||
pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
|
||||
if ( pNtkNew == NULL )
|
||||
return NULL;
|
||||
if ( pNtk->pExdc )
|
||||
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
|
||||
if ( !Abc_NtkCheck( pNtkNew ) )
|
||||
{
|
||||
printf( "Abc_NtkCollapseSat: The network check has failed.\n" );
|
||||
Abc_NtkDelete( pNtkNew );
|
||||
return NULL;
|
||||
}
|
||||
return pNtkNew;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
|
|
|
|||
Loading…
Reference in New Issue