saigTrans.c File Reference

#include "saig.h"
#include "proof/fra/fra.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START void	Saig_ManStartMap1 (Aig_Man_t *p, int nFrames)
	DECLARATIONS ///. More...
static void	Saig_ManStopMap1 (Aig_Man_t *p)
static int	Saig_ManHasMap1 (Aig_Man_t *p)
static void	Saig_ManSetMap1 (Aig_Man_t *p, Aig_Obj_t *pOld, int f1, Aig_Obj_t *pNew)
static int	Saig_ManGetMap1 (Aig_Man_t *p, Aig_Obj_t *pOld, int f1)
static void	Saig_ManStartMap2 (Aig_Man_t *p, int nFrames)
static void	Saig_ManStopMap2 (Aig_Man_t *p)
static int	Saig_ManHasMap2 (Aig_Man_t *p)
static void	Saig_ManSetMap2 (Aig_Man_t *p, Aig_Obj_t *pOld, int f1, Aig_Obj_t *pNew, int f2)
static int	Saig_ManGetMap2 (Aig_Man_t *p, Aig_Obj_t *pOld, int f1, int *pf2)
void	Saig_ManCreateMapping (Aig_Man_t *pAig, Aig_Man_t *pFrames, int nFrames)
Aig_Man_t *	Saig_ManFramesNonInitial (Aig_Man_t *pAig, int nFrames)
Aig_Man_t *	Saig_ManFramesInitialMapped (Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit)
Aig_Man_t *	Saig_ManTimeframeSimplify (Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit, int fVerbose)

Function Documentation

void Saig_ManCreateMapping	(	Aig_Man_t *	pAig,
		Aig_Man_t *	pFrames,
		int	nFrames
	)

Function*************************************************************

Synopsis [Create mapping for the first nFrames timeframes of pAig.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file saigTrans.c.

{
    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) );
}

Aig_Man_t* Saig_ManFramesInitialMapped	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	nFramesMax,
		int	fInit
	)

Function*************************************************************

Synopsis [Unroll with initialization and mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 256 of file saigTrans.c.

{
    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;
}

Aig_Man_t* Saig_ManFramesNonInitial	(	Aig_Man_t *	pAig,
		int	nFrames
	)

Function*************************************************************

Synopsis [Unroll without initialization.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file saigTrans.c.

{
    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;
}

static int Saig_ManGetMap1 ( Aig_Man_t *  p, Aig_Obj_t *  pOld, int  f1  )

inlinestatic

Definition at line 81 of file saigTrans.c.

{
    Vec_Int_t * vMap = (Vec_Int_t *)p->pData;
    int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
    return Vec_IntEntry( vMap, nOffset );
}

static int Saig_ManGetMap2 ( Aig_Man_t *  p, Aig_Obj_t *  pOld, int  f1, int *  pf2  )

inlinestatic

Definition at line 129 of file saigTrans.c.

{
    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 );
}

static int Saig_ManHasMap1 ( Aig_Man_t *  p )

inlinestatic

Definition at line 69 of file saigTrans.c.

{
    return (int)(p->pData != NULL);
}

static int Saig_ManHasMap2 ( Aig_Man_t *  p )

inlinestatic

Definition at line 116 of file saigTrans.c.

{
    return (int)(p->pData2 != NULL);
}

static void Saig_ManSetMap1 ( Aig_Man_t *  p, Aig_Obj_t *  pOld, int  f1, Aig_Obj_t *  pNew  )

inlinestatic

Definition at line 73 of file saigTrans.c.

{
    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 void Saig_ManSetMap2 ( Aig_Man_t *  p, Aig_Obj_t *  pOld, int  f1, Aig_Obj_t *  pNew, int  f2  )

inlinestatic

Definition at line 120 of file saigTrans.c.

{
    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 ABC_NAMESPACE_IMPL_START void Saig_ManStartMap1 ( Aig_Man_t *  p, int  nFrames  )

inlinestatic

DECLARATIONS ///.

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Maps a node/frame into a node of a different manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file saigTrans.c.

{
    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 void Saig_ManStartMap2 ( Aig_Man_t *  p, int  nFrames  )

inlinestatic

Function*************************************************************

Synopsis [Maps a node/frame into a node/frame of a different manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file saigTrans.c.

{
    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 void Saig_ManStopMap1 ( Aig_Man_t *  p )

inlinestatic

Definition at line 63 of file saigTrans.c.

{
    assert( p->pData != NULL );
    Vec_IntFree( (Vec_Int_t *)p->pData );
    p->pData = NULL;
}

static void Saig_ManStopMap2 ( Aig_Man_t *  p )

inlinestatic

Definition at line 110 of file saigTrans.c.

{
    assert( p->pData2 != NULL );
    Vec_IntFree( (Vec_Int_t *)p->pData2 );
    p->pData2 = NULL;
}

Aig_Man_t* Saig_ManTimeframeSimplify	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	nFramesMax,
		int	fInit,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Implements dynamic simplification.]

Description []

SideEffects []

SeeAlso []

Definition at line 378 of file saigTrans.c.

{
//    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;
}