cec.h File Reference

Go to the source code of this file.

Data Structures
struct	Cec_ParSat_t_
struct	Cec_ParSim_t_
struct	Cec_ParSmf_t_
struct	Cec_ParFra_t_
struct	Cec_ParCec_t_
struct	Cec_ParCor_t_
struct	Cec_ParChc_t_
struct	Cec_ParSeq_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_	Cec_ParSat_t
	INCLUDES ///. More...
typedef struct Cec_ParSim_t_	Cec_ParSim_t
typedef struct Cec_ParSmf_t_	Cec_ParSmf_t
typedef struct Cec_ParFra_t_	Cec_ParFra_t
typedef struct Cec_ParCec_t_	Cec_ParCec_t
typedef struct Cec_ParCor_t_	Cec_ParCor_t
typedef struct Cec_ParChc_t_	Cec_ParChc_t
typedef struct Cec_ParSeq_t_	Cec_ParSeq_t

Functions
int	Cec_ManVerify (Gia_Man_t *p, Cec_ParCec_t *pPars)
	MACRO DEFINITIONS ///. More...
int	Cec_ManVerifyTwo (Gia_Man_t *p0, Gia_Man_t *p1, int fVerbose)
Gia_Man_t *	Cec_ManChoiceComputation (Gia_Man_t *pAig, Cec_ParChc_t *pPars)
int	Cec_ManLSCorrespondenceClasses (Gia_Man_t *pAig, Cec_ParCor_t *pPars)
Gia_Man_t *	Cec_ManLSCorrespondence (Gia_Man_t *pAig, Cec_ParCor_t *pPars)
void	Cec_ManSatSetDefaultParams (Cec_ParSat_t *p)
	DECLARATIONS ///. More...
void	Cec_ManSimSetDefaultParams (Cec_ParSim_t *p)
void	Cec_ManSmfSetDefaultParams (Cec_ParSmf_t *p)
void	Cec_ManFraSetDefaultParams (Cec_ParFra_t *p)
void	Cec_ManCecSetDefaultParams (Cec_ParCec_t *p)
void	Cec_ManCorSetDefaultParams (Cec_ParCor_t *p)
void	Cec_ManChcSetDefaultParams (Cec_ParChc_t *p)
Gia_Man_t *	Cec_ManSatSweeping (Gia_Man_t *pAig, Cec_ParFra_t *pPars)
Gia_Man_t *	Cec_ManSatSolving (Gia_Man_t *pAig, Cec_ParSat_t *pPars)
void	Cec_ManSimulation (Gia_Man_t *pAig, Cec_ParSim_t *pPars)
int	Cec_ManSeqResimulateCounter (Gia_Man_t *pAig, Cec_ParSim_t *pPars, Abc_Cex_t *pCex)
int	Cec_ManSeqSemiformal (Gia_Man_t *pAig, Cec_ParSmf_t *pPars)
int	Cec_ManCheckNonTrivialCands (Gia_Man_t *pAig)
int	Cec_SeqReadMinDomSize (Cec_ParSeq_t *p)
int	Cec_SeqReadVerbose (Cec_ParSeq_t *p)
void	Cec_SeqSynthesisSetDefaultParams (Cec_ParSeq_t *pPars)
	DECLARATIONS ///. More...
int	Cec_SequentialSynthesisPart (Gia_Man_t *p, Cec_ParSeq_t *pPars)

Typedef Documentation

typedef struct Cec_ParCec_t_ Cec_ParCec_t

Definition at line 117 of file cec.h.

typedef struct Cec_ParChc_t_ Cec_ParChc_t

Definition at line 159 of file cec.h.

typedef struct Cec_ParCor_t_ Cec_ParCor_t

Definition at line 132 of file cec.h.

typedef struct Cec_ParFra_t_ Cec_ParFra_t

Definition at line 94 of file cec.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_ Cec_ParSat_t

INCLUDES ///.

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

