ssw.h File Reference

Go to the source code of this file.

Data Structures
struct	Ssw_Pars_t_
struct	Ssw_RarPars_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Ssw_Pars_t_	Ssw_Pars_t
	INCLUDES ///. More...
typedef struct Ssw_RarPars_t_	Ssw_RarPars_t
typedef struct Ssw_Sml_t_	Ssw_Sml_t

Functions
int	Ssw_BmcDynamic (Aig_Man_t *pAig, int nFramesMax, int nConfLimit, int fVerbose, int *piFrame)
	MACRO DEFINITIONS ///. More...
int	Ssw_ManSetConstrPhases (Aig_Man_t *p, int nFrames, Vec_Int_t **pvInits)
void	Ssw_ManSetDefaultParams (Ssw_Pars_t *p)
	DECLARATIONS ///. More...
void	Ssw_ManSetDefaultParamsLcorr (Ssw_Pars_t *p)
Aig_Man_t *	Ssw_SignalCorrespondence (Aig_Man_t *pAig, Ssw_Pars_t *pPars)
Aig_Man_t *	Ssw_LatchCorrespondence (Aig_Man_t *pAig, Ssw_Pars_t *pPars)
int	Ssw_SecWithSimilarityPairs (Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs, Ssw_Pars_t *pPars)
int	Ssw_SecWithSimilarity (Aig_Man_t *p0, Aig_Man_t *p1, Ssw_Pars_t *pPars)
Aig_Man_t *	Ssw_SignalCorrespondencePart (Aig_Man_t *pAig, Ssw_Pars_t *pPars)
	DECLARATIONS ///. More...
int	Ssw_MiterStatus (Aig_Man_t *p, int fVerbose)
	DECLARATIONS ///. More...
int	Ssw_SecWithPairs (Aig_Man_t *pAig1, Aig_Man_t *pAig2, Vec_Int_t *vIds1, Vec_Int_t *vIds2, Ssw_Pars_t *pPars)
int	Ssw_SecGeneral (Aig_Man_t *pAig1, Aig_Man_t *pAig2, Ssw_Pars_t *pPars)
int	Ssw_SecGeneralMiter (Aig_Man_t *pMiter, Ssw_Pars_t *pPars)
void	Ssw_RarSetDefaultParams (Ssw_RarPars_t *p)
	FUNCTION DEFINITIONS ///. More...
