| /**CFile**************************************************************** |
| |
| FileName [saigTempor.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Sequential AIG package.] |
| |
| Synopsis [Temporal decomposition.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: saigTempor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "saig.h" |
| #include "sat/bmc/bmc.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates initialized timeframes for temporal decomposition.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames ) |
| { |
| Aig_Man_t * pFrames; |
| Aig_Obj_t * pObj, * pObjLi, * pObjLo; |
| int i, f; |
| // start the frames package |
| Aig_ManCleanData( pAig ); |
| pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); |
| pFrames->pName = Abc_UtilStrsav( pAig->pName ); |
| // initiliaze the flops |
| Saig_ManForEachLo( pAig, pObj, i ) |
| pObj->pData = Aig_ManConst0(pFrames); |
| // for each timeframe |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames); |
| Saig_ManForEachPi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi(pFrames); |
| Aig_ManForEachNode( pAig, pObj, i ) |
| pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| Aig_ManForEachCo( pAig, pObj, i ) |
| pObj->pData = Aig_ObjChild0Copy(pObj); |
| Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) |
| pObjLo->pData = pObjLi->pData; |
| } |
| // create POs for the flop inputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObj->pData ); |
| Aig_ManCleanup( pFrames ); |
| return pFrames; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames ) |
| { |
| Aig_Man_t * pAigNew, * pFrames; |
| Aig_Obj_t * pObj, * pReset; |
| int i; |
| if ( pAig->nConstrs > 0 ) |
| { |
| printf( "The AIG manager should have no constraints.\n" ); |
| return NULL; |
| } |
| // create initialized timeframes |
| pFrames = Saig_ManTemporFrames( pAig, nFrames ); |
| assert( Aig_ManCoNum(pFrames) == Aig_ManRegNum(pAig) ); |
| |
| // start the new manager |
| Aig_ManCleanData( pAig ); |
| pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); |
| pAigNew->pName = Abc_UtilStrsav( pAig->pName ); |
| // map the constant node and primary inputs |
| Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); |
| Saig_ManForEachPi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pAigNew ); |
| |
| // insert initialization logic |
| Aig_ManConst1(pFrames)->pData = Aig_ManConst1( pAigNew ); |
| Aig_ManForEachCi( pFrames, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pAigNew ); |
| Aig_ManForEachNode( pFrames, pObj, i ) |
| pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| Aig_ManForEachCo( pFrames, pObj, i ) |
| pObj->pData = Aig_ObjChild0Copy(pObj); |
| |
| // create reset latch (the first one among the latches) |
| pReset = Aig_ObjCreateCi( pAigNew ); |
| |
| // create flop output values |
| Saig_ManForEachLo( pAig, pObj, i ) |
| pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreateCi(pAigNew), (Aig_Obj_t *)Aig_ManCo(pFrames, i)->pData ); |
| Aig_ManStop( pFrames ); |
| |
| // add internal nodes of this frame |
| Aig_ManForEachNode( pAig, pObj, i ) |
| pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| // create primary outputs |
| Saig_ManForEachPo( pAig, pObj, i ) |
| Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) ); |
| |
| // create reset latch (the first one among the latches) |
| Aig_ObjCreateCo( pAigNew, Aig_ManConst1(pAigNew) ); |
| // create latch inputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) ); |
| |
| // finalize |
| Aig_ManCleanup( pAigNew ); |
| Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); // + reset latch (011111...) |
| return pAigNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find index of first non-zero entry.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Vec_IntLastNonZeroBeforeLimit( Vec_Int_t * vTemp, int Limit ) |
| { |
| int Entry, i; |
| if ( vTemp == NULL ) |
| return -1; |
| Vec_IntForEachEntryReverse( vTemp, Entry, i ) |
| { |
| if ( i >= Limit ) |
| continue; |
| if ( Entry ) |
| return i; |
| } |
| return -1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose ) |
| { |
| extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans ); |
| |
| Vec_Int_t * vTransSigs = NULL; |
| int RetValue, nFramesFinished = -1; |
| assert( nFrames >= 0 ); |
| if ( nFrames == 0 ) |
| { |
| nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose, &vTransSigs ); |
| if ( nFrames == 0 ) |
| { |
| Vec_IntFreeP( &vTransSigs ); |
| printf( "The leading sequence has length 0. Temporal decomposition is not performed.\n" ); |
| return NULL; |
| } |
| if ( nFrames == 1 ) |
| { |
| Vec_IntFreeP( &vTransSigs ); |
| printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" ); |
| return NULL; |
| } |
| if ( fUseTransSigs ) |
| { |
| int Entry, i, iLast = -1; |
| Vec_IntForEachEntry( vTransSigs, Entry, i ) |
| iLast = Entry ? i :iLast; |
| if ( iLast > 0 && iLast < nFrames ) |
| { |
| Abc_Print( 1, "Reducing frame count from %d to %d to fit the last transient.\n", nFrames, iLast ); |
| nFrames = iLast; |
| } |
| } |
| Abc_Print( 1, "Using computed frame number (%d).\n", nFrames ); |
| } |
| else |
| Abc_Print( 1, "Using user-given frame number (%d).\n", nFrames ); |
| // run BMC2 |
| if ( fUseBmc ) |
| { |
| RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0, 0 ); |
| if ( RetValue == 0 ) |
| { |
| Vec_IntFreeP( &vTransSigs ); |
| printf( "A cex found in the first %d frames.\n", nFrames ); |
| return NULL; |
| } |
| if ( nFramesFinished + 1 < nFrames ) |
| { |
| int iLastBefore = Vec_IntLastNonZeroBeforeLimit( vTransSigs, nFramesFinished ); |
| if ( iLastBefore < 1 || !fUseTransSigs ) |
| { |
| Vec_IntFreeP( &vTransSigs ); |
| printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames ); |
| return NULL; |
| } |
| assert( iLastBefore < nFramesFinished ); |
| printf( "BMC succeeded to frame %d. Adjusting frame count to be (%d) based on the last transient signal.\n", nFramesFinished, iLastBefore ); |
| nFrames = iLastBefore; |
| } |
| } |
| Vec_IntFreeP( &vTransSigs ); |
| return Saig_ManTemporDecompose( pAig, nFrames ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| ABC_NAMESPACE_IMPL_END |
| |