FileName [cec.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

cec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 43 of file cec.h.

typedef struct Cec_ParSeq_t_ Cec_ParSeq_t

Definition at line 172 of file cec.h.

typedef struct Cec_ParSim_t_ Cec_ParSim_t

Definition at line 58 of file cec.h.

typedef struct Cec_ParSmf_t_ Cec_ParSmf_t

Definition at line 77 of file cec.h.

Function Documentation

void Cec_ManCecSetDefaultParams

(

Cec_ParCec_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file cecCore.c.

{
    memset( p, 0, sizeof(Cec_ParCec_t) );
    p->nBTLimit       =    1000;  // conflict limit at a node
    p->TimeLimit      =       0;  // the runtime limit in seconds
//    p->fFirstStop     =       0;  // stop on the first sat output
    p->fUseSmartCnf   =       0;  // use smart CNF computation
    p->fRewriting     =       0;  // enables AIG rewriting
    p->fVeryVerbose   =       0;  // verbose stats
    p->fVerbose       =       0;  // verbose stats
    p->iOutFail       =      -1;  // the number of failed output
}  

void Cec_ManChcSetDefaultParams

(

Cec_ParChc_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file cecCore.c.

{
    memset( p, 0, sizeof(Cec_ParChc_t) );
    p->nWords         =      15;  // the number of simulation words
    p->nRounds        =      15;  // the number of simulation rounds
    p->nBTLimit       =    1000;  // conflict limit at a node
    p->fUseRings      =       1;  // use rings
    p->fUseCSat       =       0;  // use circuit-based solver
    p->fVeryVerbose   =       0;  // verbose stats
    p->fVerbose       =       0;  // verbose stats
}  

int Cec_ManCheckNonTrivialCands

(

Gia_Man_t *

pAig

)

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

Synopsis [Returns the number of POs that are not const0 cands.]

Description []

SideEffects []

SeeAlso []

Definition at line 295 of file cecSeq.c.

{
    Gia_Obj_t * pObj;
    int i, RetValue = 0;
    if ( pAig->pReprs == NULL )
        return 0;
    // label internal nodes driving POs
    Gia_ManForEachPo( pAig, pObj, i )
        Gia_ObjFanin0(pObj)->fMark0 = 1;
    // check if there are non-labled equivs
    Gia_ManForEachObj( pAig, pObj, i )
        if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID )
        {
            RetValue = 1;
            break;
        }
    // clean internal nodes driving POs
    Gia_ManForEachPo( pAig, pObj, i )
        Gia_ObjFanin0(pObj)->fMark0 = 0;
    return RetValue;
}

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

void Cec_ManCorSetDefaultParams

(

Cec_ParCor_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file cecCore.c.

{
    memset( p, 0, sizeof(Cec_ParCor_t) );
    p->nWords         =      15;  // the number of simulation words
    p->nRounds        =      15;  // the number of simulation rounds
    p->nFrames        =       1;  // the number of time frames
    p->nBTLimit       =     100;  // conflict limit at a node
    p->nLevelMax      =      -1;  // (scorr only) the max number of levels
    p->nStepsMax      =      -1;  // (scorr only) the max number of induction steps
    p->fLatchCorr     =       0;  // consider only latch outputs
    p->fConstCorr     =       0;  // consider only constants
    p->fUseRings      =       1;  // combine classes into rings
    p->fUseCSat       =       1;  // use circuit-based solver
//    p->fFirstStop     =       0;  // stop on the first sat output
    p->fUseSmartCnf   =       0;  // use smart CNF computation
    p->fVeryVerbose   =       0;  // verbose stats
    p->fVerbose       =       0;  // verbose stats
}  

void Cec_ManFraSetDefaultParams

(

Cec_ParFra_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 125 of file cecCore.c.

{
    memset( p, 0, sizeof(Cec_ParFra_t) );
    p->nWords         =      15;  // the number of simulation words
    p->nRounds        =      15;  // the number of simulation rounds
    p->TimeLimit      =       0;  // the runtime limit in seconds
    p->nItersMax      =      10;  // the maximum number of iterations of SAT sweeping
    p->nBTLimit       =     100;  // conflict limit at a node
    p->nLevelMax      =       0;  // restriction on the level of nodes to be swept
    p->nDepthMax      =       1;  // the depth in terms of steps of speculative reduction
    p->fRewriting     =       0;  // enables AIG rewriting
    p->fCheckMiter    =       0;  // the circuit is the miter
//    p->fFirstStop     =       0;  // stop on the first sat output
    p->fDualOut       =       0;  // miter with separate outputs
    p->fColorDiff     =       0;  // miter with separate outputs
    p->fSatSweeping   =       0;  // enable SAT sweeping
    p->fVeryVerbose   =       0;  // verbose stats
    p->fVerbose       =       0;  // verbose stats
    p->iOutFail       =      -1;  // the failed output
} 

Gia_Man_t* Cec_ManLSCorrespondence	(	Gia_Man_t *	pAig,
		Cec_ParCor_t *	pPars
	)

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

Synopsis [Top-level procedure for register correspondence.]

Description []

SideEffects []

SeeAlso []

Definition at line 1147 of file cecCorr.c.

{  
    Gia_Man_t * pNew, * pTemp;
    unsigned * pInitState;
    int RetValue;
    ABC_FREE( pAig->pReprs );
    ABC_FREE( pAig->pNexts );
    if ( pPars->nPrefix == 0 )
    {
        RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
        if ( RetValue == 0 )
            return Gia_ManDup( pAig );
    }
    else
    {
        // compute the cycles AIG
        pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix );
        pTemp = Gia_ManDupFlip( pAig, (int *)pInitState );
        ABC_FREE( pInitState );
        // compute classes of this AIG
        RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
        // transfer the class info
        pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
        pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
        // perform additional BMC
        pPars->fUseCSat = 0;
        pPars->nBTLimit = Abc_MaxInt( pPars->nBTLimit, 1000 );
        Cec_ManLSCorrespondenceBmc( pAig, pPars, pPars->nPrefix );
/*
        // transfer the class info back
        pTemp->pReprs = pAig->pReprs; pAig->pReprs = NULL;
        pTemp->pNexts = pAig->pNexts; pAig->pNexts = NULL;
        // continue refining
        RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
        // transfer the class info
        pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
        pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
*/
        Gia_ManStop( pTemp );
    }
    // derive reduced AIG
    if ( pPars->fMakeChoices )
    {
        pNew = Gia_ManEquivToChoices( pAig, 1 );
//        Gia_ManHasChoices_very_old( pNew );
    }
    else
    {
//        Gia_ManEquivImprove( pAig );
        pNew = Gia_ManCorrReduce( pAig );
        pNew = Gia_ManSeqCleanup( pTemp = pNew );
        Gia_ManStop( pTemp );
        //Gia_AigerWrite( pNew, "reduced.aig", 0, 0 );
    }
    // 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) );
    }
    if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
        Abc_Print( 1, "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
    // print verbose info about equivalences
    if ( pPars->fVerboseFlops )
    {
        if ( pAig->vNamesIn == NULL )
            Abc_Print( 1, "Flop output names are not available. Use command \"&get -n\".\n" );
        else
            Cec_ManPrintFlopEquivs( pAig );
    }
    return pNew;
}

int Cec_ManLSCorrespondenceClasses	(	Gia_Man_t *	pAig,
		Cec_ParCor_t *	pPars
	)

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

Synopsis [Internal procedure for register correspondence.]

Description []

SideEffects []

SeeAlso []

Definition at line 909 of file cecCorr.c.

{  
    int nIterMax     = 100000;
    int nAddFrames   = 1; // additional timeframes to simulate
    int fRunBmcFirst = 1;
    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 clkTotal = Abc_Clock();
    abctime clkSat = 0, clkSim = 0, clkSrm = 0;
    abctime clk2, clk = Abc_Clock();
    if ( Gia_ManRegNum(pAig) == 0 )
    {
        Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
        return 0;
    }
    Gia_ManRandom( 1 );
    // prepare simulation manager
    Cec_ManSimSetDefaultParams( pParsSim );
    pParsSim->nWords     = pPars->nWords;
    pParsSim->nFrames    = pPars->nFrames;
    pParsSim->fVerbose   = pPars->fVerbose;
    pParsSim->fLatchCorr = pPars->fLatchCorr;
    pParsSim->fConstCorr = pPars->fConstCorr;
    pParsSim->fSeqSimulate = 1;
    // create equivalence classes of registers
    pSim = Cec_ManSimStart( pAig, pParsSim );
    if ( pAig->pReprs == NULL )
    {
        Cec_ManSimClassesPrepare( pSim, pPars->nLevelMax );
        Cec_ManSimClassesRefine( pSim );
    }
    // prepare SAT solving
    Cec_ManSatSetDefaultParams( pParsSat );
    pParsSat->nBTLimit = pPars->nBTLimit;
    pParsSat->fVerbose = pPars->fVerbose;
    // limit the number of conflicts in the circuit-based solver
    if ( pPars->fUseCSat )
        pParsSat->nBTLimit = Abc_MinInt( pParsSat->nBTLimit, 1000 );
    if ( pPars->fVerbose )
    {
        Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
            Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), 
            pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
    }
    // check the base case
    if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
        Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
    if ( pPars->pFunc )
    {
        ((int (*)(void *))pPars->pFunc)( pPars->pData );
        ((int (*)(void *))pPars->pFunc)( pPars->pData );
    }
    if ( pPars->nStepsMax == 0 )
    {
        Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
        Cec_ManSimStop( pSim );
        return 1;
    }
    // perform refinement of equivalence classes
    for ( r = 0; r < nIterMax; r++ )
    { 
        if ( pPars->nStepsMax == r )
        {
            Cec_ManSimStop( pSim );
            Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
            return 1;
        }
        clk = Abc_Clock();
        // perform speculative reduction
        clk2 = Abc_Clock();
        pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
        clkSrm += Abc_Clock() - clk2;
        if ( Gia_ManCoNum(pSrm) == 0 )
        {
            Vec_IntFree( vOutputs );
            Gia_ManStop( pSrm );            
            break;
        }
//Gia_DumpAiger( pSrm, "corrsrm", 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 )
        {
            Vec_IntFree( vCexStore );
            Vec_StrFree( vStatus );
            Vec_IntFree( vOutputs );
            break;
        }
//        Cec_ManLSCorrAnalyzeDependence( pAig, vOutputs, vStatus );        

        // refine classes with these counter-examples
        clk2 = Abc_Clock();
        RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
        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 );
        if ( pPars->pFunc )
            ((int (*)(void *))pPars->pFunc)( pPars->pData );
        // quit if const is no longer there
        if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) )
        {
            printf( "Iterative refinement is stopped after iteration %d\n", r );
            printf( "because the property output is no longer a candidate constant.\n" );
            Cec_ManSimStop( pSim );
            return 0;
        }
    }
    if ( pPars->fVerbose )
        Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );
    // check the overflow
    if ( r == nIterMax )
        Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
    Cec_ManSimStop( pSim );
    // check the base case
    if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
        Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
    clkTotal = Abc_Clock() - clkTotal;
    // report the results
    if ( pPars->fVerbose )
    {
        ABC_PRTP( "Srm  ", clkSrm,                        clkTotal );
        ABC_PRTP( "Sat  ", clkSat,                        clkTotal );
        ABC_PRTP( "Sim  ", clkSim,                        clkTotal );
        ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
        Abc_PrintTime( 1, "TOTAL",  clkTotal );
    }
    return 1;
}    

