cecChoice.c File Reference

#include "cecInt.h"
#include "aig/gia/giaAig.h"
#include "proof/dch/dch.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START void	Cec_ManCombSpecReduce_rec (Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
	DECLARATIONS ///. More...
int	Cec_ManResimulateCounterExamplesComb (Cec_ManSim_t *pSim, Vec_Int_t *vCexStore)
int	Gia_ManCheckRefinements (Gia_Man_t *p, Vec_Str_t *vStatus, Vec_Int_t *vOutputs, Cec_ManSim_t *pSim, int fRings)
static int	Cec_ManCombSpecReal (Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
	FUNCTION DEFINITIONS ///. More...
Gia_Man_t *	Cec_ManCombSpecReduce (Gia_Man_t *p, Vec_Int_t **pvOutputs, int fRings)
int	Cec_ManChoiceComputation_int (Gia_Man_t *pAig, Cec_ParChc_t *pPars)
Gia_Man_t *	Cec_ManChoiceComputationVec (Gia_Man_t *pGia, int nGias, Cec_ParChc_t *pPars)
Gia_Man_t *	Cec_ManChoiceComputation (Gia_Man_t *pAig, Cec_ParChc_t *pParsChc)
Aig_Man_t *	Cec_ComputeChoices (Gia_Man_t *pGia, Dch_Pars_t *pPars)

Function Documentation

Aig_Man_t* Cec_ComputeChoices	(	Gia_Man_t *	pGia,
		Dch_Pars_t *	pPars
	)

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

Synopsis [Performs computation of AIGs with choices.]

Description [Takes several AIGs and performs choicing.]

SideEffects []

SeeAlso []

Definition at line 385 of file cecChoice.c.

{
    Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
    Aig_Man_t * pAig;
    if ( pPars->fVerbose )
        Abc_PrintTime( 1, "Synthesis time", pPars->timeSynth );
    Cec_ManChcSetDefaultParams( pParsChc );
    pParsChc->nBTLimit = pPars->nBTLimit;
    pParsChc->fUseCSat = pPars->fUseCSat;
    if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
        pParsChc->nBTLimit = 100;
    pParsChc->fVerbose = pPars->fVerbose;
    pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc );
    Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
    pAig = Gia_ManToAig( pGia, 1 );
    Gia_ManStop( pGia );
    return pAig;
}

Gia_Man_t* Cec_ManChoiceComputation	(	Gia_Man_t *	pAig,
		Cec_ParChc_t *	pParsChc
	)

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

Synopsis [Computes choices for one AIGs.]

Description []

SideEffects []

SeeAlso []

Definition at line 348 of file cecChoice.c.

{
//    extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
    Dch_Pars_t Pars, * pPars = &Pars;
    Aig_Man_t * pMan, * pManNew;
    Gia_Man_t * pGia;
    if ( 0 ) 
    {
        pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc );
    }
    else
    {
        pMan = Gia_ManToAig( pAig, 0 );
        Dch_ManSetDefaultParams( pPars );
        pPars->fUseGia  = 1;
        pPars->nBTLimit = pParsChc->nBTLimit;
        pPars->fUseCSat = pParsChc->fUseCSat;
        pPars->fVerbose = pParsChc->fVerbose;
        pManNew = Dar_ManChoiceNew( pMan, pPars );
        pGia = Gia_ManFromAig( pManNew );
        Aig_ManStop( pManNew );
//        Aig_ManStop( pMan );
    }
    return pGia;
}

int Cec_ManChoiceComputation_int	(	Gia_Man_t *	pAig,
		Cec_ParChc_t *	pPars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 201 of file cecChoice.c.

{
    int nItersMax = 1000;
    Vec_Str_t * vStatus;
    Vec_Int_t * vOutputs;
    Vec_Int_t * vCexStore;
    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
    Cec_ManSim_t * pSim;
    Gia_Man_t * pSrm;
    int r, RetValue;
    abctime clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = Abc_Clock();
    abctime clk2, clk = Abc_Clock();
    ABC_FREE( pAig->pReprs );
    ABC_FREE( pAig->pNexts );
    Gia_ManRandom( 1 );
    // prepare simulation manager
    Cec_ManSimSetDefaultParams( pParsSim );
    pParsSim->nWords     = pPars->nWords;
    pParsSim->nFrames    = pPars->nRounds;
    pParsSim->fVerbose   = pPars->fVerbose;
    pParsSim->fLatchCorr   = 0;
    pParsSim->fSeqSimulate = 0;
    // create equivalence classes of registers
    pSim = Cec_ManSimStart( pAig, pParsSim );
    Cec_ManSimClassesPrepare( pSim, -1 );
    Cec_ManSimClassesRefine( pSim );
    // prepare SAT solving
    Cec_ManSatSetDefaultParams( pParsSat );
    pParsSat->nBTLimit = pPars->nBTLimit;
    pParsSat->fVerbose = pPars->fVerbose;
    if ( pPars->fVerbose )
    {
        Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
            Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
    }
    // perform refinement of equivalence classes
    for ( r = 0; r < nItersMax; r++ )
    { 
        clk = Abc_Clock();
        // perform speculative reduction
        clk2 = Abc_Clock();
        pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );
        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );
        clkSrm += Abc_Clock() - clk2;
        if ( Gia_ManCoNum(pSrm) == 0 )
        {
            if ( pPars->fVerbose )
                Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );
            Vec_IntFree( vOutputs );
            Gia_ManStop( pSrm );            
            break;
        }
