Intersection a bug in rewrite/refactor.

This commit is contained in:
Alan Mishchenko 2022-02-22 21:14:48 -08:00
parent 31519bd6d6
commit bcf21e4677
9 changed files with 84 additions and 46 deletions

View File

@ -559,7 +559,7 @@ extern ABC_DLL Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, A
extern ABC_DLL Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern ABC_DLL Abc_Obj_t * Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
extern ABC_DLL Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
extern ABC_DLL void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel );
extern ABC_DLL int Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel );
extern ABC_DLL void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
extern ABC_DLL void Abc_AigRehash( Abc_Aig_t * pMan );
extern ABC_DLL int Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );

View File

@ -847,7 +847,7 @@ Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
SeeAlso []
***********************************************************************/
void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel )
int Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel )
{
assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 );
assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 );
@ -859,6 +859,8 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
{
pOld = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceOld );
pNew = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceNew );
if ( Abc_ObjFanoutNum(pOld) != 0 )
return 0;
Abc_AigReplace_int( pMan, pOld, pNew, fUpdateLevel );
}
if ( fUpdateLevel )
@ -867,6 +869,7 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
if ( pMan->pNtkAig->vLevelsR )
Abc_AigUpdateLevelR_int( pMan );
}
return 1;
}
/**Function*************************************************************

View File

@ -7312,8 +7312,8 @@ usage:
***********************************************************************/
int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pDup;
int c, RetValue;
int fUpdateLevel;
int fPrecompute;
int fUseZeros;
@ -7383,10 +7383,21 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose, fPlaceEnable ) )
pDup = Abc_NtkDup( pNtk );
RetValue = Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose, fPlaceEnable );
if ( RetValue == -1 )
{
Abc_Print( -1, "Rewriting has failed.\n" );
return 1;
Abc_FrameReplaceCurrentNetwork( pAbc, pDup );
printf( "An error occurred during computation. The original network is restored.\n" );
}
else
{
Abc_NtkDelete( pDup );
if ( RetValue == 0 )
{
Abc_Print( 0, "Rewriting has failed.\n" );
return 1;
}
}
return 0;
@ -7415,8 +7426,8 @@ usage:
***********************************************************************/
int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pDup;
int c, RetValue;
int nNodeSizeMax;
int nConeSizeMax;
int fUpdateLevel;
@ -7506,10 +7517,21 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ) )
pDup = Abc_NtkDup( pNtk );
RetValue = Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
if ( RetValue == -1 )
{
Abc_Print( -1, "Refactoring has failed.\n" );
return 1;
Abc_FrameReplaceCurrentNetwork( pAbc, pDup );
printf( "An error occurred during computation. The original network is restored.\n" );
}
else
{
Abc_NtkDelete( pDup );
if ( RetValue == 0 )
{
Abc_Print( 0, "Refactoring has failed.\n" );
return 1;
}
}
return 0;

View File

@ -325,7 +325,7 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
***********************************************************************/
int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
{
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Abc_ManRef_t * pManRef;
Abc_ManCut_t * pManCut;
@ -333,7 +333,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int f
Vec_Ptr_t * vFanins;
Abc_Obj_t * pNode;
abctime clk, clkStart = Abc_Clock();
int i, nNodes;
int i, nNodes, RetValue = 1;
assert( Abc_NtkIsStrash(pNtk) );
// cleanup the AIG
@ -377,7 +377,12 @@ pManRef->timeRes += Abc_Clock() - clk;
continue;
// acceptable replacement found, update the graph
clk = Abc_Clock();
Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
if ( !Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain ) )
{
Dec_GraphFree( pFForm );
RetValue = -1;
break;
}
pManRef->timeNtk += Abc_Clock() - clk;
Dec_GraphFree( pFForm );
}
@ -394,18 +399,21 @@ pManRef->timeTotal = Abc_Clock() - clkStart;
// put the nodes into the DFS order and reassign their IDs
Abc_NtkReassignIds( pNtk );
// Abc_AigCheckFaninOrder( pNtk->pManFunc );
// fix the levels
if ( fUpdateLevel )
Abc_NtkStopReverseLevels( pNtk );
else
Abc_NtkLevel( pNtk );
// check
if ( !Abc_NtkCheck( pNtk ) )
if ( RetValue != -1 )
{
printf( "Abc_NtkRefactor: The network check has failed.\n" );
return 0;
// fix the levels
if ( fUpdateLevel )
Abc_NtkStopReverseLevels( pNtk );
else
Abc_NtkLevel( pNtk );
// check
if ( !Abc_NtkCheck( pNtk ) )
{
printf( "Abc_NtkRefactor: The network check has failed.\n" );
return 0;
}
}
return 1;
return RetValue;
}