void Cec_ManSatSetDefaultParams

(

Cec_ParSat_t *

p

)

DECLARATIONS ///.

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

FileName [cecCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file cecCore.c.

{
    memset( p, 0, sizeof(Cec_ParSat_t) );
    p->nBTLimit       =     100;  // conflict limit at a node
    p->nSatVarMax     =    2000;  // the max number of SAT variables
    p->nCallsRecycle  =     200;  // calls to perform before recycling SAT solver
    p->fNonChrono     =       0;  // use non-chronological backtracling (for circuit SAT only)
    p->fPolarFlip     =       1;  // flops polarity of variables
    p->fCheckMiter    =       0;  // the circuit is the miter
//    p->fFirstStop     =       0;  // stop on the first sat output
    p->fLearnCls      =       0;  // perform clause learning
    p->fVerbose       =       0;  // verbose stats
}  

Gia_Man_t* Cec_ManSatSolving	(	Gia_Man_t *	pAig,
		Cec_ParSat_t *	pPars
	)

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

Synopsis [Core procedure for SAT sweeping.]

Description []

SideEffects []

SeeAlso []

Definition at line 234 of file cecCore.c.

{
    Gia_Man_t * pNew;
    Cec_ManPat_t * pPat;
    pPat = Cec_ManPatStart();
    Cec_ManSatSolve( pPat, pAig, pPars );
//    pNew = Gia_ManDupDfsSkip( pAig );
    pNew = Gia_ManDup( pAig );
    Cec_ManPatStop( pPat );
    return pNew;
}

Gia_Man_t* Cec_ManSatSweeping	(	Gia_Man_t *	pAig,
		Cec_ParFra_t *	pPars
	)

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

Synopsis [Core procedure for SAT sweeping.]

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file cecCore.c.

{
    int fOutputResult = 0;
    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
    Gia_Man_t * pIni, * pSrm, * pTemp;
    Cec_ManFra_t * p;
    Cec_ManSim_t * pSim;
    Cec_ManPat_t * pPat;
    int i, fTimeOut = 0, nMatches = 0;
    abctime clk, clk2, clkTotal = Abc_Clock();

    // duplicate AIG and transfer equivalence classes
    Gia_ManRandom( 1 );
    pIni = Gia_ManDup(pAig);
    pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
    pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;

    // prepare the managers
    // SAT sweeping
    p = Cec_ManFraStart( pIni, pPars );
    if ( pPars->fDualOut )
        pPars->fColorDiff = 1;
    // simulation
    Cec_ManSimSetDefaultParams( pParsSim );
    pParsSim->nWords      = pPars->nWords;
    pParsSim->nFrames     = pPars->nRounds;
    pParsSim->fCheckMiter = pPars->fCheckMiter;
    pParsSim->fDualOut    = pPars->fDualOut;
    pParsSim->fVerbose    = pPars->fVerbose;
    pSim = Cec_ManSimStart( p->pAig, pParsSim );
    // SAT solving
    Cec_ManSatSetDefaultParams( pParsSat );
    pParsSat->nBTLimit = pPars->nBTLimit;
    pParsSat->fVerbose = pPars->fVeryVerbose;
    // simulation patterns
    pPat = Cec_ManPatStart();
    pPat->fVerbose = pPars->fVeryVerbose;

    // start equivalence classes
clk = Abc_Clock();
    if ( p->pAig->pReprs == NULL )
    {
        if ( Cec_ManSimClassesPrepare(pSim, -1) || Cec_ManSimClassesRefine(pSim) )
        {
            Gia_ManStop( p->pAig );
            p->pAig = NULL;
            goto finalize;
        }
    }
p->timeSim += Abc_Clock() - clk;
    // perform solving
    for ( i = 1; i <= pPars->nItersMax; i++ )
    {
        clk2 = Abc_Clock();
        nMatches = 0;
        if ( pPars->fDualOut )
        {
            nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose );
//            p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig );
//            Gia_ManEquivTransform( p->pAig, 1 );
        }
        pSrm = Cec_ManFraSpecReduction( p ); 

//        Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );

        if ( pPars->fVeryVerbose )
            Gia_ManPrintStats( pSrm, NULL );
        if ( Gia_ManCoNum(pSrm) == 0 )
        {
            Gia_ManStop( pSrm );
            if ( p->pPars->fVerbose )
                Abc_Print( 1, "Considered all available candidate equivalences.\n" );
            if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 )
            {
                if ( pPars->fColorDiff )
                {
                    if ( p->pPars->fVerbose )
                        Abc_Print( 1, "Switching into reduced mode.\n" );
                    pPars->fColorDiff = 0;
                }
                else
                {
                    if ( p->pPars->fVerbose )
                        Abc_Print( 1, "Switching into normal mode.\n" );
                    pPars->fDualOut = 0;
                }
                continue;
            }
            break;
        }
clk = Abc_Clock();
        if ( pPars->fRunCSat )
            Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); 
        else
            Cec_ManSatSolve( pPat, pSrm, pParsSat ); 