int	Ssw_RarSignalFilter (Aig_Man_t *pAig, Ssw_RarPars_t *pPars)
int	Ssw_RarSimulate (Aig_Man_t *pAig, Ssw_RarPars_t *pPars)
Ssw_Sml_t *	Ssw_SmlSimulateComb (Aig_Man_t *pAig, int nWords)
Ssw_Sml_t *	Ssw_SmlSimulateSeq (Aig_Man_t *pAig, int nPref, int nFrames, int nWords)
void	Ssw_SmlUnnormalize (Ssw_Sml_t *p)
void	Ssw_SmlStop (Ssw_Sml_t *p)
int	Ssw_SmlNumFrames (Ssw_Sml_t *p)
int	Ssw_SmlNumWordsTotal (Ssw_Sml_t *p)
unsigned *	Ssw_SmlSimInfo (Ssw_Sml_t *p, Aig_Obj_t *pObj)
int	Ssw_SmlObjsAreEqualWord (Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
void	Ssw_SmlInitializeSpecial (Ssw_Sml_t *p, Vec_Int_t *vInit)
int	Ssw_SmlCheckNonConstOutputs (Ssw_Sml_t *p)
Vec_Ptr_t *	Ssw_SmlSimDataPointers (Ssw_Sml_t *p)

Typedef Documentation

typedef typedefABC_NAMESPACE_HEADER_START struct Ssw_Pars_t_ Ssw_Pars_t

INCLUDES ///.

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

FileName [ssw.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 40 of file ssw.h.

typedef struct Ssw_RarPars_t_ Ssw_RarPars_t

Definition at line 89 of file ssw.h.

typedef struct Ssw_Sml_t_ Ssw_Sml_t

Definition at line 115 of file ssw.h.

Function Documentation

int Ssw_BmcDynamic	(	Aig_Man_t *	pAig,
		int	nFramesMax,
		int	nConfLimit,
		int	fVerbose,
		int *	piFrame
	)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 126 of file sswBmc.c.

{
    Ssw_Frm_t * pFrm;
    Ssw_Sat_t * pSat;
    Aig_Obj_t * pObj, * pObjFrame;
    int status, Lit, i, f, RetValue;
    abctime clkPart;

    // start managers
    assert( Saig_ManRegNum(pAig) > 0 );
    Aig_ManSetCioIds( pAig );
    pSat = Ssw_SatStart( 0 );
    pFrm = Ssw_FrmStart( pAig );
    pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 );
    // report statistics
    if ( fVerbose )
    {
        Abc_Print( 1, "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n",
            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
        fflush( stdout );
    }
    // perform dynamic unrolling
    RetValue = -1;
    for ( f = 0; f < nFramesMax; f++ )
    {
        clkPart = Abc_Clock();
        Saig_ManForEachPo( pAig, pObj, i )
        {
            // unroll the circuit for this output
            Ssw_BmcUnroll_rec( pFrm, pObj, f );
            pObjFrame = Ssw_ObjFrame_( pFrm, pObj, f );
            Ssw_CnfNodeAddToSolver( pSat, Aig_Regular(pObjFrame) );
            status = sat_solver_simplify(pSat->pSat);
            assert( status );
            // solve
            Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) );
            if ( fVerbose )
            {
                Abc_Print( 1, "Solving output %2d of frame %3d ... \r",
                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
            }
            status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
            if ( status == l_False )
            {
/*
                Lit = lit_neg( Lit );
                RetValue = sat_solver_addclause( pSat->pSat, &Lit, &Lit + 1 );
                assert( RetValue );
                if ( pSat->pSat->qtail != pSat->pSat->qhead )
                {
                    RetValue = sat_solver_simplify(pSat->pSat);
                    assert( RetValue );
                }
*/
                RetValue = 1;
                continue;
            }
            else if ( status == l_True )
            {
                pAig->pSeqModel = Ssw_BmcGetCounterExample( pFrm, pSat, i, f );
                if ( piFrame )
                    *piFrame = f;
                RetValue = 0;
                break;
            }
            else
            {
                if ( piFrame )
                    *piFrame = f;
                RetValue = -1;
                break;
            }
        }
        if ( fVerbose )
        {
            Abc_Print( 1, "Solved %2d outputs of frame %3d.  ", Saig_ManPoNum(pAig), f );
            Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ",
                (double)pSat->pSat->stats.conflicts,
                pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
            ABC_PRT( "T", Abc_Clock() - clkPart );
            clkPart = Abc_Clock();
            fflush( stdout );
        }
        if ( RetValue != 1 )
            break;
    }

    Ssw_SatStop( pSat );
    Ssw_FrmStop( pFrm );
    return RetValue;
}

Aig_Man_t* Ssw_LatchCorrespondence	(	Aig_Man_t *	pAig,
		Ssw_Pars_t *	pPars
	)

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

Synopsis [Performs computation of latch correspondence.]

Description []

SideEffects []

SeeAlso []

Definition at line 521 of file sswCore.c.

{
    Aig_Man_t * pRes;
    Ssw_Pars_t Pars;
    if ( pPars == NULL )
        Ssw_ManSetDefaultParamsLcorr( pPars = &Pars );
    pRes = Ssw_SignalCorrespondence( pAig, pPars );
//    if ( pPars->fConstrs && pPars->fVerbose )
//        Ssw_ReportConeReductions( pAig, pRes );
    return pRes;
}

int Ssw_ManSetConstrPhases	(	Aig_Man_t *	p,
		int	nFrames,
		Vec_Int_t **	pvInits
	)

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

Synopsis [Finds one satisfiable assignment of the timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file sswConstr.c.

{
    Aig_Man_t * pFrames;
    sat_solver * pSat;
    Cnf_Dat_t * pCnf;
    Aig_Obj_t * pObj;
    int i, RetValue;
    if ( pvInits )
        *pvInits = NULL;
//    assert( p->nConstrs > 0 );
    // derive the timeframes
    pFrames = Ssw_FramesWithConstraints( p, nFrames );
    // create CNF
    pCnf = Cnf_Derive( pFrames, 0 );
    // create SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    if ( pSat == NULL )
    {
        Cnf_DataFree( pCnf );
        Aig_ManStop( pFrames );
        return 1;
    }
    // solve
    RetValue = sat_solver_solve( pSat, NULL, NULL,
        (ABC_INT64_T)1000000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( RetValue == l_True && pvInits )
    {
        *pvInits = Vec_IntAlloc( 1000 );
        Aig_ManForEachCi( pFrames, pObj, i )
            Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) );

//        Aig_ManForEachCi( pFrames, pObj, i )
//            Abc_Print( 1, "%d", Vec_IntEntry(*pvInits, i) );
//        Abc_Print( 1, "\n" );
    }
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    Aig_ManStop( pFrames );
    if ( RetValue == l_False )
        return 1;
    if ( RetValue == l_True )
        return 0;
    return -1;
}

void Ssw_ManSetDefaultParams

(

Ssw_Pars_t *

p

)

DECLARATIONS ///.

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

FileName [sswCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [The core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswCore.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswCore.c.

{
    memset( p, 0, sizeof(Ssw_Pars_t) );
    p->nPartSize      =       0;  // size of the partition
    p->nOverSize      =       0;  // size of the overlap between partitions
    p->nFramesK       =       1;  // the induction depth
    p->nFramesAddSim  =       2;  // additional frames to simulate
    p->fConstrs       =       0;  // treat the last nConstrs POs as seq constraints
    p->fMergeFull     =       0;  // enables full merge when constraints are used
    p->nBTLimit       =    1000;  // conflict limit at a node
    p->nBTLimitGlobal = 5000000;  // conflict limit for all runs
    p->nMinDomSize    =     100;  // min clock domain considered for optimization
    p->nItersStop     =      -1;  // stop after the given number of iterations
    p->nResimDelta    =    1000;  // the internal of nodes to resimulate
    p->nStepsMax      =      -1;  // (scorr only) the max number of induction steps
    p->fPolarFlip     =       0;  // uses polarity adjustment
    p->fLatchCorr     =       0;  // performs register correspondence
    p->fConstCorr     =       0;  // performs constant correspondence
    p->fOutputCorr    =       0;  // perform 'PO correspondence'
    p->fSemiFormal    =       0;  // enable semiformal filtering
    p->fDynamic       =       0;  // dynamic partitioning
    p->fLocalSim      =       0;  // local simulation
    p->fVerbose       =       0;  // verbose stats
    p->fEquivDump     =       0;  // enables dumping equivalences

    // latch correspondence
    p->fLatchCorrOpt  =       0;  // performs optimized register correspondence
    p->nSatVarMax     =    1000;  // the max number of SAT variables
    p->nRecycleCalls  =      50;  // calls to perform before recycling SAT solver
    // signal correspondence
    p->nSatVarMax2    =    5000;  // the max number of SAT variables
    p->nRecycleCalls2 =     250;  // calls to perform before recycling SAT solver
    // return values
    p->nIters         =       0;  // the number of iterations performed
}

void Ssw_ManSetDefaultParamsLcorr

(

Ssw_Pars_t *

p

)

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

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 92 of file sswCore.c.

{
    Ssw_ManSetDefaultParams( p );
    p->fLatchCorrOpt = 1;
    p->nBTLimit      = 10000;
}

int Ssw_MiterStatus	(	Aig_Man_t *	p,
		int	fVerbose
	)

DECLARATIONS ///.

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

FileName [sswPairs.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Calls to the SAT solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswPairs.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Reports the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswPairs.c.

{
    Aig_Obj_t * pObj, * pChild;
    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
//    if ( p->pData )
//        return 0;
    Saig_ManForEachPo( p, pObj, i )
    {
        pChild = Aig_ObjChild0(pObj);
        // check if the output is constant 0
        if ( pChild == Aig_ManConst0(p) )
        {
            CountConst0++;
            continue;
        }
        // check if the output is constant 1
        if ( pChild == Aig_ManConst1(p) )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output is a primary input
        if ( p->nRegs == 0 && Aig_ObjIsCi(Aig_Regular(pChild)) )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output can be not constant 0
        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
        {
            CountNonConst0++;
            continue;
        }
        CountUndecided++;
    }

    if ( fVerbose )
    {
        Abc_Print( 1, "Miter has %d outputs. ", Saig_ManPoNum(p) );
        Abc_Print( 1, "Const0 = %d.  ", CountConst0 );
        Abc_Print( 1, "NonConst0 = %d.  ", CountNonConst0 );
        Abc_Print( 1, "Undecided = %d.  ", CountUndecided );
        Abc_Print( 1, "\n" );
    }

    if ( CountNonConst0 )
        return 0;
    if ( CountUndecided )
        return -1;
    return 1;
}

void Ssw_RarSetDefaultParams

(

Ssw_RarPars_t *

p

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file sswRarity.c.

{
    memset( p, 0, sizeof(Ssw_RarPars_t) );
    p->nFrames       =  20;
    p->nWords        =  50;
    p->nBinSize      =   8;
    p->nRounds       =   0;
    p->nRestart      =   0;
    p->nRandSeed     =   0;
    p->TimeOut       =   0;
    p->TimeOutGap    =   0;
    p->fSolveAll     =   0;
    p->fDropSatOuts  =   0;
    p->fSetLastState =   0;
    p->fVerbose      =   0;
    p->fNotVerbose   =   0;
}

int Ssw_RarSignalFilter	(	Aig_Man_t *	pAig,
		Ssw_RarPars_t *	pPars
	)

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

Synopsis [Filter equivalence classes of nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1219 of file sswRarity.c.

{
    Ssw_RarMan_t * p;
    int r, f = -1, i, k;
    abctime clkTotal = Abc_Clock();
    abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    int nNumRestart = 0;
    int nSavedSeed = pPars->nRandSeed;
    int RetValue = -1;
    assert( Aig_ManRegNum(pAig) > 0 );
    assert( Aig_ManConstrNum(pAig) == 0 );
    // consider the case of empty AIG
    if ( Aig_ManNodeNum(pAig) == 0 )
        return -1;
    // check trivially SAT miters
    if ( pPars->fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
        return 0;
    if ( pPars->fVerbose )
        Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
            pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRandSeed, pPars->TimeOut );
    // reset random numbers
    Ssw_RarManPrepareRandom( nSavedSeed );

    // create manager
    p = Ssw_RarManStart( pAig, pPars );
    // compute starting state if needed
    assert( p->vInits == NULL );
    if ( pPars->pCex )
    {
        p->vInits = Ssw_RarFindStartingState( pAig, pPars->pCex );
        Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" );
    }
    else
        p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
    // duplicate the array
    for ( i = 1; i < pPars->nWords; i++ )
        for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
            Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
    assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * pPars->nWords );

    // create trivial equivalence classes with all nodes being candidates for constant 1
    if ( pAig->pReprs == NULL )
        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchOnly, 0 );
    else
        p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
    Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
    // print the stats
    if ( pPars->fVerbose )
    {
        Abc_Print( 1, "Initial  :  " );
        Ssw_ClassesPrint( p->ppClasses, 0 );
    }
    // refine classes using BMC
    for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
    {
        // start filtering equivalence classes
        if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
        {
            Abc_Print( 1, "All equivalences are refined away.\n" );
            break;
        }
        // simulate
        for ( f = 0; f < pPars->nFrames; f++ )
        {
            Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
            if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, -1, 0) )
            {
                if ( !pPars->fVerbose )
                    Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
//                Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * pPars->nFrames, (r+1) * pPars->nFrames );
                if ( pPars->fVerbose )
                    Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
                Ssw_RarManPrepareRandom( nSavedSeed );
                Abc_CexFree( pAig->pSeqModel );
                pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, 1 );
                // print final report
                Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
                RetValue = 0;
                goto finish;
            }
            // check timeout
            if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
            {
                if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
                Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
                Abc_Print( 1, "Reached timeout (%d sec).\n",  pPars->TimeOut );
                goto finish;
            }
        }
        // get initialization patterns
        if ( pPars->pCex == NULL && pPars->nRestart && r == pPars->nRestart )
        {
            r = -1;
            nSavedSeed = (nSavedSeed + 1) % 1000;
            Ssw_RarManPrepareRandom( nSavedSeed );
            Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
            nNumRestart++;
            Vec_IntClear( p->vPatBests );
            // clean rarity info
//            memset( p->pRarity, 0, sizeof(int) * (1 << nBinSize) * p->nGroups );
        }
        else
            Ssw_RarTransferPatterns( p, p->vInits );
        // printout
        if ( pPars->fVerbose )
        {
            Abc_Print( 1, "Round %3d:  ", r );
            Ssw_ClassesPrint( p->ppClasses, 0 );
        }
        else
        {
            Abc_Print( 1, "." );
        }
    }
finish:
    // report
    if ( r == pPars->nRounds && f == pPars->nFrames )
    {
        if ( !pPars->fVerbose )
            Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
        Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs.    ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
    }
    // cleanup
    Ssw_RarManStop( p );
    return RetValue;
}

int Ssw_RarSimulate	(	Aig_Man_t *	pAig,
		Ssw_RarPars_t *	pPars
	)

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

Synopsis [Perform sequential simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 973 of file sswRarity.c.

{
    int fTryBmc = 0;
    int fMiter = 1;
    Ssw_RarMan_t * p;
    int r, f = -1;
    abctime clk, clkTotal = Abc_Clock();
    abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    abctime timeLastSolved = 0;
    int nNumRestart = 0;
    int nSavedSeed = pPars->nRandSeed;
    int RetValue = -1;
    int iFrameFail = -1;
    assert( Aig_ManRegNum(pAig) > 0 );
    assert( Aig_ManConstrNum(pAig) == 0 );
    ABC_FREE( pAig->pSeqModel );
    // consider the case of empty AIG
//    if ( Aig_ManNodeNum(pAig) == 0 )
//        return -1;
    // check trivially SAT miters
//    if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
//        return 0;
    if ( pPars->fVerbose )
        Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d restart, %d seed, and %d sec timeout.\n",
            pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRestart, pPars->nRandSeed, pPars->TimeOut );
    // reset random numbers
    Ssw_RarManPrepareRandom( nSavedSeed );

    // create manager
    p = Ssw_RarManStart( pAig, pPars );
    p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * pPars->nWords );

    // perform simulation rounds
    pPars->nSolved = 0;
    timeLastSolved = Abc_Clock();
    for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
    {
        clk = Abc_Clock();
        if ( fTryBmc )
        {
            Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
            Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 );
//            if ( pNewAig->pSeqModel != NULL )
//                Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail );
            Aig_ManStop( pNewAig );
        }
        // simulate
        for ( f = 0; f < pPars->nFrames; f++ )
        {
            Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
            if ( fMiter )
            {
                int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, Abc_Clock() - clkTotal);
                if ( Status == 2 )
                {
                    Abc_Print( 1, "Quitting due to callback on fail.\n" );
                    goto finish;
                }
                if ( Status == 1 ) // found CEX
                {
                    RetValue = 0;
                    if ( !pPars->fSolveAll )
                    {
                        if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
        //                Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
                        Ssw_RarManPrepareRandom( nSavedSeed );
                        if ( pPars->fVerbose )
                            Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
                        pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
                        // print final report
                        Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
                        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
                        goto finish;
                    }
                    timeLastSolved = Abc_Clock();
                }
                // else - did not find a counter example
            }
            // check timeout
            if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
            {
                if ( !pPars->fSilent )
                {
                if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
                Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
                Abc_Print( 1, "Reached timeout (%d sec).\n",  pPars->TimeOut );
                }
                goto finish;
            }
            if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
            {
                if ( !pPars->fSilent )
                {
                if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
                Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs.  ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
                Abc_Print( 1, "Reached gap timeout (%d sec).\n",  pPars->TimeOutGap );
                }
                goto finish;
            }
            // check if all outputs are solved by now
            if ( pPars->fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 )
                goto finish;
        }
        // get initialization patterns
        if ( pPars->nRestart && r == pPars->nRestart )
        {
            r = -1;
            nSavedSeed = (nSavedSeed + 1) % 1000;
            Ssw_RarManPrepareRandom( nSavedSeed );
            Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
            nNumRestart++;
            Vec_IntClear( p->vPatBests );
            // clean rarity info
//            memset( p->pRarity, 0, sizeof(int) * (1 << nBinSize) * p->nGroups );
        }
        else
            Ssw_RarTransferPatterns( p, p->vInits );
        // printout
        if ( pPars->fVerbose )
        {
            if ( pPars->fSolveAll )
            {
                Abc_Print( 1, "Starts =%6d   ",  nNumRestart );
                Abc_Print( 1, "Rounds =%6d   ",  nNumRestart * pPars->nRestart + ((r==-1)?0:r) );
                Abc_Print( 1, "Frames =%6d   ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames );
                Abc_Print( 1, "CEX =%6d (%6.2f %%)   ", pPars->nSolved, 100.0*pPars->nSolved/Saig_ManPoNum(p->pAig) );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
            }
            else
                Abc_Print( 1, "." );
        }

    }
finish:
    if ( pPars->fSetLastState && p->vInits )
    {
        assert( Vec_IntSize(p->vInits) % Aig_ManRegNum(pAig) == 0 );
        Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) );
        pAig->pData = p->vInits;  p->vInits = NULL;
    }
    if ( pPars->nSolved )
    {
/*
        if ( !pPars->fSilent )
        {
        if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
        Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs.    ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
        }
*/
    }
    else if ( r == pPars->nRounds && f == pPars->nFrames )
    {
        if ( !pPars->fSilent )
        {
        if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
        Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs.    ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
        }
    }
    // cleanup
    Ssw_RarManStop( p );
    return RetValue;
}

int Ssw_SecGeneral	(	Aig_Man_t *	pAig1,
		Aig_Man_t *	pAig2,
		Ssw_Pars_t *	pPars
	)

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

Synopsis [Runs inductive SEC for the miter of two AIGs.]

Description []

SideEffects []

SeeAlso []

Definition at line 415 of file sswPairs.c.

{
    Aig_Man_t * pAigRes, * pMiter;
    int RetValue;
    abctime clk = Abc_Clock();
    // try the new AIGs
    Abc_Print( 1, "Performing general verification without node pairs.\n" );
    pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
    Aig_ManCleanup( pMiter );
    pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
    Aig_ManStop( pMiter );
    // report the results
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    // cleanup
    Aig_ManStop( pAigRes );
    return RetValue;
}

int Ssw_SecGeneralMiter	(	Aig_Man_t *	pMiter,
		Ssw_Pars_t *	pPars
	)

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

Synopsis [Runs inductive SEC for the miter of two AIGs.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file sswPairs.c.

{
    Aig_Man_t * pAigRes;
    int RetValue;
    abctime clk = Abc_Clock();
    // try the new AIGs
//    Abc_Print( 1, "Performing general verification without node pairs.\n" );
    pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
    // report the results
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    // cleanup
    Aig_ManStop( pAigRes );
    return RetValue;
}

int Ssw_SecWithPairs	(	Aig_Man_t *	pAig1,
		Aig_Man_t *	pAig2,
		Vec_Int_t *	vIds1,
		Vec_Int_t *	vIds2,
		Ssw_Pars_t *	pPars
	)

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

Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.]

Description []

SideEffects []

SeeAlso []

Definition at line 380 of file sswPairs.c.

{
    Aig_Man_t * pAigRes;
    int RetValue;
    abctime clk = Abc_Clock();
    assert( vIds1 != NULL && vIds2 != NULL );
    // try the new AIGs
    Abc_Print( 1, "Performing specialized verification with node pairs.\n" );
    pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars );
    // report the results
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig1) + Aig_ManRegNum(pAig2) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    // cleanup
    Aig_ManStop( pAigRes );
    return RetValue;
}