View File

@ -105,7 +105,7 @@ static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
***********************************************************************/
int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, int fUpdateLevel, int fUseZeros, int fVerbose )
{
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Abc_ManRst_t * pManRst;
Cut_Man_t * pManCut;

View File

@ -136,7 +136,7 @@ extern abctime s_ResubTime;
***********************************************************************/
int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose )
{
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Abc_ManRes_t * pManRes;
Abc_ManCut_t * pManCut;

View File

@ -60,14 +60,14 @@ extern void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets
***********************************************************************/
int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable )
{
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
extern int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Cut_Man_t * pManCut;
Rwr_Man_t * pManRwr;
Abc_Obj_t * pNode;
// Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
Dec_Graph_t * pGraph;
int i, nNodes, nGain, fCompl;
int i, nNodes, nGain, fCompl, RetValue = 1;
abctime clk, clkStart = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
@ -138,7 +138,11 @@ Rwr_ManAddTimeCuts( pManRwr, Abc_Clock() - clk );
// complement the FF if needed
if ( fCompl ) Dec_GraphComplement( pGraph );
clk = Abc_Clock();
Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
if ( !Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain ) )
{
RetValue = -1;
break;
}
Rwr_ManAddTimeUpdate( pManRwr, Abc_Clock() - clk );
if ( fCompl ) Dec_GraphComplement( pGraph );
@ -175,17 +179,20 @@ Rwr_ManAddTimeTotal( pManRwr, Abc_Clock() - clkStart );
}
// Abc_AigCheckFaninOrder( pNtk->pManFunc );
// fix the levels
if ( fUpdateLevel )
Abc_NtkStopReverseLevels( pNtk );
else
Abc_NtkLevel( pNtk );
// check
if ( !Abc_NtkCheck( pNtk ) )
if ( RetValue >= 0 )
{
printf( "Abc_NtkRewrite: The network check has failed.\n" );
return 0;
if ( fUpdateLevel )
Abc_NtkStopReverseLevels( pNtk );
else
Abc_NtkLevel( pNtk );
// check
if ( !Abc_NtkCheck( pNtk ) )
{
printf( "Abc_NtkRewrite: The network check has failed.\n" );
return 0;
}
}
return 1;
return RetValue;
}

View File

@ -397,10 +397,7 @@ int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Ab
else assert( 0 );
// replace
if ( pFanout == NULL )
{
Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 );
return 1;
}
return Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 );
// find the fanout after redundancy removal
if ( pNode == Abc_ObjFanin0(pFanout) )
pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) );

View File

@ -237,20 +237,21 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
SeeAlso []
***********************************************************************/
void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
{
extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
Abc_Obj_t * pRootNew;
Abc_Ntk_t * pNtk = pRoot->pNtk;
int nNodesNew, nNodesOld;
int nNodesNew, nNodesOld, RetValue;
nNodesOld = Abc_NtkNodeNum(pNtk);
// create the new structure of nodes
pRootNew = Dec_GraphToNetwork( pNtk, pGraph );
// remove the old nodes
Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
RetValue = Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
// compare the gains
nNodesNew = Abc_NtkNodeNum(pNtk);
//assert( nGain <= nNodesOld - nNodesNew );
return RetValue;
}