p->timeSat += Abc_Clock() - clk;
        if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
        {
            Gia_ManStop( pSrm );
            Gia_ManStop( p->pAig );
            p->pAig = NULL;
            goto finalize;
        }
        Gia_ManStop( pSrm );

        // update the manager
        pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut );
        if ( p->pAig == NULL )
        {
            p->pAig = pTemp;
            break;
        }
        Gia_ManStop( pTemp );
        if ( p->pPars->fVerbose )
        {
            Abc_Print( 1, "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", 
                i, p->nAllProved, p->nAllDisproved, p->nAllFailed, nMatches, Gia_ManAndNum(p->pAig) );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
        }
        if ( Gia_ManAndNum(p->pAig) == 0 )
        {
            if ( p->pPars->fVerbose )
                Abc_Print( 1, "Network after reduction is empty.\n" );
            break;
        }
        // check resource limits
        if ( p->pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
        {
            fTimeOut = 1;
            break;
        }
//        if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved )
        if ( p->nAllFailed > p->nAllProved + p->nAllDisproved )
        {
            if ( pParsSat->nBTLimit >= 10001 )
                break;
            if ( pPars->fSatSweeping )
            {
                if ( p->pPars->fVerbose )
                    Abc_Print( 1, "Exceeded the limit on the number of conflicts (%d).\n", pParsSat->nBTLimit );
                break;
            }
            pParsSat->nBTLimit *= 10;
            if ( p->pPars->fVerbose )
            {
                if ( p->pPars->fVerbose )
                    Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
                if ( fOutputResult )
                {
                    Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 );
                    Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
                }
            }
        }
        if ( pPars->fDualOut && pPars->fColorDiff && (Gia_ManAndNum(p->pAig) < 100000 || p->nAllProved + p->nAllDisproved < 10) )
        {
            if ( p->pPars->fVerbose )
                Abc_Print( 1, "Switching into reduced mode.\n" );
            pPars->fColorDiff = 0;
        }
