pdrTsim.c File Reference

#include "pdrInt.h"

Go to the source code of this file.

Macros
#define	PDR_ZER   1
	DECLARATIONS ///. More...
#define	PDR_ONE   2
#define	PDR_UND   3

Functions
static int	Pdr_ManSimInfoNot (int Value)
static int	Pdr_ManSimInfoAnd (int Value0, int Value1)
static int	Pdr_ManSimInfoGet (Aig_Man_t *p, Aig_Obj_t *pObj)
static void	Pdr_ManSimInfoSet (Aig_Man_t *p, Aig_Obj_t *pObj, int Value)
void	Pdr_ManCollectCone_rec (Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes)
	FUNCTION DEFINITIONS ///. More...
void	Pdr_ManCollectCone (Aig_Man_t *pAig, Vec_Int_t *vCoObjs, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes)
int	Pdr_ManExtendOneEval (Aig_Man_t *pAig, Aig_Obj_t *pObj)
int	Pdr_ManSimDataInit (Aig_Man_t *pAig, Vec_Int_t *vCiObjs, Vec_Int_t *vCiVals, Vec_Int_t *vNodes, Vec_Int_t *vCoObjs, Vec_Int_t *vCoVals, Vec_Int_t *vCi2Rem)
int	Pdr_ManExtendOne (Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vUndo, Vec_Int_t *vVis)
void	Pdr_ManExtendUndo (Aig_Man_t *pAig, Vec_Int_t *vUndo)
void	Pdr_ManDeriveResult (Aig_Man_t *pAig, Vec_Int_t *vCiObjs, Vec_Int_t *vCiVals, Vec_Int_t *vCi2Rem, Vec_Int_t *vRes, Vec_Int_t *vPiLits)
void	Pdr_ManPrintCex (Aig_Man_t *pAig, Vec_Int_t *vCiObjs, Vec_Int_t *vCiVals, Vec_Int_t *vCi2Rem)
Pdr_Set_t *	Pdr_ManTernarySim (Pdr_Man_t *p, int k, Pdr_Set_t *pCube)

Macro Definition Documentation

#define PDR_ONE   2

Definition at line 30 of file pdrTsim.c.

#define PDR_UND   3

Definition at line 31 of file pdrTsim.c.

#define PDR_ZER   1

DECLARATIONS ///.

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

FileName [pdrTsim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Ternary simulation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - November 20, 2010.]

Revision [

Id:

pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

]

Definition at line 29 of file pdrTsim.c.

Function Documentation

void Pdr_ManCollectCone	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vCoObjs,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vNodes
	)

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

Synopsis [Marks the TFI cone and collects CIs and nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file pdrTsim.c.

{
    Aig_Obj_t * pObj;
    int i;
    Vec_IntClear( vCiObjs );
    Vec_IntClear( vNodes );
    Aig_ManIncrementTravId( pAig );
    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
        Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes );
}

void Pdr_ManCollectCone_rec	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pObj,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vNodes
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Marks the TFI cone and collects CIs and nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file pdrTsim.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(pAig, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
        return;
    }
    Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
    if ( Aig_ObjIsCo(pObj) )
        return;
    Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
    Vec_IntPush( vNodes, Aig_ObjId(pObj) );
}

void Pdr_ManDeriveResult	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vCiVals,
		Vec_Int_t *	vCi2Rem,
		Vec_Int_t *	vRes,
		Vec_Int_t *	vPiLits
	)

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

