/**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