//        if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
        else if ( pPars->fDualOut && (Gia_ManAndNum(p->pAig) < 20000 || p->nAllProved + p->nAllDisproved < 10) )
        {
            if ( p->pPars->fVerbose )
                Abc_Print( 1, "Switching into normal mode.\n" );
            pPars->fColorDiff = 0;
            pPars->fDualOut = 0;
        }
    }
finalize:
    if ( p->pPars->fVerbose && p->pAig )
    {
        Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
            Gia_ManAndNum(pAig), Gia_ManAndNum(p->pAig), 
            100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(p->pAig))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), 
            Gia_ManRegNum(pAig), Gia_ManRegNum(p->pAig), 
            100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(p->pAig))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
        Abc_PrintTimeP( 1, "Sim ", p->timeSim, Abc_Clock() - (int)clkTotal );
        Abc_PrintTimeP( 1, "Sat ", p->timeSat-pPat->timeTotalSave, Abc_Clock() - (int)clkTotal );
        Abc_PrintTimeP( 1, "Pat ", p->timePat+pPat->timeTotalSave, Abc_Clock() - (int)clkTotal );
        Abc_PrintTime( 1, "Time", (int)(Abc_Clock() - clkTotal) );
    }

    pTemp = p->pAig; p->pAig = NULL;
    if ( pTemp == NULL && pSim->iOut >= 0 )
    {
        Abc_Print( 1, "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
        pPars->iOutFail = pSim->iOut;
    }
    else if ( pSim->pCexes )
        Abc_Print( 1, "Disproved %d outputs of the miter.\n", pSim->nOuts );
    if ( fTimeOut )
        Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );

    pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL;
    Cec_ManSimStop( pSim );
    Cec_ManPatStop( pPat );
    Cec_ManFraStop( p );
    return pTemp;
}

int Cec_ManSeqResimulateCounter	(	Gia_Man_t *	pAig,
		Cec_ParSim_t *	pPars,
		Abc_Cex_t *	pCex
	)

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

Synopsis [Resimuates one counter-example to refine equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 215 of file cecSeq.c.

{
    Vec_Ptr_t * vSimInfo;
    int RetValue;
    abctime clkTotal = Abc_Clock();
    if ( pCex == NULL )
    {
        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
        return -1;
    }
    if ( pAig->pReprs == NULL )
    {
        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" );
        return -1;
    }
    if ( Gia_ManRegNum(pAig) == 0 )
    {
        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
        return -1;
    }
//    if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
    if ( Gia_ManPiNum(pAig) != pCex->nPis )
    {
        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" );
        return -1;
    }
    if ( pPars->fVerbose )
        Abc_Print( 1, "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 );
    Gia_ManRandom( 1 );
    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
        Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 );
    Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
    if ( pPars->fVerbose )
        Gia_ManEquivPrintClasses( pAig, 0, 0 );
    RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL, pPars->fCheckMiter );
    if ( pPars->fVerbose )
        Gia_ManEquivPrintClasses( pAig, 0, 0 );
    Vec_PtrFree( vSimInfo );
    if ( pPars->fVerbose )
        ABC_PRT( "Time", Abc_Clock() - clkTotal );
//    if ( RetValue && pPars->fCheckMiter )
//        Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
    return RetValue;
}