int Ssw_SecWithSimilarity	(	Aig_Man_t *	p0,
		Aig_Man_t *	p1,
		Ssw_Pars_t *	pPars
	)

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

Synopsis [Solves SEC with structural similarity.]

Description []

SideEffects []

SeeAlso []

Definition at line 542 of file sswIslands.c.

{
    Vec_Int_t * vPairs;
    Aig_Man_t * pPart0, * pPart1;
    int RetValue;
    if ( pPars->fVerbose )
        Abc_Print( 1, "Performing sequential verification using structural similarity.\n" );
    // consider the case when a miter is given
    if ( p1 == NULL )
    {
        if ( pPars->fVerbose )
        {
            Aig_ManPrintStats( p0 );
        }
        // demiter the miter
        if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
        {
            Abc_Print( 1, "Demitering has failed.\n" );
            return -1;
        }
    }
    else
    {
        pPart0 = Aig_ManDupSimple( p0 );
        pPart1 = Aig_ManDupSimple( p1 );
    }
    if ( pPars->fVerbose )
    {
//        Aig_ManPrintStats( pPart0 );
//        Aig_ManPrintStats( pPart1 );
        if ( p1 == NULL )
        {
//        Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
//        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
//        Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
        }
    }
    assert( Aig_ManRegNum(pPart0) > 0 );
    assert( Aig_ManRegNum(pPart1) > 0 );
    assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
    assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
    // derive pairs
//    vPairs = Saig_StrSimPerformMatching_hack( pPart0, pPart1 );
    vPairs = Saig_StrSimPerformMatching( pPart0, pPart1, 0, pPars->fVerbose, NULL );
    RetValue = Ssw_SecWithSimilarityPairs( pPart0, pPart1, vPairs, pPars );
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    Vec_IntFree( vPairs );
    return RetValue;
}

