luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default.

This commit is contained in:
Alan Mishchenko 2012-02-24 13:21:32 -08:00
parent 8f4457772a
commit d80f43a185
2 changed files with 207 additions and 155 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

146
src/base/abci/abc.c
View File

@ -5681,16 +5681,20 @@ usage:
int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);//, * pNtkRes;
int fReverse = 0;
int fComb = 0;
int c;
extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
{
switch ( c )
{
case 'r':
fReverse ^= 1;
break;
case 'c':
fComb ^= 1;
break;
@ -5704,43 +5708,52 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
Abc_Print( -1, "The network is not strashed.\n" );
return 1;
}
/*
if ( Abc_NtkPoNum(pNtk) == 1 )
{
Abc_Print( -1, "The network already has one PO.\n" );
return 1;
}
*/
/*
if ( Abc_NtkLatchNum(pNtk) )
{
Abc_Print( -1, "The miter has latches. ORing is not performed.\n" );
return 1;
}
*/
// get the new network
if ( !Abc_NtkCombinePos( pNtk, 0 ) )
if ( fReverse )
{
Abc_Print( -1, "ORing the POs has failed.\n" );
return 1;
extern Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
Aig_Man_t * pMan = Abc_NtkToDarBmc( pNtk, NULL );
Abc_Ntk_t * pNtkRes = Abc_NtkFromAigPhase( pMan );
Aig_ManStop( pMan );
// perform expansion
if ( Abc_NtkPoNum(pNtk) != Abc_NtkPoNum(pNtkRes) )
printf( "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Abc_NtkPoNum(pNtkRes) );
else
printf( "The output(s) cannot be structurally decomposed.\n" );
// clear counter-example
if ( pAbc->pCex )
ABC_FREE( pAbc->pCex );
// replace the current network
ABC_FREE( pNtkRes->pName );
pNtkRes->pName = Extra_UtilStrsav(pNtk->pName);
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
else
{
if ( !Abc_NtkCombinePos( pNtk, 0 ) )
{
Abc_Print( -1, "ORing the POs has failed.\n" );
return 1;
}
// update counter-example
if ( pAbc->pCex )
pAbc->pCex->iPo = 0;
// replace the current network
// Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
// Bug fix: there is now only one PO. make sure the counterexample points to the right one
if ( pAbc->pCex )
pAbc->pCex->iPo = 0;
// replace the current network
// Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: orpos [-h]\n" );
Abc_Print( -2, "usage: orpos [-rh]\n" );
Abc_Print( -2, "\t creates single-output miter by ORing the POs of the current network\n" );
// Abc_Print( -2, "\t-c : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
Abc_Print( -2, "\t-r : performs the reverse transform (OR decomposition) [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@ -8810,58 +8823,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
*/
/*
{
// extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig );
// extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
// extern Llb4_Nonlin4SweepExperiment( Aig_Man_t * pAig );
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
// Aig_ManTerSimulate( pAig );
// Llb_Nonlin4Cluster( pAig );
// Llb4_Nonlin4SweepExperiment( pAig );
Aig_ManStop( pAig );
}
*/
/*
{
extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
// Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
// Ssm_ManExperiment( "m\\big3.ssim", "m\\big3_.ssim" );
// Ssm_ManExperiment( "m\\tb.ssim", "m\\tb_.ssim" );
Ssm_ManExperiment( "m\\simp.ssim", "m\\simp_.ssim" );
}
*/
/*
{
Gia_Man_t * pGia = Abc_ManReadAig( "bug\\61\\tmp.out", "aig:" );
Gia_ManStop( pGia );
}
*/
/*
{
extern void Abc_BddTest( Aig_Man_t * pAig, int fNew );
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
Abc_BddTest( pAig, fVeryVerbose );
Aig_ManStop( pAig );
}
*/
/*
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
if ( pAbc->pCex && pNtk )
{
Abc_Cex_t * pNew;
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
pNew = Saig_ManCbaFindCexCareBits( pAig, pAbc->pCex, 0, fVerbose );
Aig_ManStop( pAig );
Abc_FrameReplaceCex( pAbc, &pNew );
}
}
*/
{
// extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose );
extern void Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose );
@ -8872,45 +8833,22 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
extern Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap );
if ( pNtk )
{
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Aig_Man_t * pRes;
// Abc_Ntk_t * pNtkRes;
// Aig_ManInterRepar( pAig, 1 );
// Aig_ManInterTest( pAig, 1 );
// Aig_ManSupportsTest( pAig );
// Aig_SupportSizeTest( pAig );
if ( fNewAlgo )
Saig_IsoDetectFast( pAig );
else
{
pRes = Iso_ManTest( pAig, fVerbose );
Aig_Man_t * pRes = Iso_ManTest( pAig, fVerbose );
Aig_ManStopP( &pRes );
}
/*
pRes = Iso_ManTest( pAig, fVerbose );
if ( pRes != NULL )
{
pNtkRes = Abc_NtkFromAigPhase( pRes );
Aig_ManStop( pRes );
ABC_FREE( pNtkRes->pName );
pNtkRes->pName = Extra_UtilStrsav(pNtk->pName);
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
*/
Aig_ManStop( pAig );
}
}
{
// void Bdc_SpfdDecomposeTest();
// Bdc_SpfdDecomposeTest();
}
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDN] [-aovwh] <file_name>\n" );

216
src/base/abci/abcDar.c
View File

@ -45,6 +45,144 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ObjCompareById( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
{
return Abc_ObjId(Abc_ObjRegular(*pp1)) - Abc_ObjId(Abc_ObjRegular(*pp2));
}
/**Function*************************************************************
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_CollectTopOr_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
{
if ( Abc_ObjIsComplement(pObj) || !Abc_ObjIsNode(pObj) )
{
Vec_PtrPush( vSuper, pObj );
return;
}
// go through the branches
Abc_CollectTopOr_rec( Abc_ObjChild0(pObj), vSuper );
Abc_CollectTopOr_rec( Abc_ObjChild1(pObj), vSuper );
}
void Abc_CollectTopOr( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
{
Vec_PtrClear( vSuper );
if ( Abc_ObjIsComplement(pObj) )
{
Abc_CollectTopOr_rec( Abc_ObjNot(pObj), vSuper );
Vec_PtrUniqify( vSuper, (int (*)())Abc_ObjCompareById );
}
else
Vec_PtrPush( vSuper, Abc_ObjNot(pObj) );
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
Description [The returned map maps new PO IDs into old ones.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
{
Aig_Man_t * pMan;
Abc_Obj_t * pObj, * pTemp;
Vec_Ptr_t * vDrivers;
Vec_Ptr_t * vSuper;
int i, k, nDontCares;
// print warning about initial values
nDontCares = 0;
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( Abc_LatchIsInitDc(pObj) )
{
Abc_LatchSetInit0(pObj);
nDontCares++;
}
if ( nDontCares )
{
printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
printf( "The don't-care are assumed to be 0. The result may not verify.\n" );
printf( "Use command \"print_latch\" to see the init values of registers.\n" );
printf( "Use command \"zero\" to convert or \"init\" to change the values.\n" );
}
// collect the drivers
vSuper = Vec_PtrAlloc( 100 );
vDrivers = Vec_PtrAlloc( 100 );
if ( pvMap )
*pvMap = Vec_IntAlloc( 100 );
Abc_NtkForEachPo( pNtk, pObj, i )
{
Abc_CollectTopOr( Abc_ObjChild0(pObj), vSuper );
Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pTemp, k )
{
Vec_PtrPush( vDrivers, pTemp );
if ( pvMap )
Vec_IntPush( *pvMap, i );
}
}
Vec_PtrFree( vSuper );
// create network
pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
pMan->nConstrs = pNtk->nConstrs;
pMan->pName = Extra_UtilStrsav( pNtk->pName );
// transfer the pointers to the basic nodes
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
// create flops
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNotCond( Abc_ObjFanout0(pObj)->pCopy, Abc_LatchIsInit1(pObj) );
// copy internal nodes
Abc_NtkForEachNode( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
// create the POs
Vec_PtrForEachEntry( Abc_Obj_t *, vDrivers, pTemp, k )
Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjRegular(pTemp)->pCopy, !Abc_ObjIsComplement(pTemp)) );
Vec_PtrFree( vDrivers );
// create flops
Abc_NtkForEachLatchInput( pNtk, pObj, i )
Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjChild0Copy(pObj), Abc_LatchIsInit1(Abc_ObjFanout0(pObj))) );
// remove dangling nodes
Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
Aig_ManCleanup( pMan );
if ( !Aig_ManCheck( pMan ) )
{
printf( "Abc_NtkToDarBmc: AIG check has failed.\n" );
Aig_ManStop( pMan );
return NULL;
}
return pMan;
}
/**Function*************************************************************
Synopsis [Converts the network from the AIG manager into ABC.]
@ -1693,19 +1831,23 @@ static void sigfunc( int signo )
int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose, int * piFrames )
{
Aig_Man_t * pMan;
Vec_Int_t * vMap = NULL;
int status, RetValue = -1, clk = clock();
int nTimeLimit = nTimeOut ? time(NULL) + nTimeOut : 0;
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
pMan = Abc_NtkToDarBmc( pNtk, &vMap );
if ( pMan == NULL )
{
printf( "Converting miter into AIG has failed.\n" );
return RetValue;
}
assert( pMan->nRegs > 0 );
assert( Vec_IntSize(vMap) == Aig_ManPoNum(pMan) );
if ( fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) )
printf( "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
// perform verification
if ( fNewAlgo )
if ( fNewAlgo ) // command 'bmc'
{
int iFrame;
RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
@ -1715,64 +1857,24 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 )
{
// printf( "No output asserted in %d frames. ", iFrame );
printf( "Incorrect return value. " );
}
else if ( RetValue == -1 )
{
printf( "No output asserted in %d frames. Resource limit reached ", iFrame );
if ( time(NULL) > nTimeLimit )
printf( "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(iFrame,0) );
if ( nTimeLimit && time(NULL) > nTimeLimit )
printf( "(timeout %d sec). ", nTimeLimit );
else
printf( "(conf limit %d). ", nBTLimit );
}
else // if ( RetValue == 0 )
{
// extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex );
Abc_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
// Aig_ManCounterExampleValueTest( pMan, pCex );
}
ABC_PRT( "Time", clock() - clk );
}
else
{
/*
Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
Abc_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
RetValue = 0;
}
else
{
printf( "No output asserted in %d frames. ", nFrames );
RetValue = 1;
}
*/
/*
int iFrame;
RetValue = Ssw_BmcDynamic( pMan, nFrames, nBTLimit, fVerbose, &iFrame );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( RetValue == 1 )
printf( "No output asserted in %d frames. ", iFrame );
else if ( RetValue == -1 )
printf( "No output asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
else // if ( RetValue == 0 )
{
Abc_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
}
*/
RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
@ -1786,6 +1888,10 @@ ABC_PRT( "Time", clock() - clk );
printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
}
Aig_ManStop( pMan );
// update the counter-example
if ( pNtk->pSeqModel && vMap )
pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
Vec_IntFree( vMap );
return RetValue;
}
@ -1803,15 +1909,22 @@ ABC_PRT( "Time", clock() - clk );
int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
{
Aig_Man_t * pMan;
Vec_Int_t * vMap = NULL;
int status, RetValue = -1, clk = clock();
int nTimeOut = pPars->nTimeOut ? time(NULL) + pPars->nTimeOut : 0;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pPars->fSolveAll )
pMan = Abc_NtkToDar( pNtk, 0, 1 );
else
pMan = Abc_NtkToDarBmc( pNtk, &vMap );
if ( pMan == NULL )
{
printf( "Converting miter into AIG has failed.\n" );
return RetValue;
}
assert( pMan->nRegs > 0 );
if ( pPars->fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) )
printf( "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
RetValue = Saig_ManBmcScalable( pMan, pPars );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
@ -1824,8 +1937,8 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
{
if ( pPars->nFailOuts == 0 )
{
printf( "No output asserted in %d frames. Resource limit reached ", pPars->iFrame );
if ( time(NULL) > nTimeOut )
printf( "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
if ( nTimeOut && time(NULL) > nTimeOut )
printf( "(timeout %d sec). ", pPars->nTimeOut );
else
printf( "(conf limit %d). ", pPars->nConfLimit );
@ -1837,9 +1950,6 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
printf( "(timeout %d sec). ", pPars->nTimeOut );
else
printf( "(conf limit %d). ", pPars->nConfLimit );
// if ( pNtk->vSeqModelVec )
// Vec_PtrFreeFree( pNtk->vSeqModelVec );
// pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
}
else // if ( RetValue == 0 )
@ -1872,6 +1982,10 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
printf( "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
}
Aig_ManStop( pMan );
// update the counter-example
if ( pNtk->pSeqModel && vMap )
pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
Vec_IntFree( vMap );
return RetValue;
}