sswAig.c File Reference

#include "sswInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Ssw_Frm_t *	Ssw_FrmStart (Aig_Man_t *pAig)
	DECLARATIONS ///. More...
void	Ssw_FrmStop (Ssw_Frm_t *p)
static void	Ssw_FramesConstrainNode (Ssw_Man_t *p, Aig_Man_t *pFrames, Aig_Man_t *pAig, Aig_Obj_t *pObj, int iFrame, int fTwoPos)
Aig_Man_t *	Ssw_FramesWithClasses (Ssw_Man_t *p)
Aig_Man_t *	Ssw_SpeculativeReduction (Ssw_Man_t *p)

Function Documentation

static void Ssw_FramesConstrainNode ( Ssw_Man_t *  p, Aig_Man_t *  pFrames, Aig_Man_t *  pAig, Aig_Obj_t *  pObj, int  iFrame, int  fTwoPos  )

inlinestatic

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

Synopsis [Performs speculative reduction for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file sswAig.c.

{
    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
    // skip nodes without representative
    pObjRepr = Aig_ObjRepr(pAig, pObj);
    if ( pObjRepr == NULL )
        return;
    p->nConstrTotal++;
    assert( pObjRepr->Id < pObj->Id );
    // get the new node
    pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
    // get the new node of the representative
    pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
    // if this is the same node, no need to add constraints
    if ( pObj->fPhase == pObjRepr->fPhase )
    {
        assert( pObjNew != Aig_Not(pObjReprNew) );
        if ( pObjNew == pObjReprNew )
            return;
    }
    else
    {
        assert( pObjNew != pObjReprNew );
        if ( pObjNew == Aig_Not(pObjReprNew) )
            return;
    }
    p->nConstrReduced++;
    // these are different nodes - perform speculative reduction
    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
    // set the new node
    Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
    // add the constraint
    if ( fTwoPos )
    {
        Aig_ObjCreateCo( pFrames, pObjNew2 );
        Aig_ObjCreateCo( pFrames, pObjNew );
    }
    else
    {
        pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 );
        Aig_ObjCreateCo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
    }
}

Aig_Man_t* Ssw_FramesWithClasses

(

Ssw_Man_t *

p

)

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

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 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;
    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;
}

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

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

Aig_Man_t* Ssw_SpeculativeReduction

(

Ssw_Man_t *

p

)

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

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 212 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;
}