//Gia_DumpAiger( pSrm, "choicesrm", r, 2 );
        // found counter-examples to speculation
        clk2 = Abc_Clock();
        if ( pPars->fUseCSat )
            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
        else
            vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
        Gia_ManStop( pSrm );
        clkSat += Abc_Clock() - clk2;
        if ( Vec_IntSize(vCexStore) == 0 )
        {
            if ( pPars->fVerbose )
                Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
            Vec_IntFree( vCexStore );
            Vec_StrFree( vStatus );
            Vec_IntFree( vOutputs );
            break;
        }
        // refine classes with these counter-examples
        clk2 = Abc_Clock();
        RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );
        Vec_IntFree( vCexStore );
        clkSim += Abc_Clock() - clk2;
        Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
        if ( pPars->fVerbose )
            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
        Vec_StrFree( vStatus );
        Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
    }
    // check the overflow
    if ( r == nItersMax )
        Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
    Cec_ManSimStop( pSim );
    clkTotal = Abc_Clock() - clkTotal;
    // report the results
    if ( pPars->fVerbose )
    {
        Abc_PrintTimeP( 1, "Srm  ", clkSrm,                        clkTotal );
        Abc_PrintTimeP( 1, "Sat  ", clkSat,                        clkTotal );
        Abc_PrintTimeP( 1, "Sim  ", clkSim,                        clkTotal );
        Abc_PrintTimeP( 1, "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
        Abc_PrintTime( 1, "TOTAL",  clkTotal );
    }
    return 0;
}

Gia_Man_t* Cec_ManChoiceComputationVec	(	Gia_Man_t *	pGia,
		int	nGias,
		Cec_ParChc_t *	pPars
	)

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

Synopsis [Computes choices for the vector of AIGs.]

Description []

SideEffects []

SeeAlso []

Definition at line 313 of file cecChoice.c.

{
    Gia_Man_t * pNew;
    int RetValue;
    // compute equivalences of the miter
//    pMiter = Gia_ManChoiceMiter( vGias );
//    Gia_ManSetRegNum( pMiter, 0 );
    RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
    // derive AIG with choices
    pNew = Gia_ManEquivToChoices( pGia, nGias );
//    Gia_ManHasChoices_very_old( pNew );
//    Gia_ManStop( pMiter );
    // report the results
    if ( pPars->fVerbose )
    {
//        Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
//            Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), 
//            100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), 
//            Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 
//            100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
    }
    return pNew;
}

static int Cec_ManCombSpecReal ( Gia_Man_t *  pNew, Gia_Man_t *  p, Gia_Obj_t *  pObj  )

inlinestatic

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes the real value of the literal w/o spec reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file cecChoice.c.

{
    assert( Gia_ObjIsAnd(pObj) );
    Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
    Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
    return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}

Gia_Man_t* Cec_ManCombSpecReduce	(	Gia_Man_t *	p,
		Vec_Int_t **	pvOutputs,
		int	fRings
	)

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

Synopsis [Derives SRM for signal correspondence.]

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file cecChoice.c.

