absOldSim.c File Reference

#include "abs.h"

Go to the source code of this file.

Macros
#define	SAIG_ZER   1
	DECLARATIONS ///. More...
#define	SAIG_ONE   2
#define	SAIG_UND   3
#define	SAIG_ZER_NEW   0
#define	SAIG_ONE_NEW   1
#define	SAIG_ZER_OLD   2
#define	SAIG_ONE_OLD   3

Functions
static int	Saig_ManSimInfoNot (int Value)
static int	Saig_ManSimInfoAnd (int Value0, int Value1)
static int	Saig_ManSimInfoGet (Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
static void	Saig_ManSimInfoSet (Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame, int Value)
static int	Saig_ManSimInfo2IsOld (int Value)
static int	Saig_ManSimInfo2SetOld (int Value)
static int	Saig_ManSimInfo2Not (int Value)
static int	Saig_ManSimInfo2And (int Value0, int Value1)
static int	Saig_ManSimInfo2Get (Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
static void	Saig_ManSimInfo2Set (Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame, int Value)
int	Saig_ManExtendOneEval (Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
	FUNCTION DEFINITIONS ///. More...
int	Saig_ManSimDataInit (Aig_Man_t *p, Abc_Cex_t *pCex, Vec_Ptr_t *vSimInfo, Vec_Int_t *vRes)
int	Saig_ManExtendOneEval2 (Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
int	Saig_ManSimDataInit2 (Aig_Man_t *p, Abc_Cex_t *pCex, Vec_Ptr_t *vSimInfo)
void	Saig_ManSetAndDriveImplications_rec (Aig_Man_t *p, Aig_Obj_t *pObj, int f, int fMax, Vec_Ptr_t *vSimInfo)
void	Saig_ManExplorePaths_rec (Aig_Man_t *p, Aig_Obj_t *pObj, int f, int fMax, Vec_Ptr_t *vSimInfo)
Vec_Int_t *	Saig_ManProcessCex (Aig_Man_t *p, int iFirstFlopPi, Abc_Cex_t *pCex, Vec_Ptr_t *vSimInfo, int fVerbose)
Vec_Int_t *	Saig_ManExtendCounterExampleTest2 (Aig_Man_t *p, int iFirstFlopPi, Abc_Cex_t *pCex, int fVerbose)

Macro Definition Documentation

#define SAIG_ONE   2

Definition at line 31 of file absOldSim.c.

#define SAIG_ONE_NEW   1

Definition at line 69 of file absOldSim.c.

#define SAIG_ONE_OLD   3

Definition at line 71 of file absOldSim.c.

#define SAIG_UND   3

Definition at line 32 of file absOldSim.c.

#define SAIG_ZER   1

DECLARATIONS ///.

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

FileName [saigSimExt2.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Extending simulation trace to contain ternary values.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

saigSimExt2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 30 of file absOldSim.c.

#define SAIG_ZER_NEW   0

Definition at line 68 of file absOldSim.c.

#define SAIG_ZER_OLD   2

Definition at line 70 of file absOldSim.c.

Function Documentation

void Saig_ManExplorePaths_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	f,
		int	fMax,
		Vec_Ptr_t *	vSimInfo
	)

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

Synopsis [Performs recursive sensetization analysis.]

Description []

SideEffects []

SeeAlso []

Definition at line 333 of file absOldSim.c.

{
    int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f );
    if ( Saig_ManSimInfo2IsOld( Value ) )
        return;
    Saig_ManSetAndDriveImplications_rec( p, pObj, f, fMax, vSimInfo );
    assert( !Aig_ObjIsConst1(pObj) );
    if ( Saig_ObjIsLo(p, pObj) && f == 0 )
        return;
    if ( Saig_ObjIsPi(p, pObj) )
    {
        // propagate implications of this assignment
        int i, iPiNum = Aig_ObjCioId(pObj);
        for ( i = fMax; i >= 0; i-- )
            if ( i != f )
                Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, iPiNum), i, fMax, vSimInfo );
        return;
    }
    if ( Saig_ObjIsLo( p, pObj ) )
    {
        assert( f > 0 );
        Saig_ManExplorePaths_rec( p, Saig_ObjLoToLi(p, pObj), f-1, fMax, vSimInfo );
        return;
    }
    if ( Aig_ObjIsCo(pObj) )
    {
        Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    if ( Value == SAIG_ZER_OLD )
    {
//        if ( (Aig_ObjId(pObj) & 1) == 0 )
            Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo );
//        else
//            Saig_ManExplorePaths_rec( p, Aig_ObjFanin1(pObj), f, fMax, vSimInfo );
    }
    else
    {
        Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo );
        Saig_ManExplorePaths_rec( p, Aig_ObjFanin1(pObj), f, fMax, vSimInfo );
    }
}

