dchSimSat.c File Reference

#include "dchInt.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Dch_ManCollectTfoCands_rec (Dch_Man_t *p, Aig_Obj_t *pObj)
	DECLARATIONS ///. More...
void	Dch_ManCollectTfoCands (Dch_Man_t *p, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2)
void	Dch_ManResimulateSolved_rec (Dch_Man_t *p, Aig_Obj_t *pObj)
void	Dch_ManResimulateOther_rec (Dch_Man_t *p, Aig_Obj_t *pObj)
void	Dch_ManResimulateCex (Dch_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
void	Dch_ManResimulateCex2 (Dch_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)

Function Documentation

void Dch_ManCollectTfoCands	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj1,
		Aig_Obj_t *	pObj2
	)

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

Synopsis [Collect equivalence classes and const1 cands in the TFO.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file dchSimSat.c.

{
    Aig_Obj_t * pObj;
    int i;
    Vec_PtrClear( p->vSimRoots );
    Vec_PtrClear( p->vSimClasses );
    Aig_ManIncrementTravId( p->pAigTotal );
    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );    
    Dch_ManCollectTfoCands_rec( p, pObj1 );
    Dch_ManCollectTfoCands_rec( p, pObj2 );
    Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease );
    Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i )
        pObj->fMarkA = 0;
}

ABC_NAMESPACE_IMPL_START void Dch_ManCollectTfoCands_rec	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj
	)

DECLARATIONS ///.

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

FileName [dchSimSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Choice computation for tech-mapping.]

Synopsis [Performs resimulation using counter-examples.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 29, 2008.]

Revision [

Id:

dchSimSat.c,v 1.00 2008/07/29 00:00:00 alanmi Exp

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

Synopsis [Collects internal nodes in the reverse DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file dchSimSat.c.

{
    Aig_Obj_t * pFanout, * pRepr;
    int iFanout = -1, i;
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
    // traverse the fanouts
    Aig_ObjForEachFanout( p->pAigTotal, pObj, pFanout, iFanout, i )
        Dch_ManCollectTfoCands_rec( p, pFanout );
    // check if the given node has a representative
    pRepr = Aig_ObjRepr( p->pAigTotal, pObj );
    if ( pRepr == NULL )
        return;
    // pRepr is the constant 1 node
    if ( pRepr == Aig_ManConst1(p->pAigTotal) )
    {
        Vec_PtrPush( p->vSimRoots, pObj );
        return;
    }
    // pRepr is the representative of an equivalence class
    if ( pRepr->fMarkA )
        return;
    pRepr->fMarkA = 1;
    Vec_PtrPush( p->vSimClasses, pRepr );
}

void Dch_ManResimulateCex	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj,
		Aig_Obj_t *	pRepr
	)

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file dchSimSat.c.

{
    Aig_Obj_t * pRoot, ** ppClass;
    int i, k, nSize, RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    // get the equivalence classes
    Dch_ManCollectTfoCands( p, pObj, pRepr );
    // resimulate the cone of influence of the solved nodes
    p->nConeThis = 0;
    Aig_ManIncrementTravId( p->pAigTotal );
    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
    Dch_ManResimulateSolved_rec( p, pObj );
    Dch_ManResimulateSolved_rec( p, pRepr );
    p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
    // resimulate the cone of influence of the other nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
        Dch_ManResimulateOther_rec( p, pRoot );
    // refine these nodes
    RetValue1 = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
    // resimulate the cone of influence of the cand classes
    RetValue2 = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pRoot, i )
    {
        ppClass = Dch_ClassesReadClass( p->ppClasses, pRoot, &nSize );
        for ( k = 0; k < nSize; k++ )
            Dch_ManResimulateOther_rec( p, ppClass[k] );
        // refine this class
        RetValue2 += Dch_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
    }
    // make sure refinement happened
    if ( Aig_ObjIsConst1(pRepr) )
        assert( RetValue1 );
    else
        assert( RetValue2 );
p->timeSimSat += Abc_Clock() - clk;
}

void Dch_ManResimulateCex2	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj,
		Aig_Obj_t *	pRepr
	)

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file dchSimSat.c.

{
    Aig_Obj_t * pRoot;
    int i, RetValue;
    abctime clk = Abc_Clock();
    // get the equivalence class
    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
        Dch_ClassesCollectConst1Group( p->ppClasses, pObj, 500, p->vSimRoots );
    else
        Dch_ClassesCollectOneClass( p->ppClasses, pRepr, p->vSimRoots );
    // resimulate the cone of influence of the solved nodes
    p->nConeThis = 0;
    Aig_ManIncrementTravId( p->pAigTotal );
    Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
    Dch_ManResimulateSolved_rec( p, pObj );
    Dch_ManResimulateSolved_rec( p, pRepr );
    p->nConeMax = Abc_MaxInt( p->nConeMax, p->nConeThis );
    // resimulate the cone of influence of the other nodes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimRoots, pRoot, i )
        Dch_ManResimulateOther_rec( p, pRoot );
    // refine this class
    if ( Dch_ObjIsConst1Cand(p->pAigTotal, pObj) )
        RetValue = Dch_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
    else
        RetValue = Dch_ClassesRefineOneClass( p->ppClasses, pRepr, 0 );
    assert( RetValue );
p->timeSimSat += Abc_Clock() - clk;
}

void Dch_ManResimulateOther_rec	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Resimulates the cone of influence of the other nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file dchSimSat.c.

{
    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        // set random value
        pObj->fMarkB = Aig_ManRandom(0) & 1;
        return;
    }
    Dch_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
    Dch_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
}

void Dch_ManResimulateSolved_rec	(	Dch_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Resimulates the cone of influence of the solved nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file dchSimSat.c.

{
    if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        Aig_Obj_t * pObjFraig;
        int nVarNum;
        pObjFraig = Dch_ObjFraig( pObj );
        assert( !Aig_IsComplement(pObjFraig) );
        nVarNum = Dch_ObjSatNum( p, pObjFraig );
        // get the value from the SAT solver
        // (account for the fact that some vars may be minimized away)
        pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
//        pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
        return;
    }
    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
    Dch_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj) );
    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
    // count the cone size
    if ( Dch_ObjSatNum( p, Aig_Regular(Dch_ObjFraig(pObj)) ) > 0 )
        p->nConeThis++;
}