Synopsis [Derives the resulting cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file pdrTsim.c.

{
    Aig_Obj_t * pObj;
    int i, Lit;
    // mark removed flop outputs
    Aig_ManIncrementTravId( pAig );
    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
    {
        assert( Saig_ObjIsLo( pAig, pObj ) );
        Aig_ObjSetTravIdCurrent(pAig, pObj);
    }
    // collect flop outputs that are not marked
    Vec_IntClear( vRes );
    Vec_IntClear( vPiLits );
    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
    {
        if ( Saig_ObjIsPi(pAig, pObj) )
        {
            Lit = toLitCond( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
            Vec_IntPush( vPiLits, Lit );
            continue;
        }
        assert( Saig_ObjIsLo(pAig, pObj) );
        if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
            continue;
        Lit = toLitCond( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
        Vec_IntPush( vRes, Lit );
    }
    if ( Vec_IntSize(vRes) == 0 )
        Vec_IntPush(vRes, 0);
}

int Pdr_ManExtendOne	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pObj,
		Vec_Int_t *	vUndo,
		Vec_Int_t *	vVis
	)

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

Synopsis [Tries to assign ternary value to one of the CIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 199 of file pdrTsim.c.

{
    Aig_Obj_t * pFanout;
    int i, k, iFanout = -1, Value, Value2;
    assert( Saig_ObjIsLo(pAig, pObj) );
    assert( Aig_ObjIsTravIdCurrent(pAig, pObj) );
    // save original value
    Value = Pdr_ManSimInfoGet( pAig, pObj );
    assert( Value == PDR_ZER || Value == PDR_ONE );
    Vec_IntPush( vUndo, Aig_ObjId(pObj) );
    Vec_IntPush( vUndo, Value );
    // update original value
    Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
    // traverse
    Vec_IntClear( vVis );
    Vec_IntPush( vVis, Aig_ObjId(pObj) );
    Aig_ManForEachObjVec( vVis, pAig, pObj, i )
    {
        Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k )
        {
            if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
                continue;
            assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
            Value = Pdr_ManSimInfoGet( pAig, pFanout );
            if ( Value == PDR_UND )
                continue;
            Value2 = Pdr_ManExtendOneEval( pAig, pFanout );
            if ( Value2 == Value )
                continue;
            assert( Value2 == PDR_UND );
            Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
            Vec_IntPush( vUndo, Value );
            if ( Aig_ObjIsCo(pFanout) )
                return 0;
            assert( Aig_ObjIsNode(pFanout) );
            Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
        }
    }
    return 1;
}

int Pdr_ManExtendOneEval	(	Aig_Man_t *	pAig,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Performs ternary simulation for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file pdrTsim.c.

{
    int Value0, Value1, Value;
    Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
    if ( Aig_ObjFaninC0(pObj) )
        Value0 = Pdr_ManSimInfoNot( Value0 );
    if ( Aig_ObjIsCo(pObj) )
    {
        Pdr_ManSimInfoSet( pAig, pObj, Value0 );
        return Value0;
    }
    assert( Aig_ObjIsNode(pObj) );
    Value1 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin1(pObj) );
    if ( Aig_ObjFaninC1(pObj) )
        Value1 = Pdr_ManSimInfoNot( Value1 );
    Value = Pdr_ManSimInfoAnd( Value0, Value1 );
    Pdr_ManSimInfoSet( pAig, pObj, Value );
    return Value;
}

void Pdr_ManExtendUndo	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vUndo
	)

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

Synopsis [Undoes the partial results of ternary simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file pdrTsim.c.

{
    Aig_Obj_t * pObj;
    int i, Value;
    Aig_ManForEachObjVec( vUndo, pAig, pObj, i )
    {
        Value  = Vec_IntEntry(vUndo, ++i);
        assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND );
        Pdr_ManSimInfoSet( pAig, pObj, Value );
    }
}

void Pdr_ManPrintCex	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vCiVals,
		Vec_Int_t *	vCi2Rem
	)

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

Synopsis [Derives the resulting cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file pdrTsim.c.

{
    Aig_Obj_t * pObj;
    int i;
    char * pBuff = ABC_ALLOC( char, Aig_ManCiNum(pAig)+1 );
    for ( i = 0; i < Aig_ManCiNum(pAig); i++ )
        pBuff[i] = '-';
    pBuff[i] = 0;
    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
        pBuff[Aig_ObjCioId(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
    if ( vCi2Rem )
    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
        pBuff[Aig_ObjCioId(pObj)] = 'x';
    Abc_Print( 1, "%s\n", pBuff );
    ABC_FREE( pBuff );
}

int Pdr_ManSimDataInit	(	Aig_Man_t *	pAig,
		Vec_Int_t *	vCiObjs,
		Vec_Int_t *	vCiVals,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vCoObjs,
		Vec_Int_t *	vCoVals,
		Vec_Int_t *	vCi2Rem
	)

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

Synopsis [Performs ternary simulation for one design.]

Description []

SideEffects []

SeeAlso []

Definition at line 161 of file pdrTsim.c.

{
    Aig_Obj_t * pObj;
    int i;
    // set the CI values
    Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE );
    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
        Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) );
    // set the FOs to remove
    if ( vCi2Rem != NULL )
    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
        Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
    // perform ternary simulation
    Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
        Pdr_ManExtendOneEval( pAig, pObj );
    // transfer results to the output
    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
        Pdr_ManExtendOneEval( pAig, pObj );
    // check the results
    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
        if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) )
            return 0;
    return 1;
}

static int Pdr_ManSimInfoAnd ( int  Value0, int  Value1  )

inlinestatic

Definition at line 42 of file pdrTsim.c.

{
    if ( Value0 == PDR_ZER || Value1 == PDR_ZER )
        return PDR_ZER;
    if ( Value0 == PDR_ONE && Value1 == PDR_ONE )
        return PDR_ONE;
    return PDR_UND;
}

static int Pdr_ManSimInfoGet ( Aig_Man_t *  p, Aig_Obj_t *  pObj  )

inlinestatic

Definition at line 51 of file pdrTsim.c.

