sswAig.c File Reference

#include "sswInt.h"

Include dependency graph for sswAig.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Ssw_Frm_t *	Ssw_FrmStart (Aig_Man_t *pAig)
	DECLARATIONS ///.
void	Ssw_FrmStop (Ssw_Frm_t *p)
int	Aig_ObjDeref_rec (Aig_Obj_t *pNode)
int	Aig_ObjRef_rec (Aig_Obj_t *pNode)
int	Aig_ManConeSize (Aig_Obj_t *pNode0, Aig_Obj_t *pNode1)
Aig_Man_t *	Ssw_FramesWithClasses (Ssw_Man_t *p)
Aig_Man_t *	Ssw_SpeculativeReduction (Ssw_Man_t *p)

Function Documentation

Aig_ManConeSize()

int Aig_ManConeSize	(	Aig_Obj_t *	pNode0,
		Aig_Obj_t *	pNode1 )

Definition at line 115 of file sswAig.c.

{
    pNode0 = Aig_Regular(pNode0);
    pNode1 = Aig_Regular(pNode1);
    Aig_ObjRef( pNode0 );
    Aig_ObjRef( pNode1 );
    int Count0 = Aig_ObjDeref_rec(pNode0) + Aig_ObjDeref_rec(pNode1);
    int Count1 = Aig_ObjRef_rec(pNode0)   + Aig_ObjRef_rec(pNode1);   
    Aig_ObjDeref( pNode0 );
    Aig_ObjDeref( pNode1 );     
    assert( Count0 == Count1 );
    return Count0;
}

Here is the call graph for this function:

Aig_ObjDeref_rec()

int Aig_ObjDeref_rec

(

Aig_Obj_t *

pNode

)

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

Synopsis [Computes the size of two-output cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file sswAig.c.

{
    int Counter = 1;
    assert( pNode->nRefs > 0 );
    if ( --pNode->nRefs > 0 )
        return 0;
    assert( pNode->nRefs == 0 );
    if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
        return 0;
    Counter += Aig_ObjDeref_rec( Aig_ObjFanin0(pNode) );
    Counter += Aig_ObjDeref_rec( Aig_ObjFanin1(pNode) );
    return Counter;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Aig_ObjRef_rec()

int Aig_ObjRef_rec

(

Aig_Obj_t *

pNode

)

Definition at line 102 of file sswAig.c.

{
    int Counter = 1;
    assert( pNode->nRefs >= 0 );
    if ( pNode->nRefs++ > 0 )
        return 0;
    assert( pNode->nRefs == 1 );
    if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
        return 0;
    Counter += Aig_ObjRef_rec( Aig_ObjFanin0(pNode) );
    Counter += Aig_ObjRef_rec( Aig_ObjFanin1(pNode) );
    return Counter;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_FramesWithClasses()

Aig_Man_t * Ssw_FramesWithClasses

(

Ssw_Man_t *

p

)

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

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file sswAig.c.

{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
    int i, f, iLits;
    assert( p->pFrames == NULL );
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
    p->nConstrTotal = p->nConstrReduced = 0;
 
    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
    // create latches for the first frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // add timeframes
    iLits = 0;
    if ( p->pPars->nSkip )
        srand(1);
    for ( f = 0; f < p->pPars->nFramesK; f++ )
    {
        // map constants and PIs
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjNew = Aig_ObjCreateCi(pFrames);
            pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
        }
        // set the constraints on the latch outputs
        Saig_ManForEachLo( p->pAig, pObj, i )
            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
        // add internal nodes of this frame
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
        }
        // transfer to the primary outputs
        Aig_ManForEachCo( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
        // transfer latch input to the latch outputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
            Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) );
    }
    assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
    // add the POs for the latch outputs of the last frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Aig_ObjCreateCo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
    // remove dangling nodes
    Aig_ManCleanup( pFrames );
    // make sure the satisfying assignment is node assigned
    assert( pFrames->pData == NULL );
//Aig_ManShow( pFrames, 0, NULL );
    return pFrames;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_FrmStart()

ABC_NAMESPACE_IMPL_START Ssw_Frm_t * Ssw_FrmStart

(

Aig_Man_t *

pAig

)

DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

CFile****************************************************************

FileName [sswAig.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [AIG manipulation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id

sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswAig.c.

{
    Ssw_Frm_t * p;
    p = ABC_ALLOC( Ssw_Frm_t, 1 );
    memset( p, 0, sizeof(Ssw_Frm_t) );
    p->pAig          = pAig;
    p->nObjs         = Aig_ManObjNumMax( pAig );
    p->nFrames       = 0;
    p->pFrames       = NULL;
    p->vAig2Frm      = Vec_PtrAlloc( 0 );
    Vec_PtrFill( p->vAig2Frm, 2 * p->nObjs, NULL );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_FrmStop()

void Ssw_FrmStop

(

Ssw_Frm_t *

p

)

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file sswAig.c.

{
    if ( p->pFrames )
        Aig_ManStop( p->pFrames );
    Vec_PtrFree( p->vAig2Frm );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SpeculativeReduction()

Aig_Man_t * Ssw_SpeculativeReduction

(

Ssw_Man_t *

p

)

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

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file sswAig.c.

{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjNew;
    int i;
    assert( p->pFrames == NULL );
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
    p->nConstrTotal = p->nConstrReduced = 0;
 
    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
    pFrames->pName = Abc_UtilStrsav( p->pAig->pName );
    // map constants and PIs
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // create latches for the first frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // set the constraints on the latch outputs
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
    // add internal nodes of this frame
    Aig_ManForEachNode( p->pAig, pObj, i )
    {
        pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
        Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
    }
    // add the POs for the latch outputs of the last frame
    Saig_ManForEachLi( p->pAig, pObj, i )
        Aig_ObjCreateCo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
    // remove dangling nodes
    Aig_ManCleanup( pFrames );
    Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
//    Abc_Print( 1, "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", 
//        p->nConstrTotal, p->nConstrReduced );
    return pFrames;
}

Here is the call graph for this function:

Here is the caller graph for this function: