From 6da56f1f0f6942e3fc257d8396588804c5891e93 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 16 May 2008 08:01:00 -0700 Subject: Version abc80516 --- src/aig/saig/saigTrans.c | 422 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 422 insertions(+) create mode 100644 src/aig/saig/saigTrans.c (limited to 'src/aig/saig/saigTrans.c') diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c new file mode 100644 index 00000000..b0039276 --- /dev/null +++ b/src/aig/saig/saigTrans.c @@ -0,0 +1,422 @@ +/**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" + +/* + 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( 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 = 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 = 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( 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 = 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 = 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_ObjCreatePi( pFrames ); + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( 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_ObjCreatePo( 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(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_ObjCreatePo( pFrames, 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(pObj->pData) ); + } + } + else + { + // create PIs first + for ( f = 0; f < nFramesMax; f++ ) + Saig_ManForEachPi( pAig, pObj, i ) + Aig_ObjCreatePi( pFrames ); + // create registers second + Saig_ManForEachLo( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreatePi( pFrames ); + Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular(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(pObj->pData) ); + // create PI nodes for this frame + Saig_ManForEachPi( pAig, pObj, i ) + { + if ( fInit ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + else + pObj->pData = Aig_ManPi( pFrames, f * Saig_ManPiNum(pAig) + i ); + Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(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(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(pObj->pData) ); + } + // create POs for this frame + Saig_ManForEachPo( pAig, pObj, i ) + { + pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) ); + } + // save register inputs + Saig_ManForEachLi( pAig, pObj, i ) + { + pObj->pData = Aig_ObjChild0Copy(pObj); + Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(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(pObjLo->pData) ); + } + } + if ( !fInit ) + { + // create registers + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + Aig_ObjCreatePo( pFrames, 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; + int clk, clkTotal = clock(); + // create uninitialized timeframes with map1 + pFrames = Saig_ManFramesNonInitial( pAig, nFrames ); + // perform fraiging for the unrolled timeframes +clk = clock(); + pFraig = Fra_FraigEquivence( pFrames, 1000, 0 ); + // report the results + if ( fVerbose ) + { + Aig_ManPrintStats( pFrames ); + Aig_ManPrintStats( pFraig ); +PRT( "Fraiging", 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 = clock(); + pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); +PRT( "Mapped", clock() - clk ); + // free mapping + Saig_ManStopMap2( pAig ); +clk = clock(); + pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit ); +PRT( "Normal", 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 /// +//////////////////////////////////////////////////////////////////////// + + -- cgit v1.2.3