int Ssw_SecWithSimilarityPairs	(	Aig_Man_t *	p0,
		Aig_Man_t *	p1,
		Vec_Int_t *	vPairs,
		Ssw_Pars_t *	pPars
	)

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

Synopsis [Solves SEC with structural similarity.]

Description [The first two arguments are pointers to the AIG managers. The third argument is the array of pairs of IDs of structurally equivalent nodes from the first and second managers, respectively.]

SideEffects [The managers will be updated by adding "islands of difference".]

SeeAlso []

Definition at line 478 of file sswIslands.c.

{
    Ssw_Pars_t Pars;
    Aig_Man_t * pAigRes;
    int RetValue;
    abctime clk = Abc_Clock();
    // derive parameters if not given
    if ( pPars == NULL )
        Ssw_ManSetDefaultParams( pPars = &Pars );
    // reduce the AIG with pairs
    pAigRes = Ssw_SecWithSimilaritySweep( p0, p1, vPairs, pPars );
    // report the result of verification
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    Aig_ManStop( pAigRes );
    return RetValue;
}

Aig_Man_t* Ssw_SignalCorrespondence	(	Aig_Man_t *	pAig,
		Ssw_Pars_t *	pPars
	)

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

Synopsis [Performs computation of signal correspondence with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 414 of file sswCore.c.

{
    Ssw_Pars_t Pars;
    Aig_Man_t * pAigNew;
    Ssw_Man_t * p;
    assert( Aig_ManRegNum(pAig) > 0 );
    // reset random numbers
    Aig_ManRandom( 1 );
    // if parameters are not given, create them
    if ( pPars == NULL )
        Ssw_ManSetDefaultParams( pPars = &Pars );
    // consider the case of empty AIG
    if ( Aig_ManNodeNum(pAig) == 0 )
    {
        pPars->nIters = 0;
        // Ntl_ManFinalize() needs the following to satisfy an assertion
        Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
        return Aig_ManDupOrdered(pAig);
    }
    // check and update parameters
    if ( pPars->fLatchCorrOpt )
    {
        pPars->fLatchCorr = 1;
        pPars->nFramesAddSim = 0;
        if ( (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) )
           return Ssw_SignalCorrespondencePart( pAig, pPars );
    }
    else
    {
        assert( pPars->nFramesK > 0 );
        // perform partitioning
        if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
             || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
            return Ssw_SignalCorrespondencePart( pAig, pPars );
    }

    if ( pPars->fScorrGia )
    {
        if ( pPars->fLatchCorrOpt )
        {
            extern Aig_Man_t * Cec_LatchCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
            return Cec_LatchCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
        }
        else
        {
            extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
            return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
        }
    }

    // start the induction manager
    p = Ssw_ManCreate( pAig, pPars );
    // compute candidate equivalence classes
//    p->pPars->nConstrs = 1;
    if ( p->pPars->fConstrs )
    {
        // create trivial equivalence classes with all nodes being candidates for constant 1
        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
        Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
        // derive phase bits to satisfy the constraints
        if ( Ssw_ManSetConstrPhases( pAig, p->pPars->nFramesK + 1, &p->vInits ) != 0 )
        {
            Abc_Print( 1, "Ssw_SignalCorrespondence(): The init state does not satisfy the constraints!\n" );
            p->pPars->fVerbose = 0;
            Ssw_ManStop( p );
            return NULL;
        }
        // perform simulation of the first timeframes
        Ssw_ManRefineByConstrSim( p );
    }
    else
    {
        // perform one round of seq simulation and generate candidate equivalence classes
        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
//        p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
        if ( pPars->fLatchCorrOpt )
            p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
        else if ( pPars->fDynamic )
            p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
        else
            p->pSml = Ssw_SmlStart( pAig, 0, 1 + p->pPars->nFramesAddSim, 1 );
        Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
    }
    // allocate storage
    if ( p->pPars->fLocalSim )
        p->pVisited = ABC_CALLOC( int, Ssw_SmlNumFrames( p->pSml ) * Aig_ManObjNumMax(p->pAig) );
    // perform refinement of classes
    pAigNew = Ssw_SignalCorrespondenceRefine( p );
//    Ssw_ReportOutputs( pAigNew );
    if ( pPars->fConstrs && pPars->fVerbose )
        Ssw_ReportConeReductions( p, pAig, pAigNew );
    // cleanup
    Ssw_ManStop( p );
    return pAigNew;
}

Aig_Man_t* Ssw_SignalCorrespondencePart	(	Aig_Man_t *	pAig,
		Ssw_Pars_t *	pPars
	)

DECLARATIONS ///.

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

FileName [sswPart.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Partitioned signal correspondence.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:

sswPart.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Performs partitioned sequential SAT sweeping.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file sswPart.c.

{
    int fPrintParts = 0;
    char Buffer[100];
    Aig_Man_t * pTemp, * pNew;
    Vec_Ptr_t * vResult;
    Vec_Int_t * vPart;
    int * pMapBack;
    int i, nCountPis, nCountRegs;
    int nClasses, nPartSize, fVerbose;
    abctime clk = Abc_Clock();
    if ( pPars->fConstrs )
    {
        Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
        return NULL;
    }
    // save parameters
    nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
    fVerbose  = pPars->fVerbose;  pPars->fVerbose  = 0;
    // generate partitions
    if ( pAig->vClockDoms )
    {
        // divide large clock domains into separate partitions
        vResult = Vec_PtrAlloc( 100 );
        Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
        {
            if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
                Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
            else
                Vec_PtrPush( vResult, Vec_IntDup(vPart) );
        }
    }
    else
        vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
//    vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); 
//    vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
    if ( fPrintParts )
    {
        // print partitions
        Abc_Print( 1, "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
        Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
        {
//            extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
            sprintf( Buffer, "part%03d.aig", i );
            pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
            Ioa_WriteAiger( 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), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
            Aig_ManStop( pTemp );
        }
    }

    // perform SSW with partitions
    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
    Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
    {
        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
        Aig_ManSetRegNum( pTemp, pTemp->nRegs );
        // create the projection of 1-hot registers
        if ( pAig->vOnehots )
            pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
        // run SSW
        if (nCountPis>0) {
            pNew = Ssw_SignalCorrespondence( pTemp, pPars );
            nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
            if ( fVerbose )
                Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
                    i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
            Aig_ManStop( pNew );
        }
        Aig_ManStop( pTemp );
        ABC_FREE( pMapBack );
    }
    // remap the AIG
    pNew = Aig_ManDupRepr( pAig, 0 );
    Aig_ManSeqCleanup( pNew );
//    Aig_ManPrintStats( pAig );
//    Aig_ManPrintStats( pNew );
    Vec_VecFree( (Vec_Vec_t *)vResult );
    pPars->nPartSize = nPartSize;
    pPars->fVerbose = fVerbose;
    if ( fVerbose )
    {
        ABC_PRT( "Total time", Abc_Clock() - clk );
    }
    return pNew;
}

int Ssw_SmlCheckNonConstOutputs

(

Ssw_Sml_t *

p

)

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

Synopsis [Check if any of the POs becomes non-constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 980 of file sswSim.c.

{
    Aig_Obj_t * pObj;
    int i;
    Saig_ManForEachPo( p->pAig, pObj, i )
    {
        if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
            return 0;
        if ( !Ssw_SmlNodeIsZero(p, pObj) )
            return 1;
    }
    return 0;
}

void Ssw_SmlInitializeSpecial	(	Ssw_Sml_t *	p,
		Vec_Int_t *	vInit
	)

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

Synopsis [Assings random simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 928 of file sswSim.c.

{
    Aig_Obj_t * pObj;
    int Entry, i, nRegs;
    nRegs = Aig_ManRegNum(p->pAig);
    assert( nRegs > 0 );
    assert( nRegs <= Aig_ManCiNum(p->pAig) );
    assert( Vec_IntSize(vInit) == nRegs * p->nWordsFrame );
    // assign random info for primary inputs
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_SmlAssignRandom( p, pObj );
    // assign the initial state for the latches
    Vec_IntForEachEntry( vInit, Entry, i )
        Ssw_SmlObjAssignConstWord( p, Saig_ManLo(p->pAig, i % nRegs), Entry, 0, i / nRegs );
}

int Ssw_SmlNumFrames

(

Ssw_Sml_t *

p

)

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

Synopsis [Returns the number of frames simulated in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1288 of file sswSim.c.

{
    return p->nFrames;
}

int Ssw_SmlNumWordsTotal

(

Ssw_Sml_t *

p

)

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

Synopsis [Returns the total number of simulation words.]

Description []

SideEffects []

SeeAlso []

Definition at line 1304 of file sswSim.c.

{
    return p->nWordsTotal;
}

int Ssw_SmlObjsAreEqualWord	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj0,
		Aig_Obj_t *	pObj1
	)

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 124 of file sswSim.c.

{
    unsigned * pSims0, * pSims1;
    int i;
    pSims0 = Ssw_ObjSim(p, pObj0->Id);
    pSims1 = Ssw_ObjSim(p, pObj1->Id);
    for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
        if ( pSims0[i] != pSims1[i] )
            return 0;
    return 1;
}

Vec_Ptr_t* Ssw_SmlSimDataPointers

(

Ssw_Sml_t *

p

)

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

Synopsis [Get simulation data.]

Description []

SideEffects []

SeeAlso []

Definition at line 1189 of file sswSim.c.

{
    Vec_Ptr_t * vSimInfo;
    Aig_Obj_t * pObj;
    int i;
    vSimInfo = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
    Aig_ManForEachObj( p->pAig, pObj, i )
        Vec_PtrWriteEntry( vSimInfo, i, Ssw_ObjSim(p, i) );
    return vSimInfo;
}

unsigned* Ssw_SmlSimInfo	(	Ssw_Sml_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Returns the pointer to the simulation info of the node.]

Description [The simulation info is normalized unless procedure Ssw_SmlUnnormalize() is called in advance.]

SideEffects []

SeeAlso []

Definition at line 1321 of file sswSim.c.

{
    assert( !Aig_IsComplement(pObj) );
    return Ssw_ObjSim( p, pObj->Id );
}

Ssw_Sml_t* Ssw_SmlSimulateComb	(	Aig_Man_t *	pAig,
		int	nWords
	)

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

Synopsis [Performs simulation of the uninitialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 1228 of file sswSim.c.

{
    Ssw_Sml_t * p;
    p = Ssw_SmlStart( pAig, 0, 1, nWords );
    Ssw_SmlInitialize( p, 0 );
    Ssw_SmlSimulateOne( p );
    return p;
}

Ssw_Sml_t* Ssw_SmlSimulateSeq	(	Aig_Man_t *	pAig,
		int	nPref,
		int	nFrames,
		int	nWords
	)

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

Synopsis [Performs simulation of the initialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 1248 of file sswSim.c.

{
    Ssw_Sml_t * p;
    p = Ssw_SmlStart( pAig, nPref, nFrames, nWords );
    Ssw_SmlInitialize( p, 1 );
    Ssw_SmlSimulateOne( p );
    p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
    return p;
}

void Ssw_SmlStop

(

Ssw_Sml_t *

p

)

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

Synopsis [Deallocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1211 of file sswSim.c.

{
    ABC_FREE( p );
}

void Ssw_SmlUnnormalize

(

Ssw_Sml_t *

p

)

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

Synopsis [Converts simulation information to be not normallized.]

Description []

SideEffects []

SeeAlso []

Definition at line 1044 of file sswSim.c.

{
    Aig_Obj_t * pObj;
    unsigned * pSims;
    int i, k;
    // convert constant 1
    pSims  = Ssw_ObjSim( p, 0 );
    for ( i = 0; i < p->nWordsFrame; i++ )
        pSims[i] = ~pSims[i];
    // convert internal nodes
    Aig_ManForEachNode( p->pAig, pObj, k )
    {
        if ( pObj->fPhase == 0 )
            continue;
        pSims  = Ssw_ObjSim( p, pObj->Id );
        for ( i = 0; i < p->nWordsFrame; i++ )
            pSims[i] = ~pSims[i];
    }
    // PIs/POs are always stored in their natural state
}