{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pRepr;
    Vec_Int_t * vXorLits;
    int i, iPrev, iObj, iPrevNew, iObjNew;
    assert( p->pReprs != NULL );
    Gia_ManSetPhase( p );
    Gia_ManFillValue( p );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManHashAlloc( pNew );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachCi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    *pvOutputs = Vec_IntAlloc( 1000 );
    vXorLits = Vec_IntAlloc( 1000 );
    if ( fRings )
    {
        Gia_ManForEachObj1( p, pObj, i )
        {
            if ( Gia_ObjIsConst( p, i ) )
            {
                iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
                iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
                if ( iObjNew != 0 )
                {
                    Vec_IntPush( *pvOutputs, 0 );
                    Vec_IntPush( *pvOutputs, i );
                    Vec_IntPush( vXorLits, iObjNew );
                }
            }
            else if ( Gia_ObjIsHead( p, i ) )
            {
                iPrev = i;
                Gia_ClassForEachObj1( p, i, iObj )
                {
                    iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
                    iObjNew  = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
                    iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
                    iObjNew  = Abc_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
                    if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
                    {
                        Vec_IntPush( *pvOutputs, iPrev );
                        Vec_IntPush( *pvOutputs, iObj );
                        Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
                    }
                    iPrev = iObj;
                }
                iObj = i;
                iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
                iObjNew  = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
                iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
                iObjNew  = Abc_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
                if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
                {
                    Vec_IntPush( *pvOutputs, iPrev );
                    Vec_IntPush( *pvOutputs, iObj );
                    Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
                }
            }
        }
    }
    else
    {
        Gia_ManForEachObj1( p, pObj, i )
        {
            pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
            if ( pRepr == NULL )
                continue;
            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Cec_ManCombSpecReal( pNew, p, pRepr );
            iObjNew  = Cec_ManCombSpecReal( pNew, p, pObj );
            iObjNew  = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
            if ( iPrevNew != iObjNew )
            {
                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
                Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
            }
        }
    }
    Vec_IntForEachEntry( vXorLits, iObjNew, i )
        Gia_ManAppendCo( pNew, iObjNew );
    Vec_IntFree( vXorLits );
    Gia_ManHashStop( pNew );
//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
    pNew = Gia_ManCleanup( pTemp = pNew );
//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
    Gia_ManStop( pTemp );
    return pNew;
}

void Cec_ManCombSpecReduce_rec ( Gia_Man_t *  pNew, Gia_Man_t *  p, Gia_Obj_t *  pObj  )

static

DECLARATIONS ///.

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

FileName [cecChoice.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Computation of structural choices.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

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

Synopsis [Recursively performs speculative reduction for the object.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file cecChoice.c.

{
    Gia_Obj_t * pRepr;
    if ( ~pObj->Value )
        return;
    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
    {
        Cec_ManCombSpecReduce_rec( pNew, p, pRepr );
        pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
        return;
    }
    pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj );
}

int Cec_ManResimulateCounterExamplesComb	(	Cec_ManSim_t *	pSim,
		Vec_Int_t *	vCexStore
	)

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

Synopsis [Resimulates counter-examples derived by the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 583 of file cecCorr.c.

{ 
    Vec_Ptr_t * vSimInfo; 
    int RetValue = 0, iStart = 0;
    Gia_ManCreateValueRefs( pSim->pAig );
    pSim->pPars->nFrames = 1;
    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
    while ( iStart < Vec_IntSize(vCexStore) )
    {
        Cec_ManStartSimInfo( vSimInfo, 0 );
        iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
        RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
    }
    assert( iStart == Vec_IntSize(vCexStore) );
    Vec_PtrFree( vSimInfo );
    return RetValue;
}

int Gia_ManCheckRefinements	(	Gia_Man_t *	p,
		Vec_Str_t *	vStatus,
		Vec_Int_t *	vOutputs,
		Cec_ManSim_t *	pSim,
		int	fRings
	)

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

Synopsis [Updates equivalence classes by marking those that timed out.]

Description [Returns 1 if all ndoes are proved.]

SideEffects []

SeeAlso []

Definition at line 612 of file cecCorr.c.

{
    int i, status, iRepr, iObj;
    int Counter = 0;
    assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
    Vec_StrForEachEntry( vStatus, status, i )
    {
        iRepr = Vec_IntEntry( vOutputs, 2*i );
        iObj  = Vec_IntEntry( vOutputs, 2*i+1 );
        if ( status == 1 )
            continue;
        if ( status == 0 )
        {
            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
                Counter++;
//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
//                Abc_Print( 1, "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
//                Cec_ManSimClassRemoveOne( pSim, iObj );
            continue;
        }
        if ( status == -1 )
        {
//            if ( !Gia_ObjFailed( p, iObj ) )
//                Abc_Print( 1, "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
//            Gia_ObjSetFailed( p, iRepr );
//            Gia_ObjSetFailed( p, iObj );        
//            if ( fRings )
//            Cec_ManSimClassRemoveOne( pSim, iRepr );
            Cec_ManSimClassRemoveOne( pSim, iObj );
            continue;
        }
    }
//    if ( Counter )
//    Abc_Print( 1, "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
    return 1;
}