{
    return 3 & (p->pTerSimData[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
}

static int Pdr_ManSimInfoNot ( int  Value )

inlinestatic

Definition at line 33 of file pdrTsim.c.

{
    if ( Value == PDR_ZER )
        return PDR_ONE;
    if ( Value == PDR_ONE )
        return PDR_ZER;
    return PDR_UND;
}

static void Pdr_ManSimInfoSet ( Aig_Man_t *  p, Aig_Obj_t *  pObj, int  Value  )

inlinestatic

Definition at line 56 of file pdrTsim.c.

{
    assert( Value >= PDR_ZER && Value <= PDR_UND );
    Value ^= Pdr_ManSimInfoGet( p, pObj );
    p->pTerSimData[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
}

Pdr_Set_t* Pdr_ManTernarySim	(	Pdr_Man_t *	p,
		int	k,
		Pdr_Set_t *	pCube
	)

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

Synopsis [Shrinks values using ternary simulation.]

Description [The cube contains the set of flop index literals which, when converted into a clause and applied to the combinational outputs, led to a satisfiable SAT run in frame k (values stored in the SAT solver). If the cube is NULL, it is assumed that the first property output was asserted and failed. The resulting array is a set of flop index literals that asserts the COs. Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]

SideEffects []

SeeAlso []

Definition at line 351 of file pdrTsim.c.

{
    Pdr_Set_t * pRes;
    Vec_Int_t * vPrio   = p->vPrio;    // priority flops (flop indices)
    Vec_Int_t * vPiLits = p->vLits;    // array of literals (0/1 PI values)
    Vec_Int_t * vCiObjs = p->vCiObjs;  // cone leaves (CI obj IDs)
    Vec_Int_t * vCoObjs = p->vCoObjs;  // cone roots (CO obj IDs)
    Vec_Int_t * vCiVals = p->vCiVals;  // cone leaf values (0/1 CI values)
    Vec_Int_t * vCoVals = p->vCoVals;  // cone root values (0/1 CO values)
    Vec_Int_t * vNodes  = p->vNodes;   // cone nodes (node obj IDs)
    Vec_Int_t * vUndo   = p->vUndo;    // cone undos (node obj IDs)
    Vec_Int_t * vVisits = p->vVisits;  // intermediate (obj IDs)
    Vec_Int_t * vCi2Rem = p->vCi2Rem;  // CIs to be removed (CI obj IDs)
    Vec_Int_t * vRes    = p->vRes;     // final result (flop literals)
    Aig_Obj_t * pObj;
    int i, Entry, RetValue;
    abctime clk = Abc_Clock();

    // collect CO objects
    Vec_IntClear( vCoObjs );
    if ( pCube == NULL ) // the target is the property output
    {
//        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, p->iOutCur)) );
    }
    else // the target is the cube
    {
        for ( i = 0; i < pCube->nLits; i++ )
        {
            if ( pCube->Lits[i] == -1 )
                continue;
            pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1));
            Vec_IntPush( vCoObjs, Aig_ObjId(pObj) );
        }
    }
if ( p->pPars->fVeryVerbose )
{
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
    Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
else
    Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}

    // collect CI objects
    Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes );
    // collect values
    Pdr_ManCollectValues( p, k, vCiObjs, vCiVals );
    Pdr_ManCollectValues( p, k, vCoObjs, vCoVals );
    // simulate for the first time
if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
    RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
    assert( RetValue );

#if 1
    // try removing high-priority flops
    Vec_IntClear( vCi2Rem );
    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
    {
        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
            continue;
        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
        if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
            continue;
        Vec_IntClear( vUndo );
        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
        else
            Pdr_ManExtendUndo( p->pAig, vUndo );
    }
    // try removing low-priority flops
    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
    {
        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
            continue;
        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
        if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
            continue;
        Vec_IntClear( vUndo );
        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
        else
            Pdr_ManExtendUndo( p->pAig, vUndo );
    }
#else
    // try removing low-priority flops
    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
    {
        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
            continue;
        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
        if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
            continue;
        Vec_IntClear( vUndo );
        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
        else
            Pdr_ManExtendUndo( p->pAig, vUndo );
    }
    // try removing high-priority flops
    Vec_IntClear( vCi2Rem );
    Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
    {
        if ( !Saig_ObjIsLo( p->pAig, pObj ) )
            continue;
        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
        if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
            continue;
        Vec_IntClear( vUndo );
        if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
            Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
        else
            Pdr_ManExtendUndo( p->pAig, vUndo );
    }
#endif

if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
    RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
    assert( RetValue );

    // derive the set of resulting registers
    Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
    assert( Vec_IntSize(vRes) > 0 );
    p->tTsim += Abc_Clock() - clk;
    pRes = Pdr_SetCreate( vRes, vPiLits );
    assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
    return pRes;
}