int Cec_ManSeqSemiformal	(	Gia_Man_t *	pAig,
		Cec_ParSmf_t *	pPars
	)

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

Synopsis [Performs semiformal refinement of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file cecSeq.c.

{ 
    int nAddFrames = 16; // additional timeframes to simulate
    int nCountNoRef = 0;
    int nFramesReal;
    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
    Vec_Ptr_t * vSimInfo; 
    Vec_Str_t * vStatus;
    Abc_Cex_t * pState;
    Gia_Man_t * pSrm, * pReduce, * pAux;
    int r, nPats, RetValue = 0;
    if ( pAig->pReprs == NULL )
    { 
        Abc_Print( 1, "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
        return -1;
    }
    if ( Gia_ManRegNum(pAig) == 0 )
    {
        Abc_Print( 1, "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
        return -1;
    }
    Gia_ManRandom( 1 );
    // prepare starting pattern
    pState = Abc_CexAlloc( Gia_ManRegNum(pAig), 0, 0 );
    pState->iFrame = -1;
    pState->iPo = -1;
    // prepare SAT solving
    Cec_ManSatSetDefaultParams( pParsSat );
    pParsSat->nBTLimit = pPars->nBTLimit;
    pParsSat->fVerbose = pPars->fVerbose;
    if ( pParsSat->fVerbose )
    {
        Abc_Print( 1, "Starting: " );
        Gia_ManEquivPrintClasses( pAig, 0, 0 );
    }
    // perform the given number of BMC rounds
    Gia_ManCleanMark0( pAig );
    for ( r = 0; r < pPars->nRounds; r++ )
    {
        if ( !Cec_ManCheckNonTrivialCands(pAig) )
        {
            Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
            break;
        }
//        Abc_CexPrint( pState );
        // derive speculatively reduced model
//        pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
        pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs );
        if ( pSrm == NULL )
        {
            Abc_Print( 1, "Quitting refinement because miter could not be unrolled.\n" );
            break;
        }
        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) );
        if ( pPars->fVerbose )
            Abc_Print( 1, "Unrolled for %d frames.\n", nFramesReal );
        // allocate room for simulation info
        vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
            Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords );
        Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
        // fill in simulation info with counter-examples
        vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
        Vec_StrFree( vStatus );
        Gia_ManStop( pSrm );
        // resimulate and refine the classes
        RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState, pPars->fCheckMiter );
        Vec_PtrFree( vSimInfo );
        assert( pState->iPo >= 0 ); // hit counter
        pState->iPo = -1;
        if ( pPars->fVerbose )
        {
            Abc_Print( 1, "BMC = %3d ", nPats );
            Gia_ManEquivPrintClasses( pAig, 0, 0 );
        }

        // write equivalence classes
        Gia_AigerWrite( pAig, "gore.aig", 0, 0 );
        // reduce the model
        pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
        if ( pReduce )
        {
            pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
            Gia_ManStop( pAux );
            Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
//            Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
//          Gia_ManPrintStatsShort( pReduce );
            Gia_ManStop( pReduce );
        }

        if ( RetValue )
        {
            Abc_Print( 1, "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" );
            break;
        }
        // decide when to stop
        if ( nPats > 0 )
            nCountNoRef = 0;
        else if ( ++nCountNoRef == pPars->nNonRefines )
            break;
    }
    ABC_FREE( pState );
    if ( pPars->fCheckMiter )
    {
        int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
        if ( nNonConsts )
            Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
    }
    return RetValue;
}

void Cec_ManSimSetDefaultParams

