From d80f43a1851035b48b80dbeb2a898a3eeaea2df1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 24 Feb 2012 13:21:32 -0800 Subject: Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default. --- src/base/abci/abc.c | 144 ++++++++++----------------------- src/base/abci/abcDar.c | 216 +++++++++++++++++++++++++++++++++++++------------ 2 files changed, 206 insertions(+), 154 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fb6b468c..e47917c8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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) ) + // get the new network + if ( fReverse ) { - Abc_Print( -1, "The miter has latches. ORing is not performed.\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 ); } -*/ - // get the new network - if ( !Abc_NtkCombinePos( pNtk, 0 ) ) + else { - Abc_Print( -1, "ORing the POs has failed.\n" ); - return 1; + 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] \n" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index d54092f9..8efa669f 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -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; } -- cgit v1.2.3