| /**CFile**************************************************************** |
| |
| FileName [saigTrans.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Sequential AIG package.] |
| |
| Synopsis [Dynamic simplication of the transition relation.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: saigTrans.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "saig.h" |
| #include "proof/fra/fra.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| /* |
| A similar approach is presented in the his paper: |
| A. Kuehlmann. Dynamic transition relation simplification for |
| bounded property checking. ICCAD'04, pp. 50-57. |
| */ |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Maps a node/frame into a node of a different manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Saig_ManStartMap1( Aig_Man_t * p, int nFrames ) |
| { |
| Vec_Int_t * vMap; |
| int i; |
| assert( p->pData == NULL ); |
| vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames ); |
| for ( i = 0; i < vMap->nCap; i++ ) |
| vMap->pArray[i] = -1; |
| vMap->nSize = vMap->nCap; |
| p->pData = vMap; |
| } |
| static inline void Saig_ManStopMap1( Aig_Man_t * p ) |
| { |
| assert( p->pData != NULL ); |
| Vec_IntFree( (Vec_Int_t *)p->pData ); |
| p->pData = NULL; |
| } |
| static inline int Saig_ManHasMap1( Aig_Man_t * p ) |
| { |
| return (int)(p->pData != NULL); |
| } |
| static inline void Saig_ManSetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew ) |
| { |
| Vec_Int_t * vMap = (Vec_Int_t *)p->pData; |
| int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id; |
| assert( !Aig_IsComplement(pOld) ); |
| assert( !Aig_IsComplement(pNew) ); |
| Vec_IntWriteEntry( vMap, nOffset, pNew->Id ); |
| } |
| static inline int Saig_ManGetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1 ) |
| { |
| Vec_Int_t * vMap = (Vec_Int_t *)p->pData; |
| int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id; |
| return Vec_IntEntry( vMap, nOffset ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Maps a node/frame into a node/frame of a different manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline void Saig_ManStartMap2( Aig_Man_t * p, int nFrames ) |
| { |
| Vec_Int_t * vMap; |
| int i; |
| assert( p->pData2 == NULL ); |
| vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames * 2 ); |
| for ( i = 0; i < vMap->nCap; i++ ) |
| vMap->pArray[i] = -1; |
| vMap->nSize = vMap->nCap; |
| p->pData2 = vMap; |
| } |
| static inline void Saig_ManStopMap2( Aig_Man_t * p ) |
| { |
| assert( p->pData2 != NULL ); |
| Vec_IntFree( (Vec_Int_t *)p->pData2 ); |
| p->pData2 = NULL; |
| } |
| static inline int Saig_ManHasMap2( Aig_Man_t * p ) |
| { |
| return (int)(p->pData2 != NULL); |
| } |
| static inline void Saig_ManSetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew, int f2 ) |
| { |
| Vec_Int_t * vMap = (Vec_Int_t *)p->pData2; |
| int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id; |
| assert( !Aig_IsComplement(pOld) ); |
| assert( !Aig_IsComplement(pNew) ); |
| Vec_IntWriteEntry( vMap, 2*nOffset + 0, pNew->Id ); |
| Vec_IntWriteEntry( vMap, 2*nOffset + 1, f2 ); |
| } |
| static inline int Saig_ManGetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, int * pf2 ) |
| { |
| Vec_Int_t * vMap = (Vec_Int_t *)p->pData2; |
| int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id; |
| *pf2 = Vec_IntEntry( vMap, 2*nOffset + 1 ); |
| return Vec_IntEntry( vMap, 2*nOffset ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Create mapping for the first nFrames timeframes of pAig.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManCreateMapping( Aig_Man_t * pAig, Aig_Man_t * pFrames, int nFrames ) |
| { |
| Aig_Obj_t * pObj, * pObjFrame, * pObjRepr; |
| int i, f, iNum, iFrame; |
| assert( pFrames->pReprs != NULL ); // mapping from nodes into their representatives |
| // start step mapping for both orignal manager and fraig |
| Saig_ManStartMap2( pAig, nFrames ); |
| Saig_ManStartMap2( pFrames, 1 ); |
| // for each object in each frame |
| for ( f = 0; f < nFrames; f++ ) |
| Aig_ManForEachObj( pAig, pObj, i ) |
| { |
| // get the frame object |
| iNum = Saig_ManGetMap1( pAig, pObj, f ); |
| pObjFrame = Aig_ManObj( pFrames, iNum ); |
| // if the node has no prototype, map it into itself |
| if ( pObjFrame == NULL ) |
| { |
| Saig_ManSetMap2( pAig, pObj, f, pObj, f ); |
| continue; |
| } |
| // get the representative object |
| pObjRepr = Aig_ObjRepr( pFrames, pObjFrame ); |
| if ( pObjRepr == NULL ) |
| pObjRepr = pObjFrame; |
| // check if this is the first time this object is reached |
| if ( Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame ) == -1 ) |
| Saig_ManSetMap2( pFrames, pObjRepr, 0, pObj, f ); |
| // set the map for the main object |
| iNum = Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame ); |
| Saig_ManSetMap2( pAig, pObj, f, Aig_ManObj(pAig, iNum), iFrame ); |
| } |
| Saig_ManStopMap2( pFrames ); |
| assert( Saig_ManHasMap2(pAig) ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Unroll without initialization.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManFramesNonInitial( Aig_Man_t * pAig, int nFrames ) |
| { |
| Aig_Man_t * pFrames; |
| Aig_Obj_t * pObj, * pObjLi, * pObjLo; |
| int i, f; |
| assert( Saig_ManRegNum(pAig) > 0 ); |
| // start node map |
| Saig_ManStartMap1( pAig, nFrames ); |
| // start the new manager |
| pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); |
| // map the constant node |
| Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); |
| // create variables for register outputs |
| Saig_ManForEachLo( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pFrames ); |
| // add timeframes |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| // create PI nodes for this frame |
| Saig_ManForEachPi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCi( pFrames ); |
| // add internal nodes of this frame |
| Aig_ManForEachNode( pAig, pObj, i ) |
| pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| // create POs for this frame |
| Saig_ManForEachPo( pAig, pObj, i ) |
| pObj->pData = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) ); |
| // save register inputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| pObj->pData = Aig_ObjChild0Copy(pObj); |
| // save the mapping |
| Aig_ManForEachObj( pAig, pObj, i ) |
| { |
| assert( pObj->pData != NULL ); |
| Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) ); |
| } |
| // quit if the last frame |
| if ( f == nFrames - 1 ) |
| break; |
| // transfer to register outputs |
| Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) |
| pObjLo->pData = pObjLi->pData; |
| } |
| // remember register outputs |
| Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) |
| Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLi->pData ); |
| Aig_ManCleanup( pFrames ); |
| return pFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Unroll with initialization and mapping.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManFramesInitialMapped( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit ) |
| { |
| Aig_Man_t * pFrames; |
| Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pRepr; |
| int i, f, iNum1, iNum2, iFrame2; |
| assert( nFrames <= nFramesMax ); |
| assert( Saig_ManRegNum(pAig) > 0 ); |
| // start node map |
| Saig_ManStartMap1( pAig, nFramesMax ); |
| // start the new manager |
| pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFramesMax ); |
| // create variables for register outputs |
| if ( fInit ) |
| { |
| Saig_ManForEachLo( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_ManConst0( pFrames ); |
| Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular((Aig_Obj_t *)pObj->pData) ); |
| } |
| } |
| else |
| { |
| // create PIs first |
| for ( f = 0; f < nFramesMax; f++ ) |
| Saig_ManForEachPi( pAig, pObj, i ) |
| Aig_ObjCreateCi( pFrames ); |
| // create registers second |
| Saig_ManForEachLo( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_ObjCreateCi( pFrames ); |
| Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular((Aig_Obj_t *)pObj->pData) ); |
| } |
| } |
| // add timeframes |
| for ( f = 0; f < nFramesMax; f++ ) |
| { |
| // map the constant node |
| pObj = Aig_ManConst1(pAig); |
| pObj->pData = Aig_ManConst1( pFrames ); |
| Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) ); |
| // create PI nodes for this frame |
| Saig_ManForEachPi( pAig, pObj, i ) |
| { |
| if ( fInit ) |
| pObj->pData = Aig_ObjCreateCi( pFrames ); |
| else |
| pObj->pData = Aig_ManCi( pFrames, f * Saig_ManPiNum(pAig) + i ); |
| Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) ); |
| } |
| // add internal nodes of this frame |
| Aig_ManForEachNode( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); |
| Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) ); |
| if ( !Saig_ManHasMap2(pAig) ) |
| continue; |
| if ( f < nFrames ) |
| { |
| // get the mapping for this node |
| iNum2 = Saig_ManGetMap2( pAig, pObj, f, &iFrame2 ); |
| } |
| else |
| { |
| // get the mapping for this node |
| iNum2 = Saig_ManGetMap2( pAig, pObj, nFrames-1, &iFrame2 ); |
| iFrame2 += f - (nFrames-1); |
| } |
| assert( iNum2 != -1 ); |
| assert( f >= iFrame2 ); |
| // get the corresponding frames node |
| iNum1 = Saig_ManGetMap1( pAig, Aig_ManObj(pAig, iNum2), iFrame2 ); |
| pRepr = Aig_ManObj( pFrames, iNum1 ); |
| // compare the phases of these nodes |
| pObj->pData = Aig_NotCond( pRepr, pRepr->fPhase ^ Aig_ObjPhaseReal((Aig_Obj_t *)pObj->pData) ); |
| } |
| // create POs for this frame |
| Saig_ManForEachPo( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) ); |
| Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) ); |
| } |
| // save register inputs |
| Saig_ManForEachLi( pAig, pObj, i ) |
| { |
| pObj->pData = Aig_ObjChild0Copy(pObj); |
| Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) ); |
| } |
| // quit if the last frame |
| if ( f == nFramesMax - 1 ) |
| break; |
| // transfer to register outputs |
| Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) |
| { |
| pObjLo->pData = pObjLi->pData; |
| if ( !fInit ) |
| Saig_ManSetMap1( pAig, pObjLo, f+1, Aig_Regular((Aig_Obj_t *)pObjLo->pData) ); |
| } |
| } |
| if ( !fInit ) |
| { |
| // create registers |
| Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) |
| Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLi->pData ); |
| // set register number |
| Aig_ManSetRegNum( pFrames, pAig->nRegs ); |
| } |
| Aig_ManCleanup( pFrames ); |
| Saig_ManStopMap1( pAig ); |
| return pFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Implements dynamic simplification.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose ) |
| { |
| // extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve ); |
| Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2; |
| abctime clk; |
| // create uninitialized timeframes with map1 |
| pFrames = Saig_ManFramesNonInitial( pAig, nFrames ); |
| // perform fraiging for the unrolled timeframes |
| clk = Abc_Clock(); |
| pFraig = Fra_FraigEquivence( pFrames, 1000, 0 ); |
| // report the results |
| if ( fVerbose ) |
| { |
| Aig_ManPrintStats( pFrames ); |
| Aig_ManPrintStats( pFraig ); |
| ABC_PRT( "Fraiging", Abc_Clock() - clk ); |
| } |
| Aig_ManStop( pFraig ); |
| assert( pFrames->pReprs != NULL ); |
| // create AIG with map2 |
| Saig_ManCreateMapping( pAig, pFrames, nFrames ); |
| Aig_ManStop( pFrames ); |
| Saig_ManStopMap1( pAig ); |
| // create reduced initialized timeframes |
| clk = Abc_Clock(); |
| pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); |
| ABC_PRT( "Mapped", Abc_Clock() - clk ); |
| // free mapping |
| Saig_ManStopMap2( pAig ); |
| clk = Abc_Clock(); |
| pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); |
| ABC_PRT( "Normal", Abc_Clock() - clk ); |
| // report the results |
| if ( fVerbose ) |
| { |
| Aig_ManPrintStats( pRes1 ); |
| Aig_ManPrintStats( pRes2 ); |
| } |
| Aig_ManStop( pRes1 ); |
| assert( !Saig_ManHasMap1(pAig) ); |
| assert( !Saig_ManHasMap2(pAig) ); |
| return pRes2; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