(

Cec_ParSim_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file cecCore.c.

{
    memset( p, 0, sizeof(Cec_ParSim_t) );
    p->nWords         =      31;  // the number of simulation words
    p->nFrames        =     100;  // the number of simulation frames
    p->nRounds        =      20;  // the max number of simulation rounds
    p->nNonRefines    =       3;  // the max number of rounds without refinement
    p->TimeLimit      =       0;  // the runtime limit in seconds
    p->fCheckMiter    =       0;  // the circuit is the miter
//    p->fFirstStop     =       0;  // stop on the first sat output
    p->fDualOut       =       0;  // miter with separate outputs
    p->fConstCorr     =       0;  // consider only constants
    p->fSeqSimulate   =       0;  // performs sequential simulation
    p->fVeryVerbose   =       0;  // verbose stats
    p->fVerbose       =       0;  // verbose stats
} 

void Cec_ManSimulation	(	Gia_Man_t *	pAig,
		Cec_ParSim_t *	pPars
	)

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

Synopsis [Core procedure for simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 284 of file cecCore.c.

{
    int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0;
    Gia_ManRandom( 1 );
    if ( pPars->fSeqSimulate )
        Abc_Print( 1, "Performing rounds of random simulation of %d frames with %d words.\n", 
            pPars->nRounds, pPars->nFrames, pPars->nWords );
    nLitsOld = Gia_ManEquivCountLits( pAig );
    for ( r = 0; r < pPars->nRounds; r++ )
    {
        if ( Cec_ManSimulationOne( pAig, pPars ) )
        {
            fStop = 1;
            break;
        }
        // decide when to stop
        nLitsNew = Gia_ManEquivCountLits( pAig );
        if ( nLitsOld == 0 || nLitsOld > nLitsNew )
        {
            nLitsOld = nLitsNew;
            nCountNoRef = 0;
        }
        else if ( ++nCountNoRef == pPars->nNonRefines )
        {
            r++;
            break;
        }
        assert( nLitsOld == nLitsNew );
    }
//    if ( pPars->fVerbose )
    if ( r == pPars->nRounds || fStop )
        Abc_Print( 1, "Random simulation is stopped after %d rounds.\n", r );
    else
        Abc_Print( 1, "Random simulation saturated after %d rounds.\n", r );
    if ( pPars->fCheckMiter )
    {
        int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
        if ( nNonConsts )
            Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
    }
}

void Cec_ManSmfSetDefaultParams

(

Cec_ParSmf_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file cecCore.c.

{
    memset( p, 0, sizeof(Cec_ParSmf_t) );
    p->nWords         =      31;  // the number of simulation words
    p->nRounds        =     200;  // the number of simulation rounds
    p->nFrames        =     200;  // the max number of time frames
    p->nNonRefines    =       3;  // the max number of rounds without refinement
    p->nMinOutputs    =       0;  // the min outputs to accumulate
    p->nBTLimit       =     100;  // conflict limit at a node
    p->TimeLimit      =       0;  // the runtime limit in seconds
    p->fDualOut       =       0;  // miter with separate outputs
    p->fCheckMiter    =       0;  // the circuit is the miter
//    p->fFirstStop     =       0;  // stop on the first sat output
    p->fVerbose       =       0;  // verbose stats
} 

int Cec_ManVerify	(	Gia_Man_t *	pInit,
		Cec_ParCec_t *	pPars
	)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [New CEC engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file cecCec.c.

{
    int fDumpUndecided = 0;
    Cec_ParFra_t ParsFra, * pParsFra = &ParsFra;
    Gia_Man_t * p, * pNew;
    int RetValue;
    abctime clk = Abc_Clock();
    abctime clkTotal = Abc_Clock();
    // consider special cases:
    // 1) (SAT) a pair of POs have different value under all-0 pattern
    // 2) (SAT) a pair of POs has different PI/Const drivers
    // 3) (UNSAT) 1-2 do not hold and there is no nodes
    RetValue = Cec_ManHandleSpecialCases( pInit, pPars );
    if ( RetValue == 0 || RetValue == 1 )
        return RetValue;
    // preprocess 
    p = Gia_ManDup( pInit );
    Gia_ManEquivFixOutputPairs( p );
    p = Gia_ManCleanup( pNew = p );
    Gia_ManStop( pNew );
    if ( pPars->fNaive )
    {
        RetValue = Cec_ManVerifyNaive( p, pPars );
        Gia_ManStop( p );
        return RetValue;
    }
    // sweep for equivalences
    Cec_ManFraSetDefaultParams( pParsFra );
    pParsFra->nItersMax    = 1000;
    pParsFra->nBTLimit     = pPars->nBTLimit;
    pParsFra->TimeLimit    = pPars->TimeLimit;
    pParsFra->fVerbose     = pPars->fVerbose;
    pParsFra->fCheckMiter  = 1;
    pParsFra->fDualOut     = 1;
    pNew = Cec_ManSatSweeping( p, pParsFra );
    pPars->iOutFail = pParsFra->iOutFail;
    // update
    pInit->pCexComb = p->pCexComb; p->pCexComb = NULL;
    Gia_ManStop( p );
    p = pInit;
    // continue
    if ( pNew == NULL )
    {
        if ( p->pCexComb != NULL )
        {
            if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
                Abc_Print( 1, "Counter-example simulation has failed.\n" );
            Abc_Print( 1, "Networks are NOT EQUIVALENT.  " );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            return 0;
        }
        p = Gia_ManDup( pInit );
        Gia_ManEquivFixOutputPairs( p );
        p = Gia_ManCleanup( pNew = p );
        Gia_ManStop( pNew );
        pNew = p;
    }
    if ( pPars->fVerbose )
    {
        Abc_Print( 1, "Networks are UNDECIDED after the new CEC engine.  " );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    if ( fDumpUndecided )
    {
        ABC_FREE( pNew->pReprs );
        ABC_FREE( pNew->pNexts );
        Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 );
        Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
    }
    if ( pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
    {
        Gia_ManStop( pNew );
        return -1;
    }
    // call other solver
    if ( pPars->fVerbose )
        Abc_Print( 1, "Calling the old CEC engine.\n" );
    fflush( stdout );
    RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal );
    p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
    if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
        Abc_Print( 1, "Counter-example simulation has failed.\n" );
    Gia_ManStop( pNew );
    return RetValue;
}

int Cec_ManVerifyTwo	(	Gia_Man_t *	p0,
		Gia_Man_t *	p1,
		int	fVerbose
	)

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

Synopsis [New CEC engine applied to two circuits.]

Description []

SideEffects []

SeeAlso []

Definition at line 405 of file cecCec.c.

{
    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
    Gia_Man_t * pMiter;
    int RetValue;
    Cec_ManCecSetDefaultParams( pPars );
    pPars->fVerbose = fVerbose;
    pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, 0, pPars->fVerbose );
    if ( pMiter == NULL )
        return -1;
    RetValue = Cec_ManVerify( pMiter, pPars );
    p0->pCexComb = pMiter->pCexComb; pMiter->pCexComb = NULL;
    Gia_ManStop( pMiter );
    return RetValue;
}

int Cec_SeqReadMinDomSize

(

Cec_ParSeq_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file cecSynth.c.

{
    return p->nMinDomSize;
}

int Cec_SeqReadVerbose

(

Cec_ParSeq_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file cecSynth.c.

{
    return p->fVerbose;
}

void Cec_SeqSynthesisSetDefaultParams

(

Cec_ParSeq_t *

p

)

DECLARATIONS ///.

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

FileName [cecSynth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Partitioned sequential synthesis.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Populate sequential synthesis parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file cecSynth.c.

{
    memset( p, 0, sizeof(Cec_ParSeq_t) );
    p->fUseLcorr    =    0;  // enables latch correspondence
    p->fUseScorr    =    0;  // enables signal correspondence
    p->nBTLimit     = 1000;  // (scorr/lcorr) conflict limit at a node
    p->nFrames      =    1;  // (scorr only) the number of timeframes
    p->nLevelMax    =   -1;  // (scorr only) the max number of levels
    p->fConsts      =    1;  // (scl only) merging constants
    p->fEquivs      =    1;  // (scl only) merging equivalences
    p->fUseMiniSat  =    0;  // enables MiniSat in lcorr/scorr
    p->nMinDomSize  =  100;  // the size of minimum clock domain
    p->fVeryVerbose =    0;  // verbose stats
    p->fVerbose     =    0;  // verbose stats
}

int Cec_SequentialSynthesisPart	(	Gia_Man_t *	p,
		Cec_ParSeq_t *	pPars
	)

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

Synopsis [Partitioned sequential synthesis.]

Description [Returns AIG annotated with equivalence classes.]

SideEffects []

SeeAlso []

Definition at line 291 of file cecSynth.c.

{
    int fPrintParts = 0;
    char Buffer[100];
    Gia_Man_t * pTemp;
    Vec_Ptr_t * vParts = (Vec_Ptr_t *)p->vClockDoms;
    Vec_Int_t * vPart;
    int * pMapBack, * pReprs;
    int i, nCountPis, nCountRegs;
    int nClasses;
    abctime clk = Abc_Clock();

    // save parameters
    if ( fPrintParts )
    {
        // print partitions
        Abc_Print( 1, "The following clock domains are used:\n" );
        Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
        {
            pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
            sprintf( Buffer, "part%03d.aig", i );
            Gia_AigerWrite( pTemp, Buffer, 0, 0 );
            Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
                i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) );
            Gia_ManStop( pTemp );
        }
    }

    // perform sequential synthesis for clock domains
    pReprs = ABC_FALLOC( int, Gia_ManObjNum(p) );
    Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
    {
        pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, &pMapBack );
        if ( nCountPis > 0 ) 
        {
            if ( pPars->fUseScorr )
            {
                Cec_ParCor_t CorPars, * pCorPars = &CorPars;
                Cec_ManCorSetDefaultParams( pCorPars );
                pCorPars->nBTLimit   = pPars->nBTLimit;
                pCorPars->nLevelMax  = pPars->nLevelMax;
                pCorPars->fVerbose   = pPars->fVeryVerbose;
                pCorPars->fUseCSat   = 1;
                Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
            }
            else if ( pPars->fUseLcorr )
            {
                Cec_ParCor_t CorPars, * pCorPars = &CorPars;
                Cec_ManCorSetDefaultParams( pCorPars );
                pCorPars->fLatchCorr = 1;
                pCorPars->nBTLimit   = pPars->nBTLimit;
                pCorPars->fVerbose   = pPars->fVeryVerbose;
                pCorPars->fUseCSat   = 1;
                Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
            }
            else
            {
//                pNew = Gia_ManSeqStructSweep( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
//                Gia_ManStop( pNew );
                Gia_ManSeqCleanupClasses( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
            }
//Abc_Print( 1, "Part equivalences = %d.\n", Gia_ManEquivCountLitsAll(pTemp) );
            nClasses = Gia_TransferMappedClasses( pTemp, pMapBack, pReprs );
            if ( pPars->fVerbose )
            {
                Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. Cl = %5d.\n", 
                    i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp), nClasses );
            }
        }
        Gia_ManStop( pTemp );
        ABC_FREE( pMapBack );
    }

    // generate resulting equivalences
    Gia_ManNormalizeEquivalences( p, pReprs );
//Abc_Print( 1, "Total equivalences = %d.\n", Gia_ManEquivCountLitsAll(p) );
    ABC_FREE( pReprs );
    if ( pPars->fVerbose )
    {
        Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
    }
    return 1;
}