Vec_Int_t* Saig_ManExtendCounterExampleTest2	(	Aig_Man_t *	p,
		int	iFirstFlopPi,
		Abc_Cex_t *	pCex,
		int	fVerbose
	)

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

Synopsis [Returns the array of PIs for flops that should not be absracted.]

Description []

SideEffects []

SeeAlso []

Definition at line 443 of file absOldSim.c.

{
    Vec_Int_t * vRes;
    Vec_Ptr_t * vSimInfo;
    abctime clk;
    if ( Saig_ManPiNum(p) != pCex->nPis )
    {
        printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
            Aig_ManCiNum(p), pCex->nPis );
        return NULL;
    }
    Aig_ManFanoutStart( p );
    vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) );
    Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) );

clk = Abc_Clock();
    vRes = Saig_ManProcessCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
    if ( fVerbose )
    {
        printf( "Total new PIs = %3d. Non-removable PIs = %3d.  ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }
    Vec_PtrFree( vSimInfo );
    Aig_ManFanoutStop( p );
    return vRes;
}

int Saig_ManExtendOneEval	(	Vec_Ptr_t *	vSimInfo,
		Aig_Obj_t *	pObj,
		int	iFrame
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Performs ternary simulation for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file absOldSim.c.

{
    int Value0, Value1, Value;
    Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame );
    if ( Aig_ObjFaninC0(pObj) )
        Value0 = Saig_ManSimInfoNot( Value0 );
    if ( Aig_ObjIsCo(pObj) )
    {
        Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
        return Value0;
    }
    assert( Aig_ObjIsNode(pObj) );
    Value1 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin1(pObj), iFrame );
    if ( Aig_ObjFaninC1(pObj) )
        Value1 = Saig_ManSimInfoNot( Value1 );
    Value = Saig_ManSimInfoAnd( Value0, Value1 );
    Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
    return Value;
}

int Saig_ManExtendOneEval2	(	Vec_Ptr_t *	vSimInfo,
		Aig_Obj_t *	pObj,
		int	iFrame
	)

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

Synopsis [Performs ternary simulation for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file absOldSim.c.

{
    int Value0, Value1, Value;
    Value0 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin0(pObj), iFrame );
    if ( Aig_ObjFaninC0(pObj) )
        Value0 = Saig_ManSimInfo2Not( Value0 );
    if ( Aig_ObjIsCo(pObj) )
    {
        Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value0 );
        return Value0;
    }
    assert( Aig_ObjIsNode(pObj) );
    Value1 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin1(pObj), iFrame );
    if ( Aig_ObjFaninC1(pObj) )
        Value1 = Saig_ManSimInfo2Not( Value1 );
    Value = Saig_ManSimInfo2And( Value0, Value1 );
    Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value );
    return Value;
}

Vec_Int_t* Saig_ManProcessCex	(	Aig_Man_t *	p,
		int	iFirstFlopPi,
		Abc_Cex_t *	pCex,
		Vec_Ptr_t *	vSimInfo,
		int	fVerbose
	)

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

Synopsis [Returns the array of PIs for flops that should not be absracted.]

Description []

SideEffects []

SeeAlso []

Definition at line 388 of file absOldSim.c.

{
    Aig_Obj_t * pObj;
    Vec_Int_t * vRes, * vResInv;
    int i, f, Value;
//    assert( Aig_ManRegNum(p) > 0 );
    assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) );
    // start simulation data
    Value = Saig_ManSimDataInit2( p, pCex, vSimInfo );
    assert( Value == SAIG_ONE_NEW );
    // derive implications of constants and primary inputs
    Saig_ManForEachLo( p, pObj, i )
        Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo );
    for ( f = pCex->iFrame; f >= 0; f-- )
    {
        Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo );
        for ( i = 0; i < iFirstFlopPi; i++ )
            Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, i), f, pCex->iFrame, vSimInfo );
    }
    // recursively compute justification
    Saig_ManExplorePaths_rec( p, Aig_ManCo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo );
    // select the result
    vRes = Vec_IntAlloc( 1000 );
    vResInv = Vec_IntAlloc( 1000 );
    for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
    {
        for ( f = pCex->iFrame; f >= 0; f-- )
        {
            Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManCi(p, i), f );
            if ( Saig_ManSimInfo2IsOld( Value ) )
                break;
        }
        if ( f >= 0 )
            Vec_IntPush( vRes, i );
        else
            Vec_IntPush( vResInv, i );
    }
    // resimulate to make sure it is valid
    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
    assert( Value == SAIG_ONE );
    Vec_IntFree( vResInv );
    return vRes;
}

void Saig_ManSetAndDriveImplications_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	f,
		int	fMax,
		Vec_Ptr_t *	vSimInfo
	)

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

Synopsis [Drive implications of the given node towards primary outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 280 of file absOldSim.c.

{
    Aig_Obj_t * pFanout;
    int k, iFanout = -1, Value0, Value1;
    int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f );
    assert( !Saig_ManSimInfo2IsOld( Value ) );
    Saig_ManSimInfo2Set( vSimInfo, pObj, f, Saig_ManSimInfo2SetOld(Value) );
    if ( (Aig_ObjIsCo(pObj) && f == fMax) || Saig_ObjIsPo(p, pObj) )
        return;
    if ( Saig_ObjIsLi( p, pObj ) )
    {
        assert( f < fMax );
        pFanout = Saig_ObjLiToLo(p, pObj);
        Value = Saig_ManSimInfo2Get( vSimInfo, pFanout, f+1 );
        if ( !Saig_ManSimInfo2IsOld( Value ) )
            Saig_ManSetAndDriveImplications_rec( p, pFanout, f+1, fMax, vSimInfo );
        return;
    }
    assert( Aig_ObjIsCi(pObj) || Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) );
    Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k )
    {
        Value = Saig_ManSimInfo2Get( vSimInfo, pFanout, f );
        if ( Saig_ManSimInfo2IsOld( Value ) )
            continue;
        if ( Aig_ObjIsCo(pFanout) )
        {
            Saig_ManSetAndDriveImplications_rec( p, pFanout, f, fMax, vSimInfo );
            continue;
        }
        assert( Aig_ObjIsNode(pFanout) );
        Value0 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin0(pFanout), f );
        Value1 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin1(pFanout), f );
        if ( Aig_ObjFaninC0(pFanout) )
            Value0 = Saig_ManSimInfo2Not( Value0 );
        if ( Aig_ObjFaninC1(pFanout) )
            Value1 = Saig_ManSimInfo2Not( Value1 );
        if ( Value0 == SAIG_ZER_OLD || Value1 == SAIG_ZER_OLD || 
            (Value0 == SAIG_ONE_OLD && Value1 == SAIG_ONE_OLD) )
            Saig_ManSetAndDriveImplications_rec( p, pFanout, f, fMax, vSimInfo );
    }
}

int Saig_ManSimDataInit	(	Aig_Man_t *	p,
		Abc_Cex_t *	pCex,
		Vec_Ptr_t *	vSimInfo,
		Vec_Int_t *	vRes
	)

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

Synopsis [Performs ternary simulation for one design.]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file absOldSim.c.

{
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i, f, Entry, iBit = 0;
    Saig_ManForEachLo( p, pObj, i )
        Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE );
        Saig_ManForEachPi( p, pObj, i )
            Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
        if ( vRes )
        Vec_IntForEachEntry( vRes, Entry, i )
            Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND );
        Aig_ManForEachNode( p, pObj, i )
            Saig_ManExtendOneEval( vSimInfo, pObj, f );
        Aig_ManForEachCo( p, pObj, i )
            Saig_ManExtendOneEval( vSimInfo, pObj, f );
        if ( f == pCex->iFrame )
            break;
        Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
            Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) );
    }
    // make sure the output of the property failed
    pObj = Aig_ManCo( p, pCex->iPo );
    return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame );
}

int Saig_ManSimDataInit2	(	Aig_Man_t *	p,
		Abc_Cex_t *	pCex,
		Vec_Ptr_t *	vSimInfo
	)

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

Synopsis [Performs sensitization analysis for one design.]

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file absOldSim.c.

{
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i, f, iBit = 0;
    Saig_ManForEachLo( p, pObj, i )
        Saig_ManSimInfo2Set( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW );
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        Saig_ManSimInfo2Set( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE_NEW );
        Saig_ManForEachPi( p, pObj, i )
            Saig_ManSimInfo2Set( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW );
        Aig_ManForEachNode( p, pObj, i )
            Saig_ManExtendOneEval2( vSimInfo, pObj, f );
        Aig_ManForEachCo( p, pObj, i )
            Saig_ManExtendOneEval2( vSimInfo, pObj, f );
        if ( f == pCex->iFrame )
            break;
        Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
            Saig_ManSimInfo2Set( vSimInfo, pObjLo, f+1, Saig_ManSimInfo2Get(vSimInfo, pObjLi, f) );
    }
    // make sure the output of the property failed
    pObj = Aig_ManCo( p, pCex->iPo );
    return Saig_ManSimInfo2Get( vSimInfo, pObj, pCex->iFrame );
}

static int Saig_ManSimInfo2And ( int  Value0, int  Value1  )

inlinestatic

Definition at line 102 of file absOldSim.c.

{
    if ( Value0 == SAIG_ZER_NEW || Value1 == SAIG_ZER_NEW )
        return SAIG_ZER_NEW;
    if ( Value0 == SAIG_ONE_NEW && Value1 == SAIG_ONE_NEW )
        return SAIG_ONE_NEW;
    assert( 0 );
    return 0;
}

static int Saig_ManSimInfo2Get ( Vec_Ptr_t *  vSimInfo, Aig_Obj_t *  pObj, int  iFrame  )

inlinestatic

Definition at line 112 of file absOldSim.c.

{
    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
    return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1));
}

static int Saig_ManSimInfo2IsOld ( int  Value )

inlinestatic

Definition at line 73 of file absOldSim.c.

{
    return Value == SAIG_ZER_OLD || Value == SAIG_ONE_OLD;
}

static int Saig_ManSimInfo2Not ( int  Value )

inlinestatic

Definition at line 88 of file absOldSim.c.

{
    if ( Value == SAIG_ZER_NEW )
        return SAIG_ONE_NEW;
    if ( Value == SAIG_ONE_NEW )
        return SAIG_ZER_NEW;
    if ( Value == SAIG_ZER_OLD )
        return SAIG_ONE_OLD;
    if ( Value == SAIG_ONE_OLD )
        return SAIG_ZER_OLD;
    assert( 0 );
    return 0;
}

static void Saig_ManSimInfo2Set ( Vec_Ptr_t *  vSimInfo, Aig_Obj_t *  pObj, int  iFrame, int  Value  )

inlinestatic

Definition at line 118 of file absOldSim.c.

{
    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
    Value ^= Saig_ManSimInfo2Get( vSimInfo, pObj, iFrame );
    pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1));
}

static int Saig_ManSimInfo2SetOld ( int  Value )

inlinestatic

Definition at line 78 of file absOldSim.c.

{
    if ( Value == SAIG_ZER_NEW )
        return SAIG_ZER_OLD;
    if ( Value == SAIG_ONE_NEW )
        return SAIG_ONE_OLD;
    assert( 0 );
    return 0;
}

static int Saig_ManSimInfoAnd ( int  Value0, int  Value1  )

inlinestatic

Definition at line 43 of file absOldSim.c.

{
    if ( Value0 == SAIG_ZER || Value1 == SAIG_ZER )
        return SAIG_ZER;
    if ( Value0 == SAIG_ONE && Value1 == SAIG_ONE )
        return SAIG_ONE;
    return SAIG_UND;
}

static int Saig_ManSimInfoGet ( Vec_Ptr_t *  vSimInfo, Aig_Obj_t *  pObj, int  iFrame  )

inlinestatic

Definition at line 52 of file absOldSim.c.

{
    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
    return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1));
}

static int Saig_ManSimInfoNot ( int  Value )

inlinestatic

Definition at line 34 of file absOldSim.c.

{
    if ( Value == SAIG_ZER )
        return SAIG_ONE;
    if ( Value == SAIG_ONE )
        return SAIG_ZER;
    return SAIG_UND;
}

static void Saig_ManSimInfoSet ( Vec_Ptr_t *  vSimInfo, Aig_Obj_t *  pObj, int  iFrame, int  Value  )

inlinestatic

Definition at line 58 of file absOldSim.c.

{
    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
    assert( Value >= SAIG_ZER && Value <= SAIG_UND );
    Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
    pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1));
}