sswInt.h File Reference

#include "aig/saig/saig.h"
#include "sat/bsat/satSolver.h"
#include "ssw.h"
#include "aig/ioa/ioa.h"

Include dependency graph for sswInt.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Ssw_Man_t_
struct	Ssw_Sat_t_
struct	Ssw_Frm_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_	Ssw_Man_t
	INCLUDES ///.
typedef struct Ssw_Frm_t_	Ssw_Frm_t
typedef struct Ssw_Sat_t_	Ssw_Sat_t
typedef struct Ssw_Cla_t_	Ssw_Cla_t

Functions
Ssw_Frm_t *	Ssw_FrmStart (Aig_Man_t *pAig)
	FUNCTION DECLARATIONS ///.
void	Ssw_FrmStop (Ssw_Frm_t *p)
Aig_Man_t *	Ssw_FramesWithClasses (Ssw_Man_t *p)
Aig_Man_t *	Ssw_SpeculativeReduction (Ssw_Man_t *p)
Ssw_Cla_t *	Ssw_ClassesStart (Aig_Man_t *pAig)
void	Ssw_ClassesSetData (Ssw_Cla_t *p, void *pManData, unsigned(*pFuncNodeHash)(void *, Aig_Obj_t *), int(*pFuncNodeIsConst)(void *, Aig_Obj_t *), int(*pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *))
void	Ssw_ClassesStop (Ssw_Cla_t *p)
Aig_Man_t *	Ssw_ClassesReadAig (Ssw_Cla_t *p)
Vec_Ptr_t *	Ssw_ClassesGetRefined (Ssw_Cla_t *p)
void	Ssw_ClassesClearRefined (Ssw_Cla_t *p)
int	Ssw_ClassesCand1Num (Ssw_Cla_t *p)
int	Ssw_ClassesClassNum (Ssw_Cla_t *p)
int	Ssw_ClassesLitNum (Ssw_Cla_t *p)
Aig_Obj_t **	Ssw_ClassesReadClass (Ssw_Cla_t *p, Aig_Obj_t *pRepr, int *pnSize)
void	Ssw_ClassesCollectClass (Ssw_Cla_t *p, Aig_Obj_t *pRepr, Vec_Ptr_t *vClass)
void	Ssw_ClassesCheck (Ssw_Cla_t *p)
void	Ssw_ClassesPrint (Ssw_Cla_t *p, int fVeryVerbose)
void	Ssw_ClassesRemoveNode (Ssw_Cla_t *p, Aig_Obj_t *pObj)
Ssw_Cla_t *	Ssw_ClassesPrepare (Aig_Man_t *pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose)
Ssw_Cla_t *	Ssw_ClassesPrepareSimple (Aig_Man_t *pAig, int fLatchCorr, int nMaxLevs)
Ssw_Cla_t *	Ssw_ClassesPrepareFromReprs (Aig_Man_t *pAig)
Ssw_Cla_t *	Ssw_ClassesPrepareTargets (Aig_Man_t *pAig)
Ssw_Cla_t *	Ssw_ClassesPreparePairs (Aig_Man_t *pAig, Vec_Int_t **pvClasses)
Ssw_Cla_t *	Ssw_ClassesPreparePairsSimple (Aig_Man_t *pMiter, Vec_Int_t *vPairs)
int	Ssw_ClassesRefine (Ssw_Cla_t *p, int fRecursive)
int	Ssw_ClassesRefineGroup (Ssw_Cla_t *p, Vec_Ptr_t *vReprs, int fRecursive)
int	Ssw_ClassesRefineOneClass (Ssw_Cla_t *p, Aig_Obj_t *pRepr, int fRecursive)
int	Ssw_ClassesRefineConst1Group (Ssw_Cla_t *p, Vec_Ptr_t *vRoots, int fRecursive)
int	Ssw_ClassesRefineConst1 (Ssw_Cla_t *p, int fRecursive)
int	Ssw_ClassesPrepareRehash (Ssw_Cla_t *p, Vec_Ptr_t *vCands, int fConstCorr)
Ssw_Sat_t *	Ssw_SatStart (int fPolarFlip)
	DECLARATIONS ///.
void	Ssw_SatStop (Ssw_Sat_t *p)
void	Ssw_CnfNodeAddToSolver (Ssw_Sat_t *p, Aig_Obj_t *pObj)
int	Ssw_CnfGetNodeValue (Ssw_Sat_t *p, Aig_Obj_t *pObjFraig)
int	Ssw_ManSweepBmcConstr (Ssw_Man_t *p)
int	Ssw_ManSweepConstr (Ssw_Man_t *p)
void	Ssw_ManRefineByConstrSim (Ssw_Man_t *p)
Aig_Man_t *	Ssw_SignalCorrespondenceRefine (Ssw_Man_t *p)
void	Ssw_ManLoadSolver (Ssw_Man_t *p, Aig_Obj_t *pRepr, Aig_Obj_t *pObj)
int	Ssw_ManSweepDyn (Ssw_Man_t *p)
int	Ssw_ManSweepLatch (Ssw_Man_t *p)
Ssw_Man_t *	Ssw_ManCreate (Aig_Man_t *pAig, Ssw_Pars_t *pPars)
	DECLARATIONS ///.
void	Ssw_ManCleanup (Ssw_Man_t *p)
void	Ssw_ManStop (Ssw_Man_t *p)
int	Ssw_NodesAreEquiv (Ssw_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
	DECLARATIONS ///.
int	Ssw_NodesAreConstrained (Ssw_Man_t *p, Aig_Obj_t *pOld, Aig_Obj_t *pNew)
int	Ssw_NodeIsConstrained (Ssw_Man_t *p, Aig_Obj_t *pPoObj)
int	Ssw_FilterUsingSemi (Ssw_Man_t *pMan, int fCheckTargets, int nConfMax, int fVerbose)
unsigned	Ssw_SmlObjHashWord (Ssw_Sml_t *p, Aig_Obj_t *pObj)
	FUNCTION DEFINITIONS ///.
int	Ssw_SmlObjIsConstWord (Ssw_Sml_t *p, Aig_Obj_t *pObj)
int	Ssw_SmlObjsAreEqualWord (Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
int	Ssw_SmlObjIsConstBit (void *p, Aig_Obj_t *pObj)
int	Ssw_SmlObjsAreEqualBit (void *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
void	Ssw_SmlAssignRandomFrame (Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Ssw_Sml_t *	Ssw_SmlStart (Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
void	Ssw_SmlClean (Ssw_Sml_t *p)
void	Ssw_SmlStop (Ssw_Sml_t *p)
void	Ssw_SmlObjAssignConst (Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
void	Ssw_SmlObjSetWord (Ssw_Sml_t *p, Aig_Obj_t *pObj, unsigned Word, int iWord, int iFrame)
void	Ssw_SmlAssignDist1Plus (Ssw_Sml_t *p, unsigned *pPat)
void	Ssw_SmlSimulateOne (Ssw_Sml_t *p)
void	Ssw_SmlSimulateOneFrame (Ssw_Sml_t *p)
void	Ssw_SmlSimulateOneDyn_rec (Ssw_Sml_t *p, Aig_Obj_t *pObj, int f, int *pVisited, int nVisCounter)
void	Ssw_SmlResimulateSeq (Ssw_Sml_t *p)
void	Ssw_ManResimulateBit (Ssw_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pRepr)
	DECLARATIONS ///.
void	Ssw_ManResimulateWord (Ssw_Man_t *p, Aig_Obj_t *pCand, Aig_Obj_t *pRepr, int f)
int	Ssw_ManGetSatVarValue (Ssw_Man_t *p, Aig_Obj_t *pObj, int f)
	DECLARATIONS ///.
void	Ssw_SmlSavePatternAig (Ssw_Man_t *p, int f)
int	Ssw_ManSweepNode (Ssw_Man_t *p, Aig_Obj_t *pObj, int f, int fBmc, Vec_Int_t *vPairs)
int	Ssw_ManSweepBmc (Ssw_Man_t *p)
int	Ssw_ManSweep (Ssw_Man_t *p)
void	Ssw_UniqueRegisterPairInfo (Ssw_Man_t *p)
	DECLARATIONS ///.
int	Ssw_ManUniqueOne (Ssw_Man_t *p, Aig_Obj_t *pRepr, Aig_Obj_t *pObj, int fVerbose)
int	Ssw_ManUniqueAddConstraint (Ssw_Man_t *p, Vec_Ptr_t *vCommon, int f1, int f2)

Typedef Documentation

Ssw_Cla_t

typedef struct Ssw_Cla_t_ Ssw_Cla_t

Definition at line 50 of file sswInt.h.

Ssw_Frm_t

typedef struct Ssw_Frm_t_ Ssw_Frm_t

Definition at line 48 of file sswInt.h.

Ssw_Man_t

typedef typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_ Ssw_Man_t

INCLUDES ///.

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

FileName [sswInt.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

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

] PARAMETERS /// BASIC TYPES ///

Definition at line 47 of file sswInt.h.

Ssw_Sat_t

typedef struct Ssw_Sat_t_ Ssw_Sat_t

Definition at line 49 of file sswInt.h.

Function Documentation

Ssw_ClassesCand1Num()

int Ssw_ClassesCand1Num ( Ssw_Cla_t * p )

extern

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file sswClass.c.

{
    return p->nCands1;
}

Here is the caller graph for this function:

Ssw_ClassesCheck()

void Ssw_ClassesCheck ( Ssw_Cla_t * p )

extern

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

Synopsis [Checks candidate equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file sswClass.c.

{
    Aig_Obj_t * pObj, * pPrev, ** ppClass;
    int i, k, nLits, nClasses, nCands1;
    nClasses = nLits = 0;
    Ssw_ManForEachClass( p, ppClass, k )
    {
        pPrev = NULL;
        assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
        Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
        {
            if ( i == 0 )
                assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
            else
            {
                assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
                assert( pPrev->Id < pObj->Id );
                nLits++;
            }
            pPrev = pObj;
        }
        nClasses++;
    }
    nCands1 = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
        nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj );
    assert( p->nLits == nLits );
    assert( p->nCands1 == nCands1 );
    assert( p->nClasses == nClasses );
}

Here is the caller graph for this function:

Ssw_ClassesClassNum()

int Ssw_ClassesClassNum ( Ssw_Cla_t * p )

extern

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file sswClass.c.

{
    return p->nClasses;
}

Here is the caller graph for this function:

Ssw_ClassesClearRefined()

void Ssw_ClassesClearRefined ( Ssw_Cla_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 243 of file sswClass.c.

{
    Vec_PtrClear( p->vRefined );
}

Here is the caller graph for this function:

Ssw_ClassesCollectClass()

void Ssw_ClassesCollectClass ( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass )

extern

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file sswClass.c.

{
    int i;
    Vec_PtrClear( vClass );
    if ( p->pId2Class[pRepr->Id] == NULL )
        return;
    assert( p->pClassSizes[pRepr->Id] > 1 );
    for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
        Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
}

Here is the caller graph for this function:

Ssw_ClassesGetRefined()

Vec_Ptr_t * Ssw_ClassesGetRefined ( Ssw_Cla_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file sswClass.c.

{
    return p->vRefined;
}

Ssw_ClassesLitNum()

int Ssw_ClassesLitNum ( Ssw_Cla_t * p )

extern

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file sswClass.c.

{
    return p->nLits;
}

Here is the caller graph for this function:

Ssw_ClassesPrepare()

Ssw_Cla_t * Ssw_ClassesPrepare ( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose )

extern

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 596 of file sswClass.c.

{
//    int nFrames =  4;
//    int nWords  =  1;
//    int nIters  = 16;
 
//    int nFrames = 32;
//    int nWords  =  4;
//    int nIters  =  0;
 
    int nFrames =  Abc_MaxInt( nFramesK, 4 );
    int nWords  =  2;
    int nIters  = 16;
    Ssw_Cla_t * p;
    Ssw_Sml_t * pSml;
    Vec_Ptr_t * vCands;
    Aig_Obj_t * pObj;
    int i, k, RetValue;
    abctime clk;
 
    // start the classes
    p = Ssw_ClassesStart( pAig );
    p->fConstCorr = fConstCorr;
 
    // perform sequential simulation
clk = Abc_Clock();
    pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
if ( fVerbose )
{
    Abc_Print( 1, "Allocated %.2f MB to store simulation information.\n",
        1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
    Abc_Print( 1, "Initial simulation of %d frames with %d words.     ", nFrames, nWords );
    ABC_PRT( "Time", Abc_Clock() - clk );
}
 
    // set comparison procedures
clk = Abc_Clock();
    Ssw_ClassesSetData( 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 );
 
    // collect nodes to be considered as candidates
    vCands = Vec_PtrAlloc( 1000 );
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Saig_ObjIsLo(p->pAig, pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                continue;
            // skip the node with more that the given number of levels
            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                continue;
        }
        Vec_PtrPush( vCands, pObj );
    }
 
    // this change will consider all PO drivers
    if ( fOutputCorr )
    {
        Vec_PtrClear( vCands );
        Aig_ManForEachObj( p->pAig, pObj, i )
            pObj->fMarkB = 0;
        Saig_ManForEachPo( p->pAig, pObj, i )
            if ( Aig_ObjIsCand(Aig_ObjFanin0(pObj)) )
                Aig_ObjFanin0(pObj)->fMarkB = 1;
        Aig_ManForEachObj( p->pAig, pObj, i )
            if ( pObj->fMarkB )
                Vec_PtrPush( vCands, pObj );
        Aig_ManForEachObj( p->pAig, pObj, i )
            pObj->fMarkB = 0;
    }
 
    // allocate room for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_PtrSize(vCands) );
    p->pMemClassesFree = p->pMemClasses;
 
    // now it is time to refine the classes
    Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
if ( fVerbose )
{
    Abc_Print( 1, "Collecting candidate equivalence classes.        " );
ABC_PRT( "Time", Abc_Clock() - clk );
}
 
clk = Abc_Clock();
    // perform iterative refinement using simulation
    for ( i = 1; i < nIters; i++ )
    {
        // collect const1 candidates
        Vec_PtrClear( vCands );
        Aig_ManForEachObj( p->pAig, pObj, k )
            if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
                Vec_PtrPush( vCands, pObj );
        assert( Vec_PtrSize(vCands) == p->nCands1 );
        // perform new round of simulation
        Ssw_SmlResimulateSeq( pSml );
        // check equivalence classes
        RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
        if ( RetValue == 0 )
            break;
    }
    Ssw_SmlStop( pSml );
    Vec_PtrFree( vCands );
if ( fVerbose )
{
    Abc_Print( 1, "Simulation of %d frames with %d words (%2d rounds). ",
        nFrames, nWords, i-1 );
    ABC_PRT( "Time", Abc_Clock() - clk );
}
    Ssw_ClassesCheck( p );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesPrepareFromReprs()

Ssw_Cla_t * Ssw_ClassesPrepareFromReprs ( Aig_Man_t * pAig )

extern

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 768 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj, * pRepr;
    int * pClassSizes, nEntries, i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // allocate memory for classes
    p->pMemClasses = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
    // count classes
    p->nCands1 = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
        {
            p->nCands1++;
            continue;
        }
        if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
        {
            if ( p->pClassSizes[pRepr->Id]++ == 0 )
                p->pClassSizes[pRepr->Id]++;
        }
    }
    // add nodes
    nEntries = 0;
    p->nClasses = 0;
    pClassSizes = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( p->pClassSizes[i] )
        {
            p->pId2Class[i] = p->pMemClasses + nEntries;
            nEntries += p->pClassSizes[i];
            p->pId2Class[i][pClassSizes[i]++] = pObj;
            p->nClasses++;
            continue;
        }
        if ( Ssw_ObjIsConst1Cand(pAig, pObj) )
            continue;
        if ( (pRepr = Aig_ObjRepr(pAig, pObj)) )
            p->pId2Class[pRepr->Id][pClassSizes[pRepr->Id]++] = pObj;
    }
    p->pMemClassesFree = p->pMemClasses + nEntries;
    p->nLits = nEntries - p->nClasses;
    assert( memcmp(pClassSizes, p->pClassSizes, sizeof(int)*Aig_ManObjNumMax(pAig)) == 0 );
    ABC_FREE( pClassSizes );
//    Abc_Print( 1, "After converting:\n" );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesPreparePairs()

Ssw_Cla_t * Ssw_ClassesPreparePairs ( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )

extern

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

Synopsis [Creates classes from the temporary representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 862 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t ** ppClassNew;
    Aig_Obj_t * pObj, * pRepr, * pPrev;
    int i, k, nTotalObjs, nEntries, Entry;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // count the number of entries in the classes
    nTotalObjs = 0;
    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
        nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0;
    // allocate memory for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nTotalObjs );
    // create constant-1 class
    if ( pvClasses[0] )
    Vec_IntForEachEntry( pvClasses[0], Entry, i )
    {
        assert( (i == 0) == (Entry == 0) );
        if ( i == 0 )
            continue;
        pObj = Aig_ManObj( pAig, Entry );
        Ssw_ObjSetConst1Cand( pAig, pObj );
        p->nCands1++;
    }
    // create classes
    nEntries = 0;
    for ( i = 1; i < Aig_ManObjNumMax(pAig); i++ )
    {
        if ( pvClasses[i] == NULL )
            continue;
        // get room for storing the class
        ppClassNew = p->pMemClasses + nEntries;
        nEntries  += Vec_IntSize( pvClasses[i] );
        // store the nodes of the class
        pPrev = pRepr = Aig_ManObj( pAig, Vec_IntEntry(pvClasses[i],0) );
        ppClassNew[0] = pRepr;
        Vec_IntForEachEntryStart( pvClasses[i], Entry, k, 1 )
        {
            pObj = Aig_ManObj( pAig, Entry );
            assert( pPrev->Id < pObj->Id );
            pPrev = pObj;
            ppClassNew[k] = pObj;
            Aig_ObjSetRepr( pAig, pObj, pRepr );
        }
        // create new class
        Ssw_ObjAddClass( p, pRepr, ppClassNew, Vec_IntSize(pvClasses[i]) );
    }
    // prepare room for new classes
    p->pMemClassesFree = p->pMemClasses + nEntries;
    Ssw_ClassesCheck( p );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesPreparePairsSimple()

Ssw_Cla_t * Ssw_ClassesPreparePairsSimple ( Aig_Man_t * pMiter, Vec_Int_t * vPairs )

extern

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

Synopsis [Creates classes from the temporary representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 928 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t ** ppClassNew;
    Aig_Obj_t * pObj, * pRepr;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pMiter );
    // allocate memory for classes
    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
    // create classes
    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
    {
        pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
        pObj  = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
        assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
        Aig_ObjSetRepr( pMiter, pObj, pRepr );
        // get room for storing the class
        ppClassNew = p->pMemClasses + i;
        ppClassNew[0] = pRepr;
        ppClassNew[1] = pObj;
        // create new class
        Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
    }
    // prepare room for new classes
    p->pMemClassesFree = NULL;
    Ssw_ClassesCheck( p );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesPrepareRehash()

int Ssw_ClassesPrepareRehash ( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr )

extern

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

Synopsis [Takes the set of const1 cands and rehashes them using sim info.]

Description []

SideEffects []

SeeAlso []

Definition at line 500 of file sswClass.c.

{
//    Aig_Man_t * pAig = p->pAig;
    Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
    Aig_Obj_t * pObj, * pTemp, * pRepr;
    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
 
    // allocate the hash table hashing simulation info into nodes
    nTableSize = Abc_PrimeCudd( Vec_PtrSize(vCands)/2 );
    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize );
    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
 
    // sort through the candidates
    nEntries = 0;
    p->nCands1 = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
    {
        assert( p->pClassSizes[pObj->Id] == 0 );
        Aig_ObjSetRepr( p->pAig, pObj, NULL );
        // check if the node belongs to the class of constant 1
        if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
        {
            Ssw_ObjSetConst1Cand( p->pAig, pObj );
            p->nCands1++;
            continue;
        }
        if ( fConstCorr )
            continue;
        // hash the node by its simulation info
        iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
        // add the node to the class
        if ( ppTable[iEntry] == NULL )
        {
            ppTable[iEntry] = pObj;
        }
        else
        {
            // set the representative of this node
            pRepr = ppTable[iEntry];
            Aig_ObjSetRepr( p->pAig, pObj, pRepr );
            // add node to the table
            if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
            { // this will be the second entry
                p->pClassSizes[pRepr->Id]++;
                nEntries++;
            }
            // add the entry to the list
            Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
            Ssw_ObjSetNext( ppNexts, pRepr, pObj );
            p->pClassSizes[pRepr->Id]++;
            nEntries++;
        }
    }
 
    // copy the entries into storage in the topological order
    nEntries2 = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vCands, pObj, i )
    {
        nNodes = p->pClassSizes[pObj->Id];
        // skip the nodes that are not representatives of non-trivial classes
        if ( nNodes == 0 )
            continue;
        assert( nNodes > 1 );
        // add the nodes to the class in the topological order
        ppClassNew = p->pMemClassesFree + nEntries2;
        ppClassNew[0] = pObj;
        for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp;
              pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
        {
            ppClassNew[nNodes-k] = pTemp;
        }
        // add the class of nodes
        p->pClassSizes[pObj->Id] = 0;
        Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
        // increment the number of entries
        nEntries2 += nNodes;
    }
    p->pMemClassesFree += nEntries2;
    assert( nEntries == nEntries2 );
    ABC_FREE( ppTable );
    ABC_FREE( ppNexts );
    // now it is time to refine the classes
    return Ssw_ClassesRefine( p, 1 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesPrepareSimple()

Ssw_Cla_t * Ssw_ClassesPrepareSimple ( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )

extern

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 724 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // go through the nodes
    p->nCands1 = 0;
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( fLatchCorr )
        {
            if ( !Saig_ObjIsLo(pAig, pObj) )
                continue;
        }
        else
        {
            if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
                continue;
            // skip the node with more that the given number of levels
            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                continue;
        }
        Ssw_ObjSetConst1Cand( pAig, pObj );
        p->nCands1++;
    }
    // allocate room for classes
    p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesPrepareTargets()

Ssw_Cla_t * Ssw_ClassesPrepareTargets ( Aig_Man_t * pAig )

extern

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 831 of file sswClass.c.

{
    Ssw_Cla_t * p;
    Aig_Obj_t * pObj;
    int i;
    // start the classes
    p = Ssw_ClassesStart( pAig );
    // go through the nodes
    p->nCands1 = 0;
    Saig_ManForEachPo( pAig, pObj, i )
    {
        Ssw_ObjSetConst1Cand( pAig, Aig_ObjFanin0(pObj) );
        p->nCands1++;
    }
    // allocate room for classes
    p->pMemClassesFree = p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, p->nCands1 );
//    Ssw_ClassesPrint( p, 0 );
    return p;
}

Here is the call graph for this function:

Ssw_ClassesPrint()

void Ssw_ClassesPrint ( Ssw_Cla_t * p, int fVeryVerbose )

extern

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 414 of file sswClass.c.

{
    Aig_Obj_t ** ppClass;
    Aig_Obj_t * pObj;
    int i;
    Abc_Print( 1, "Equiv classes: Const1 = %5d. Class = %5d. Lit = %5d.\n",
        p->nCands1, p->nClasses, p->nCands1+p->nLits );
    if ( !fVeryVerbose )
        return;
    Abc_Print( 1, "Constants { " );
    Aig_ManForEachObj( p->pAig, pObj, i )
        if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
            Abc_Print( 1, "%d(%d,%d,%d) ", pObj->Id, pObj->Level,
            Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
    Abc_Print( 1, "}\n" );
    Ssw_ManForEachClass( p, ppClass, i )
    {
        Abc_Print( 1, "%3d (%3d) : ", i, p->pClassSizes[i] );
        Ssw_ClassesPrintOne( p, ppClass[0] );
    }
    Abc_Print( 1, "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesReadAig()

Aig_Man_t * Ssw_ClassesReadAig ( Ssw_Cla_t * p )

extern

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file sswClass.c.

{
    return p->pAig;
}

Ssw_ClassesReadClass()

Aig_Obj_t ** Ssw_ClassesReadClass ( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )

extern

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file sswClass.c.

{
    if ( p->pId2Class[pRepr->Id] == NULL )
        return NULL;
    assert( p->pId2Class[pRepr->Id] != NULL );
    assert( p->pClassSizes[pRepr->Id] > 1 );
    *pnSize = p->pClassSizes[pRepr->Id];
    return p->pId2Class[pRepr->Id];
}

Here is the caller graph for this function:

Ssw_ClassesRefine()

int Ssw_ClassesRefine ( Ssw_Cla_t * p, int fRecursive )

extern

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

Synopsis [Refines the classes after simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1034 of file sswClass.c.

{
    Aig_Obj_t ** ppClass;
    int i, nRefis = 0;
    Ssw_ManForEachClass( p, ppClass, i )
        nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], fRecursive );
    return nRefis;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesRefineConst1()

int Ssw_ClassesRefineConst1 ( Ssw_Cla_t * p, int fRecursive )

extern

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

Synopsis [Refine the group of constant 1 nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1119 of file sswClass.c.

{
    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
    int i;
    // collect the nodes to be refined
    Vec_PtrClear( p->vClassNew );
    for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
        if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
        {
            pObj = Aig_ManObj( p->pAig, i );
            if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
            {
                Vec_PtrPush( p->vClassNew, pObj );
//                Vec_PtrPush( p->vRefined, pObj );
            }
        }
    // check if there is a new class
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
    if ( p->fConstCorr )
    {
        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
            Aig_ObjSetRepr( p->pAig, pObj, NULL );
        return 1;
    }
    p->nCands1 -= Vec_PtrSize(p->vClassNew);
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
    Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
    if ( Vec_PtrSize(p->vClassNew) == 1 )
        return 1;
    // create a new class composed of these nodes
    ppClassNew = p->pMemClassesFree;
    p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        ppClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }
    Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
    // refine them recursively
    if ( fRecursive )
        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesRefineConst1Group()

int Ssw_ClassesRefineConst1Group ( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive )

extern

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

Synopsis [Refine the group of constant 1 nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1074 of file sswClass.c.

{
    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
    int i;
    if ( Vec_PtrSize(vRoots) == 0 )
        return 0;
    // collect the nodes to be refined
    Vec_PtrClear( p->vClassNew );
    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
        if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
            Vec_PtrPush( p->vClassNew, pObj );
    // check if there is a new class
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
    p->nCands1 -= Vec_PtrSize(p->vClassNew);
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
    Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
    if ( Vec_PtrSize(p->vClassNew) == 1 )
        return 1;
    // create a new class composed of these nodes
    ppClassNew = p->pMemClassesFree;
    p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        ppClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }
    Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
    // refine them recursively
    if ( fRecursive )
        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesRefineGroup()

int Ssw_ClassesRefineGroup ( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive )

extern

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

Synopsis [Refines the classes after simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1054 of file sswClass.c.

{
    Aig_Obj_t * pObj;
    int i, nRefis = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i )
        nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive );
    return nRefis;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesRefineOneClass()

int Ssw_ClassesRefineOneClass ( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive )

extern

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

Synopsis [Iteratively refines the classes after simulation.]

Description [Returns the number of refinements performed.]

SideEffects []

SeeAlso []

Definition at line 970 of file sswClass.c.

{
    Aig_Obj_t ** pClassOld, ** pClassNew;
    Aig_Obj_t * pObj, * pReprNew;
    int i;
 
    // split the class
    Vec_PtrClear( p->vClassOld );
    Vec_PtrClear( p->vClassNew );
    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
        if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
            Vec_PtrPush( p->vClassOld, pObj );
        else
            Vec_PtrPush( p->vClassNew, pObj );
    // check if splitting happened
    if ( Vec_PtrSize(p->vClassNew) == 0 )
        return 0;
    // remember that this class is refined
//    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
//        Vec_PtrPush( p->vRefined, pObj );
 
    // get the new representative
    pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
    assert( Vec_PtrSize(p->vClassOld) > 0 );
    assert( Vec_PtrSize(p->vClassNew) > 0 );
 
    // create old class
    pClassOld = Ssw_ObjRemoveClass( p, pReprOld );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassOld, pObj, i )
    {
        pClassOld[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
    }
    // create new class
    pClassNew = pClassOld + i;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
    {
        pClassNew[i] = pObj;
        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
    }
 
    // put classes back
    if ( Vec_PtrSize(p->vClassOld) > 1 )
        Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
    if ( Vec_PtrSize(p->vClassNew) > 1 )
        Ssw_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
 
    // check if the class should be recursively refined
    if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesRemoveNode()

void Ssw_ClassesRemoveNode ( Ssw_Cla_t * p, Aig_Obj_t * pObj )

extern

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 448 of file sswClass.c.

{
    Aig_Obj_t * pRepr, * pTemp;
    assert( p->pClassSizes[pObj->Id] == 0 );
    assert( p->pId2Class[pObj->Id] == NULL );
    pRepr = Aig_ObjRepr( p->pAig, pObj );
    assert( pRepr != NULL );
//    Vec_PtrPush( p->vRefined, pObj );
    if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
    {
        assert( p->pClassSizes[pRepr->Id] == 0 );
        assert( p->pId2Class[pRepr->Id] == NULL );
        Aig_ObjSetRepr( p->pAig, pObj, NULL );
        p->nCands1--;
        return;
    }
//    Vec_PtrPush( p->vRefined, pRepr );
    Aig_ObjSetRepr( p->pAig, pObj, NULL );
    assert( p->pId2Class[pRepr->Id][0] == pRepr );
    assert( p->pClassSizes[pRepr->Id] >= 2 );
    if ( p->pClassSizes[pRepr->Id] == 2 )
    {
        p->pId2Class[pRepr->Id] = NULL;
        p->nClasses--;
        p->pClassSizes[pRepr->Id] = 0;
        p->nLits--;
    }
    else
    {
        int i, k = 0;
        // remove the entry from the class
        Ssw_ClassForEachNode( p, pRepr, pTemp, i )
            if ( pTemp != pObj )
                p->pId2Class[pRepr->Id][k++] = pTemp;
        assert( k + 1 == p->pClassSizes[pRepr->Id] );
        // reduce the class
        p->pClassSizes[pRepr->Id]--;
        p->nLits--;
    }
}

Here is the caller graph for this function:

Ssw_ClassesSetData()

void Ssw_ClassesSetData ( Ssw_Cla_t * p, void * pManData, unsigned(* pFuncNodeHash )(void *, Aig_Obj_t *), int(* pFuncNodeIsConst )(void *, Aig_Obj_t *), int(* pFuncNodesAreEqual )(void *, Aig_Obj_t *, Aig_Obj_t *) )

extern

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file sswClass.c.

{
    p->pManData           = pManData;
    p->pFuncNodeHash      = pFuncNodeHash;
    p->pFuncNodeIsConst   = pFuncNodeIsConst;
    p->pFuncNodesAreEqual = pFuncNodesAreEqual;
}

Here is the caller graph for this function:

Ssw_ClassesStart()

Ssw_Cla_t * Ssw_ClassesStart ( Aig_Man_t * pAig )

extern

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

Synopsis [Starts representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file sswClass.c.

{
    Ssw_Cla_t * p;
    p = ABC_ALLOC( Ssw_Cla_t, 1 );
    memset( p, 0, sizeof(Ssw_Cla_t) );
    p->pAig         = pAig;
    p->pId2Class    = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
    p->pClassSizes  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
    p->vClassOld    = Vec_PtrAlloc( 100 );
    p->vClassNew    = Vec_PtrAlloc( 100 );
    p->vRefined     = Vec_PtrAlloc( 1000 );
    if ( pAig->pReprs == NULL )
        Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ClassesStop()

void Ssw_ClassesStop ( Ssw_Cla_t * p )

extern

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

Synopsis [Stop representation of equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file sswClass.c.

{
    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
    Vec_PtrFree( p->vRefined );
    ABC_FREE( p->pId2Class );
    ABC_FREE( p->pClassSizes );
    ABC_FREE( p->pMemClasses );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Ssw_CnfGetNodeValue()

int Ssw_CnfGetNodeValue ( Ssw_Sat_t * p, Aig_Obj_t * pObj )

extern

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file sswCnf.c.

{
    int Value0, Value1, nVarNum;
    assert( !Aig_IsComplement(pObj) );
    nVarNum = Ssw_ObjSatNum( p, pObj );
    if ( nVarNum > 0 )
        return sat_solver_var_value( p->pSat, nVarNum );
//    if ( pObj->fMarkA == 1 )
//        return 0;
    if ( Aig_ObjIsCi(pObj) )
        return 0;
    assert( Aig_ObjIsNode(pObj) );
    Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
    Value0 ^= Aig_ObjFaninC0(pObj);
    Value1 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin1(pObj) );
    Value1 ^= Aig_ObjFaninC1(pObj);
    return Value0 & Value1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_CnfNodeAddToSolver()

void Ssw_CnfNodeAddToSolver ( Ssw_Sat_t * p, Aig_Obj_t * pObj )

extern

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file sswCnf.c.

{
    Vec_Ptr_t * vFrontier;
    Aig_Obj_t * pNode, * pFanin;
    int i, k, fUseMuxes = 1;
    // quit if CNF is ready
    if ( Ssw_ObjSatNum(p,pObj) )
        return;
    // start the frontier
    vFrontier = Vec_PtrAlloc( 100 );
    Ssw_ObjAddToFrontier( p, pObj, vFrontier );
    // explore nodes in the frontier
    Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
    {
        // create the supergate
        assert( Ssw_ObjSatNum(p,pNode) );
        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
        {
            Vec_PtrClear( p->vFanins );
            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
            Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
                Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Ssw_AddClausesMux( p, pNode );
        }
        else
        {
            Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins );
            Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
                Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
            Ssw_AddClausesSuper( p, pNode, p->vFanins );
        }
        assert( Vec_PtrSize(p->vFanins) > 1 );
    }
    Vec_PtrFree( vFrontier );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_FilterUsingSemi()

int Ssw_FilterUsingSemi ( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )

extern

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

Synopsis [Returns 1 if one of the targets has failed.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file sswSemi.c.

{
    Ssw_Sem_t * p;
    int RetValue, Frames, Iter;
    abctime clk = Abc_Clock();
    p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
    if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
    {
        assert( 0 );
        Ssw_SemManStop( p );
        return 1;
    }
    if ( fVerbose )
    {
        Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d.  ConfMax = %6d. FramesMax = %6d.\n",
            Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
            Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
    }
    RetValue = 0;
    for ( Iter = 0; Iter < p->nPatterns; Iter++ )
    {
clk = Abc_Clock();
        pMan->pMSat = Ssw_SatStart( 0 );
        Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
        if ( fVerbose )
        {
            Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
                Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
                Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
                p->pMan->nSatFailsReal? "f" : " " );
            ABC_PRT( "T", Abc_Clock() - clk );
        }
        Ssw_ManCleanup( p->pMan );
        if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
        {
            Abc_Print( 1, "Target is hit!!!\n" );
            RetValue = 1;
        }
        if ( p->nPatterns >= p->nPatternsAlloc )
            break;
    }
    Ssw_SemManStop( p );
 
    pMan->nStrangers = 0;
    pMan->nSatCalls = 0;
    pMan->nSatProof = 0;
    pMan->nSatFailsReal = 0;
    pMan->nSatCallsUnsat = 0;
    pMan->nSatCallsSat = 0;
    pMan->timeSimSat = 0;
    pMan->timeSat = 0;
    pMan->timeSatSat = 0;
    pMan->timeSatUnsat = 0;
    pMan->timeSatUndec = 0;
    return RetValue;
}

Here is the call graph for this function:

Ssw_FramesWithClasses()

Aig_Man_t * Ssw_FramesWithClasses ( Ssw_Man_t * p )

extern

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

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file sswAig.c.

{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
    int i, f, iLits;
    assert( p->pFrames == NULL );
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
    p->nConstrTotal = p->nConstrReduced = 0;
 
    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
    // create latches for the first frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // add timeframes
    iLits = 0;
    if ( p->pPars->nSkip )
        srand(1);
    for ( f = 0; f < p->pPars->nFramesK; f++ )
    {
        // map constants and PIs
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjNew = Aig_ObjCreateCi(pFrames);
            pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
        }
        // set the constraints on the latch outputs
        Saig_ManForEachLo( p->pAig, pObj, i )
            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
        // add internal nodes of this frame
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
        }
        // transfer to the primary outputs
        Aig_ManForEachCo( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
        // transfer latch input to the latch outputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
            Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjFrame(p, pObjLi,f) );
    }
    assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
    // add the POs for the latch outputs of the last frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Aig_ObjCreateCo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
    // remove dangling nodes
    Aig_ManCleanup( pFrames );
    // make sure the satisfying assignment is node assigned
    assert( pFrames->pData == NULL );
//Aig_ManShow( pFrames, 0, NULL );
    return pFrames;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_FrmStart()

Ssw_Frm_t * Ssw_FrmStart ( Aig_Man_t * pAig )

extern

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

FileName [sswAig.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [AIG manipulation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswAig.c.

{
    Ssw_Frm_t * p;
    p = ABC_ALLOC( Ssw_Frm_t, 1 );
    memset( p, 0, sizeof(Ssw_Frm_t) );
    p->pAig          = pAig;
    p->nObjs         = Aig_ManObjNumMax( pAig );
    p->nFrames       = 0;
    p->pFrames       = NULL;
    p->vAig2Frm      = Vec_PtrAlloc( 0 );
    Vec_PtrFill( p->vAig2Frm, 2 * p->nObjs, NULL );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_FrmStop()

void Ssw_FrmStop ( Ssw_Frm_t * p )

extern

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file sswAig.c.

{
    if ( p->pFrames )
        Aig_ManStop( p->pFrames );
    Vec_PtrFree( p->vAig2Frm );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManCleanup()

void Ssw_ManCleanup ( Ssw_Man_t * p )

extern

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

Synopsis [Frees the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file sswMan.c.

{
//    Aig_ManCleanMarkAB( p->pAig );
    assert( p->pMSat == NULL );
    if ( p->pFrames )
    {
        Aig_ManCleanMarkAB( p->pFrames );
        Aig_ManStop( p->pFrames );
        p->pFrames = NULL;
        memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
    }
    if ( p->vSimInfo )
    {
        Vec_PtrFree( p->vSimInfo );
        p->vSimInfo = NULL;
    }
    p->nConstrTotal = 0;
    p->nConstrReduced = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManCreate()

Ssw_Man_t * Ssw_ManCreate ( Aig_Man_t * pAig, Ssw_Pars_t * pPars )

extern

DECLARATIONS ///.

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

FileName [sswMan.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

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

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

Synopsis [Creates the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswMan.c.

{
    Ssw_Man_t * p;
    // prepare the sequential AIG
    assert( Saig_ManRegNum(pAig) > 0 );
    Aig_ManFanoutStart( pAig );
    Aig_ManSetCioIds( pAig );
    // create interpolation manager
    p = ABC_ALLOC( Ssw_Man_t, 1 );
    memset( p, 0, sizeof(Ssw_Man_t) );
    p->pPars         = pPars;
    p->pAig          = pAig;
    p->nFrames       = pPars->nFramesK + 1;
    p->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
    p->vCommon       = Vec_PtrAlloc( 100 );
    p->iOutputLit    = -1;
    // allocate storage for sim pattern
    p->nPatWords     = Abc_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
    p->pPatWords     = ABC_CALLOC( unsigned, p->nPatWords );
    // other
    p->vNewLos       = Vec_PtrAlloc( 100 );
    p->vNewPos       = Vec_IntAlloc( 100 );
    p->vResimConsts  = Vec_PtrAlloc( 100 );
    p->vResimClasses = Vec_PtrAlloc( 100 );
//    p->pPars->fVerbose = 1;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManGetSatVarValue()

int Ssw_ManGetSatVarValue ( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )

extern

DECLARATIONS ///.

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

FileName [sswSweep.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [One round of SAT sweeping.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Retrives value of the PI in the original AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file sswSweep.c.

{
    int fUseNoBoundary = 0;
    Aig_Obj_t * pObjFraig;
    int Value;
//    assert( Aig_ObjIsCi(pObj) );
    pObjFraig = Ssw_ObjFrame( p, pObj, f );
    if ( fUseNoBoundary )
    {
        Value = Ssw_CnfGetNodeValue( p->pMSat, Aig_Regular(pObjFraig) );
        Value ^= Aig_IsComplement(pObjFraig);
    }
    else
    {
        int nVarNum = Ssw_ObjSatNum( p->pMSat, Aig_Regular(pObjFraig) );
        Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pMSat->pSat, nVarNum ));
    }
 
//    Value = (Aig_IsComplement(pObjFraig) ^ ((!nVarNum)? 0 : sat_solver_var_value( p->pSat, nVarNum )));
//    Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
    if ( p->pPars->fPolarFlip )
    {
        if ( Aig_Regular(pObjFraig)->fPhase )  Value ^= 1;
    }
    return Value;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManLoadSolver()

void Ssw_ManLoadSolver ( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )

extern

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

Synopsis [Loads logic cones and relevant constraints.]

Description [Both pRepr and pObj are objects of the AIG. The result is the current SAT solver loaded with the logic cones for pRepr and pObj corresponding to them in the frames, as well as all the relevant constraints.]

SideEffects []

SeeAlso []

Definition at line 142 of file sswDyn.c.

{
    Aig_Obj_t * pObjFrames, * pReprFrames;
    Aig_Obj_t * pTemp, * pObj0, * pObj1;
    int i, iConstr, RetValue;
 
    assert( pRepr != pObj );
    // get the corresponding frames nodes
    pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) );
    pObjFrames  = Aig_Regular( Ssw_ObjFrame( p, pObj,  p->pPars->nFramesK ) );
    assert( pReprFrames != pObjFrames );
 /*
    // compute the AIG support
    Vec_PtrClear( p->vNewLos );
    Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
    Ssw_ManCollectPis_rec( pObj,  p->vNewLos );
    // add logic cones for register outputs
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
    {
        pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
        Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
    }
*/
    // add cones for the nodes
    Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
    Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );
 
    // compute the frames support
    Vec_PtrClear( p->vNewLos );
    Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
    Ssw_ManCollectPis_rec( pObjFrames,  p->vNewLos );
    // these nodes include both nodes corresponding to PIs and LOs
    // (the nodes corresponding to PIs should be labeled with fMarkB!)
 
    // collect the related constraint POs
    Vec_IntClear( p->vNewPos );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
        Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
    // check if the corresponding pairs are added
    Vec_IntForEachEntry( p->vNewPos, iConstr, i )
    {
        pObj0 = Aig_ManCo( p->pFrames, 2*iConstr   );
        pObj1 = Aig_ManCo( p->pFrames, 2*iConstr+1 );
//        if ( pObj0->fMarkB && pObj1->fMarkB )
        if ( pObj0->fMarkB || pObj1->fMarkB )
        {
            pObj0->fMarkB = 1;
            pObj1->fMarkB = 1;
            Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) );
        }
    }
    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pMSat->pSat);
        assert( RetValue != 0 );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManRefineByConstrSim()

void Ssw_ManRefineByConstrSim ( Ssw_Man_t * p )

extern

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

Synopsis [Performs fraiging for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 247 of file sswConstr.c.

{
    Aig_Obj_t * pObj, * pObjLi;
    int f, i, iLits, RetValue1, RetValue2;
    int nFrames = Vec_IntSize(p->vInits) / Saig_ManPiNum(p->pAig);
    assert( Vec_IntSize(p->vInits) % Saig_ManPiNum(p->pAig) == 0 );
    // assign register outputs
    Saig_ManForEachLi( p->pAig, pObj, i )
        pObj->fMarkB = 0;
    // simulate the timeframes
    iLits = 0;
    for ( f = 0; f < nFrames; f++ )
    {
        // set the PI simulation information
        Aig_ManConst1(p->pAig)->fMarkB = 1;
        Saig_ManForEachPi( p->pAig, pObj, i )
            pObj->fMarkB = Vec_IntEntry( p->vInits, iLits++ );
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
            pObj->fMarkB = pObjLi->fMarkB;
        // simulate internal nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
            pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                         & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
        // assign the COs
        Aig_ManForEachCo( p->pAig, pObj, i )
            pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
        // check the outputs
        Saig_ManForEachPo( p->pAig, pObj, i )
        {
            if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
            {
                if ( pObj->fMarkB && Saig_ManConstrNum(p->pAig) )
                    Abc_Print( 1, "output %d failed in frame %d.\n", i, f );
            }
            else
            {
                if ( pObj->fMarkB && Saig_ManConstrNum(p->pAig) )
                    Abc_Print( 1, "constraint %d failed in frame %d.\n", i, f );
            }
        }
        // transfer
        if ( f == 0 )
        { // copy markB into phase
            Aig_ManForEachObj( p->pAig, pObj, i )
                pObj->fPhase = pObj->fMarkB;
        }
        else
        { // refine classes
            RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
            RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
        }
    }
    assert( iLits == Vec_IntSize(p->vInits) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManResimulateBit()

void Ssw_ManResimulateBit ( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )

extern

DECLARATIONS ///.

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

FileName [sswSimSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Performs resimulation using counter-examples.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswSimSat.c.

{
    Aig_Obj_t * pObj;
    int i, RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    // set the PI simulation information
    Aig_ManConst1(p->pAig)->fMarkB = 1;
    Aig_ManForEachCi( p->pAig, pObj, i )
        pObj->fMarkB = Abc_InfoHasBit( p->pPatWords, i );
    // simulate internal nodes
    Aig_ManForEachNode( p->pAig, pObj, i )
        pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                     & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
    // if repr is given, perform refinement
    if ( pRepr )
    {
        // check equivalence classes
        RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
        RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
        // make sure refinement happened
        if ( Aig_ObjIsConst1(pRepr) )
        {
            assert( RetValue1 );
            if ( RetValue1 == 0 )
                Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
        }
        else
        {
            assert( RetValue2 );
            if ( RetValue2 == 0 )
                Abc_Print( 1, "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
        }
    }
p->timeSimSat += Abc_Clock() - clk;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManResimulateWord()

void Ssw_ManResimulateWord ( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )

extern

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

Synopsis [Handle the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 92 of file sswSimSat.c.

{
    int RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    // set the PI simulation information
    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
    // simulate internal nodes
    Ssw_SmlSimulateOne( p->pSml );
    // check equivalence classes
    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
    // make sure refinement happened
    if ( Aig_ObjIsConst1(pRepr) )
    {
        assert( RetValue1 );
        if ( RetValue1 == 0 )
            Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
    }
    else
    {
        assert( RetValue2 );
        if ( RetValue2 == 0 )
            Abc_Print( 1, "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
    }
p->timeSimSat += Abc_Clock() - clk;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManStop()

void Ssw_ManStop ( Ssw_Man_t * p )

extern

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

Synopsis [Frees the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file sswMan.c.

{
    ABC_FREE( p->pVisited );
    if ( p->pPars->fVerbose )//&& p->pPars->nStepsMax == -1 )
        Ssw_ManPrintStats( p );
    if ( p->ppClasses )
        Ssw_ClassesStop( p->ppClasses );
    if ( p->pSml )
        Ssw_SmlStop( p->pSml );
    if ( p->vDiffPairs )
        Vec_IntFree( p->vDiffPairs );
    if ( p->vInits )
        Vec_IntFree( p->vInits );
    Vec_PtrFree( p->vResimConsts );
    Vec_PtrFree( p->vResimClasses );
    Vec_PtrFree( p->vNewLos );
    Vec_IntFree( p->vNewPos );
    Vec_PtrFree( p->vCommon );
    ABC_FREE( p->pNodeToFrames );
    ABC_FREE( p->pPatWords );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManSweep()

int Ssw_ManSweep ( Ssw_Man_t * p )

extern

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 373 of file sswSweep.c.

{
    static int Counter;
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObj2, * pObjNew;
    int nConstrPairs, i, f;
    abctime clk;
    Vec_Int_t * vObjPairs;
 
    // perform speculative reduction
clk = Abc_Clock();
    // create timeframes
    p->pFrames = Ssw_FramesWithClasses( p );
    // add constants
    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
    assert( (nConstrPairs & 1) == 0 );
    for ( i = 0; i < nConstrPairs; i += 2 )
    {
        pObj  = Aig_ManCo( p->pFrames, i   );
        pObj2 = Aig_ManCo( p->pFrames, i+1 );
        Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
    }
    // build logic cones for register inputs
    for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
    {
        pObj  = Aig_ManCo( p->pFrames, nConstrPairs + i );
        Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
    }
    sat_solver_simplify( p->pMSat->pSat );
 
    // map constants and PIs of the last frame
    f = p->pPars->nFramesK;
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
p->timeReduce += Abc_Clock() - clk;
 
    // sweep internal nodes
    p->fRefined = 0;
    Ssw_ClassesClearRefined( p->ppClasses );
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
    vObjPairs = (p->pPars->fEquivDump || p->pPars->fEquivDump2)? Vec_IntAlloc(1000) : NULL;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( p->pPars->fVerbose )
            Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Saig_ObjIsLo(p->pAig, pObj) )
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vObjPairs );
        else if ( Aig_ObjIsNode(pObj) )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vObjPairs );
        }
    }
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );
 
    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    if ( p->pPars->fEquivDump )
        Ssw_ManDumpEquivMiter( p->pAig, vObjPairs, Counter++, 1 );
    if ( p->pPars->fEquivDump2 && !p->fRefined )
        Ssw_ManDumpEquivMiter( p->pAig, vObjPairs, 0, 0 );
    Vec_IntFreeP( &vObjPairs );
    return p->fRefined;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManSweepBmc()

int Ssw_ManSweepBmc ( Ssw_Man_t * p )

extern

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file sswSweep.c.

{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
    int i, f;
    abctime clk;
clk = Abc_Clock();
 
    // start initialized timeframes
    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
 
    // sweep internal nodes
    p->fRefined = 0;
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
    for ( f = 0; f < p->pPars->nFramesK; f++ )
    {
        // map constants and PIs
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
        Saig_ManForEachPi( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
        // sweep flops
        Saig_ManForEachLo( p->pAig, pObj, i )
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
        // sweep internal nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            if ( p->pPars->fVerbose )
                Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
        }
        // quit if this is the last timeframe
        if ( f == p->pPars->nFramesK - 1 )
            break;
        // transfer latch input to the latch outputs
        Aig_ManForEachCo( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
        // build logic cones for register outputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
        {
            pObjNew = Ssw_ObjFrame( p, pObjLi, f );
            Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
            Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );//
        }
    }
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );
 
    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += Abc_Clock() - clk;
    return p->fRefined;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManSweepBmcConstr()

int Ssw_ManSweepBmcConstr ( Ssw_Man_t * p )

extern

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 498 of file sswConstr.c.

{
    Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
    int i, f, iLits;
    abctime clk;
clk = Abc_Clock();
 
    // start initialized timeframes
    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
 
    // build the constraint outputs
    iLits = 0;
    p->fRefined = 0;
    for ( f = 0; f < p->pPars->nFramesK; f++ )
    {
        // map constants and PIs
        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjNew = Aig_ObjCreateCi(p->pFrames);
            pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
        }
        // build the constraint cones
        Saig_ManForEachPo( p->pAig, pObj, i )
        {
            if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
                continue;
            pObjNew = Ssw_ManSweepBmcConstr_rec( p, Aig_ObjFanin0(pObj), f );
            pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
            if ( Aig_Regular(pObjNew) == Aig_ManConst1(p->pFrames) )
            {
                assert( Aig_IsComplement(pObjNew) );
                continue;
            }
            Ssw_NodesAreConstrained( p, pObjNew, Aig_ManConst0(p->pFrames) );
        }        
        // sweep flops
        Saig_ManForEachLo( p->pAig, pObj, i )
            p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 );
        // sweep internal nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 );
        }
        // quit if this is the last timeframe
        if ( f == p->pPars->nFramesK - 1 )
            break;
        // transfer latch input to the latch outputs
        Aig_ManForEachCo( p->pAig, pObj, i )
            Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
        // build logic cones for register outputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
        {
            pObjNew = Ssw_ObjFrame( p, pObjLi, f );
            Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
            Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );//
        }
    }
    assert( Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
 
    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
p->timeBmc += Abc_Clock() - clk;
    return p->fRefined;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManSweepConstr()

int Ssw_ManSweepConstr ( Ssw_Man_t * p )

extern

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 621 of file sswConstr.c.

{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObj2, * pObjNew;
    int nConstrPairs, i, f, iLits;
    abctime clk;
//Ssw_ManPrintPolarity( p->pAig );
 
    // perform speculative reduction
clk = Abc_Clock();
    // create timeframes
    p->pFrames = Ssw_FramesWithClasses( p );
    // add constants
    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
    assert( (nConstrPairs & 1) == 0 );
    for ( i = 0; i < nConstrPairs; i += 2 )
    {
        pObj  = Aig_ManCo( p->pFrames, i   );
        pObj2 = Aig_ManCo( p->pFrames, i+1 );
        Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
    }
    // build logic cones for register inputs
    for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
    {
        pObj  = Aig_ManCo( p->pFrames, nConstrPairs + i );
        Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
    }
 
    // map constants and PIs of the last frame
    f = p->pPars->nFramesK;
//    iLits = 0;
    iLits = f * Saig_ManPiNum(p->pAig);
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
    {
        pObjNew = Aig_ObjCreateCi(p->pFrames);
        pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
        Ssw_ObjSetFrame( p, pObj, f, pObjNew );
    }
    assert( Vec_IntSize(p->vInits) == iLits );
p->timeReduce += Abc_Clock() - clk;
 
    // add constraints to all timeframes
    for ( f = 0; f <= p->pPars->nFramesK; f++ )
    {
        Saig_ManForEachPo( p->pAig, pObj, i )
        {
            if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
                continue;
            Ssw_FramesWithClasses_rec( p, Aig_ObjFanin0(pObj), f );
//            if ( Aig_Regular(Ssw_ObjChild0Fra(p,pObj,f)) == Aig_ManConst1(p->pFrames) )
            if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst0(p->pFrames) )
                continue;
            assert( Ssw_ObjChild0Fra(p,pObj,f) != Aig_ManConst1(p->pFrames) );
            if ( Ssw_ObjChild0Fra(p,pObj,f) == Aig_ManConst1(p->pFrames) )
            {
                Abc_Print( 1, "Polarity violation.\n" );
                continue;
            }
            Ssw_NodesAreConstrained( p, Ssw_ObjChild0Fra(p,pObj,f), Aig_ManConst0(p->pFrames) );
        }
    }
    f = p->pPars->nFramesK;
    // clean the solver
    sat_solver_simplify( p->pMSat->pSat );
 
 
    // sweep internal nodes
    p->fRefined = 0;
    Ssw_ClassesClearRefined( p->ppClasses );
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( p->pPars->fVerbose )
            Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Saig_ObjIsLo(p->pAig, pObj) )
            p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
        else if ( Aig_ObjIsNode(pObj) )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 0 );
        }
    }
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );
    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    return p->fRefined;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManSweepDyn()

int Ssw_ManSweepDyn ( Ssw_Man_t * p )

extern

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 373 of file sswDyn.c.

{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew;
    int i, f;
    abctime clk;
 
    // perform speculative reduction
clk = Abc_Clock();
    // create timeframes
    p->pFrames = Ssw_FramesWithClasses( p );
    Aig_ManFanoutStart( p->pFrames );
    p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames );
 
    // map constants and PIs of the last frame
    f = p->pPars->nFramesK;
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
    Aig_ManSetCioIds( p->pFrames );
    // label nodes corresponding to primary inputs
    Ssw_ManLabelPiNodes( p );
p->timeReduce += Abc_Clock() - clk;
 
    // prepare simulation info
    assert( p->vSimInfo == NULL );
    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
 
    // sweep internal nodes
    p->fRefined = 0;
    Ssw_ClassesClearRefined( p->ppClasses );
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
    p->iNodeStart = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( p->iNodeStart == 0 )
            p->iNodeStart = i;
        if ( p->pPars->fVerbose )
            Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Saig_ObjIsLo(p->pAig, pObj) )
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
        else if ( Aig_ObjIsNode(pObj) )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
        }
        // check if it is time to recycle the solver
        if ( p->pMSat->pSat == NULL ||
            (p->pPars->nSatVarMax2 &&
             p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
             p->nRecycleCalls > p->pPars->nRecycleCalls2) )
        {
            // resimulate
            if ( p->nPatterns > 0 )
            {
                p->iNodeLast = i;
                if ( p->pPars->fLocalSim )
                    Ssw_ManSweepResimulateDynLocal( p, f );
                else
                    Ssw_ManSweepResimulateDyn( p, f );
                p->iNodeStart = i+1;
            }
//                Abc_Print( 1, "Recycling SAT solver with %d vars and %d calls.\n", 
//                    p->pMSat->nSatVars, p->nRecycleCalls );
//            Aig_ManCleanMarkAB( p->pAig );
            Aig_ManCleanMarkAB( p->pFrames );
            // label nodes corresponding to primary inputs
            Ssw_ManLabelPiNodes( p );
            // replace the solver
            if ( p->pMSat )
            {
                p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
                p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
                Ssw_SatStop( p->pMSat );
                p->nRecycles++;
                p->nRecyclesTotal++;
                p->nRecycleCalls = 0;
            }
            p->pMSat = Ssw_SatStart( 0 );
            assert( p->nPatterns == 0 );
        }
        // resimulate
        if ( p->nPatterns == 32 )
        {
            p->iNodeLast = i;
            if ( p->pPars->fLocalSim )
                Ssw_ManSweepResimulateDynLocal( p, f );
            else
                Ssw_ManSweepResimulateDyn( p, f );
            p->iNodeStart = i+1;
        }
    }
    // resimulate
    if ( p->nPatterns > 0 )
    {
        p->iNodeLast = i;
        if ( p->pPars->fLocalSim )
            Ssw_ManSweepResimulateDynLocal( p, f );
        else
            Ssw_ManSweepResimulateDyn( p, f );
    }
    // collect stats
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );
 
    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    return p->fRefined;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManSweepLatch()

int Ssw_ManSweepLatch ( Ssw_Man_t * p )

extern

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

Synopsis [Performs one iteration of sweeping latches.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file sswLcorr.c.

{
//    Bar_Progress_t * pProgress = NULL;
    Vec_Ptr_t * vClass;
    Aig_Obj_t * pObj, * pRepr, * pTemp;
    int i, k;
 
    // start the timeframe
    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
    // map constants and PIs
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(p->pFrames) );
 
    // implement equivalence classes
    Saig_ManForEachLo( p->pAig, pObj, i )
    {
        pRepr = Aig_ObjRepr( p->pAig, pObj );
        if ( pRepr == NULL )
        {
            pTemp = Aig_ObjCreateCi(p->pFrames);
            pTemp->pData = pObj;
        }
        else
            pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
        Ssw_ObjSetFrame( p, pObj, 0, pTemp );
    }
    Aig_ManSetCioIds( p->pFrames );
 
    // prepare simulation info
    assert( p->vSimInfo == NULL );
    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
 
    // go through the registers
//    if ( p->pPars->fVerbose )
//        pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
    vClass = Vec_PtrAlloc( 100 );
    p->fRefined = 0;
    p->nCallsCount = p->nCallsSat = p->nCallsUnsat = 0;
    Saig_ManForEachLo( p->pAig, pObj, i )
    {
//        if ( p->pPars->fVerbose )
//            Bar_ProgressUpdate( pProgress, i, NULL );
        // consider the case of constant candidate
        if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
            Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj );
        else
        {
            // consider the case of equivalence class
            Ssw_ClassesCollectClass( p->ppClasses, pObj, vClass );
            if ( Vec_PtrSize(vClass) == 0 )
                continue;
            // try to prove equivalences in this class
            Vec_PtrForEachEntry( Aig_Obj_t *, vClass, pTemp, k )
                if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
                {
                    Ssw_ManSweepLatchOne( p, pObj, pTemp );
                    if ( p->nPatterns == 32 )
                        break;
                }
        }
        // resimulate
        if ( p->nPatterns == 32 )
            Ssw_ManSweepResimulate( p );
        // attempt recycling the SAT solver
        if ( p->pPars->nSatVarMax &&
             p->pMSat->nSatVars > p->pPars->nSatVarMax &&
             p->nRecycleCalls > p->pPars->nRecycleCalls )
        {
            p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
            p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
            Ssw_SatStop( p->pMSat );
            p->pMSat = Ssw_SatStart( 0 );
            p->nRecycles++;
            p->nRecycleCalls = 0;
        }
    }
//    ABC_PRT( "reduce", p->timeReduce );
//    Aig_TableProfile( p->pFrames );
//    Abc_Print( 1, "And gates = %d\n", Aig_ManNodeNum(p->pFrames) );
    // resimulate
    if ( p->nPatterns > 0 )
        Ssw_ManSweepResimulate( p );
    // cleanup
    Vec_PtrFree( vClass );
//    if ( p->pPars->fVerbose )
//        Bar_ProgressStop( pProgress );
 
    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    return p->fRefined;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManSweepNode()

int Ssw_ManSweepNode ( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs )

extern

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

Synopsis [Performs fraiging for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 187 of file sswSweep.c.

{
    Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
    int RetValue;
    abctime clk;
    // get representative of this class
    pObjRepr = Aig_ObjRepr( p->pAig, pObj );
    if ( pObjRepr == NULL )
        return 0;
    // get the fraiged node
    pObjFraig = Ssw_ObjFrame( p, pObj, f );
    // get the fraiged representative
    pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
    // check if constant 0 pattern distinquishes these nodes
    assert( pObjFraig != NULL && pObjReprFraig != NULL );
    assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
    // if the fraiged nodes are the same, return
    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
        return 0;
    // add constraints on demand
    if ( !fBmc && p->pPars->fDynamic )
    {
clk = Abc_Clock();
        Ssw_ManLoadSolver( p, pObjRepr, pObj );
        p->nRecycleCalls++;
p->timeMarkCones += Abc_Clock() - clk;
    }
    // call equivalence checking
    if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
    else
        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
    if ( RetValue == 1 )  // proved equivalent
    {
        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
        Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
        if ( p->pPars->fEquivDump2 && vPairs )
        {
            Vec_IntPush( vPairs, pObjRepr->Id );
            Vec_IntPush( vPairs, pObj->Id );
        }
        return 0;
    }
    if ( p->pPars->fEquivDump && vPairs )
    {
        Vec_IntPush( vPairs, pObjRepr->Id );
        Vec_IntPush( vPairs, pObj->Id );
    }
    if ( RetValue == -1 ) // timed out
    {
        Ssw_ClassesRemoveNode( p->ppClasses, pObj );
        return 1;
    }
    // disproved the equivalence
    if ( !fBmc && p->pPars->fDynamic )
    {
        Ssw_SmlAddPatternDyn( p );
        p->nPatterns++;
        return 1;
    }
    else
        Ssw_SmlSavePatternAig( p, f );
    if ( !p->pPars->fConstrs )
        Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
    else
        Ssw_ManResimulateBit( p, pObj, pObjRepr );
    assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
    if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
    {
        Abc_Print( 1, "Ssw_ManSweepNode(): Failed to refine representative.\n" );
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_ManUniqueAddConstraint()

int Ssw_ManUniqueAddConstraint ( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 )

extern

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

Synopsis [Returns the output of the uniqueness constraint.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file sswUnique.c.

{
    Aig_Obj_t * pObj, * pObj1New, * pObj2New, * pMiter, * pTotal;
    int i, pLits[2];
//    int RetValue;
    assert( Vec_PtrSize(vCommon) > 0 );
    // generate the constraint
    pTotal = Aig_ManConst0(p->pFrames);
    Vec_PtrForEachEntry( Aig_Obj_t *, vCommon, pObj, i )
    {
        assert( Saig_ObjIsLo(p->pAig, pObj) );
        pObj1New = Ssw_ObjFrame( p, pObj, f1 );
        pObj2New = Ssw_ObjFrame( p, pObj, f2 );
        pMiter = Aig_Exor( p->pFrames, pObj1New, pObj2New );
        pTotal = Aig_Or( p->pFrames, pTotal, pMiter );
    }
    if ( Aig_ObjIsConst1(Aig_Regular(pTotal)) )
    {
//        Abc_Print( 1, "Skipped\n" );
        return 0;
    }
    // create CNF
    Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pTotal) );
    // add output constraint
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_Regular(pTotal)), Aig_IsComplement(pTotal) );
/*
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    assert( RetValue );
    // simplify the solver
    if ( p->pSat->qtail != p->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pSat);
        assert( RetValue != 0 );
    }
*/
    assert( p->iOutputLit == -1 );
    p->iOutputLit = pLits[0];
    return 1;
}

Here is the call graph for this function:

Ssw_ManUniqueOne()

int Ssw_ManUniqueOne ( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose )

extern

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

Synopsis [Returns 1 if uniqueness constraints can be added.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file sswUnique.c.

{
    Aig_Obj_t * ppObjs[2], * pTemp;
    int i, k, Value0, Value1, RetValue, fFeasible;
 
    assert( p->pPars->nFramesK > 1 );
    assert( p->vDiffPairs && Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
 
    // compute the first support in terms of LOs
    ppObjs[0] = pRepr;
    ppObjs[1] = pObj;
    Aig_SupportNodes( p->pAig, ppObjs, 2, p->vCommon );
    // keep only LOs
    RetValue = Vec_PtrSize( p->vCommon );
    fFeasible = 0;
    k = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i )
    {
        assert( Aig_ObjIsCi(pTemp) );
        if ( !Saig_ObjIsLo(p->pAig, pTemp) )
            continue;
        assert( Aig_ObjCioId(pTemp) > 0 );
        Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
        if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjCioId(pTemp) - Saig_ManPiNum(p->pAig)) )
            fFeasible = 1;
    }
    Vec_PtrShrink( p->vCommon, k );
 
    if ( fVerbose )
        Abc_Print( 1, "Node = %5d : Supp = %3d. Regs = %3d. Feasible = %s. ",
            Aig_ObjId(pObj), RetValue, Vec_PtrSize(p->vCommon),
            fFeasible? "yes": "no " );
 
    // check the current values
    RetValue = 1;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i )
    {
        Value0 = Ssw_ManGetSatVarValue( p, pTemp, 0 );
        Value1 = Ssw_ManGetSatVarValue( p, pTemp, 1 );
        if ( Value0 != Value1 )
            RetValue = 0;
        if ( fVerbose )
            Abc_Print( 1, "%d", Value0 ^ Value1 );
    }
    if ( fVerbose )
        Abc_Print( 1, "\n" );
 
    return RetValue && fFeasible;
}

Here is the call graph for this function:

Ssw_NodeIsConstrained()

int Ssw_NodeIsConstrained ( Ssw_Man_t * p, Aig_Obj_t * pPoObj )

extern

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

Synopsis [Constrains one node in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 286 of file sswSat.c.

{
    int RetValue, Lit;
    Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pPoObj) );
    // add constraint A = 1  ---->  A
    Lit = toLitCond( Ssw_ObjSatNum(p->pMSat,Aig_ObjFanin0(pPoObj)), !Aig_ObjFaninC0(pPoObj) );
    if ( p->pPars->fPolarFlip )
    {
        if ( Aig_ObjFanin0(pPoObj)->fPhase )  Lit = lit_neg( Lit );
    }
    RetValue = sat_solver_addclause( p->pMSat->pSat, &Lit, &Lit + 1 );
    assert( RetValue );
    return 1;
}

Here is the call graph for this function:

Ssw_NodesAreConstrained()

int Ssw_NodesAreConstrained ( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )

extern

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

Synopsis [Constrains two nodes to be equivalent in the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file sswSat.c.

{
    int pLits[2], RetValue, fComplNew;
    Aig_Obj_t * pTemp;
 
    // sanity checks
    assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
    assert( p->pPars->fConstrs || Aig_ObjPhaseReal(pOld) == Aig_ObjPhaseReal(pNew) );
 
    // move constant to the old node
    if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
    {
        assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) );
        pTemp = pOld;
        pOld  = pNew;
        pNew  = pTemp;
    }
 
    // move complement to the new node
    if ( Aig_IsComplement(pOld) )
    {
        pOld = Aig_Regular(pOld);
        pNew = Aig_Not(pNew);
    }
    assert( p->pMSat != NULL );
 
    // if the nodes do not have SAT variables, allocate them
    Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
    Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pNew) );
 
    // transform the new node
    fComplNew = Aig_IsComplement( pNew );
    pNew = Aig_Regular( pNew );
 
    // consider the constant 1 case
    if ( pOld == Aig_ManConst1(p->pFrames) )
    {
        // add constraint A = 1  ---->  A
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew );
        if ( p->pPars->fPolarFlip )
        {
            if ( pNew->fPhase )  pLits[0] = lit_neg( pLits[0] );
        }
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 1 );
        assert( RetValue );
    }
    else
    {
        // add constraint A = B  ---->  (A v !B)(!A v B)
 
        // (A v !B)
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
        pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), !fComplNew );
        if ( p->pPars->fPolarFlip )
        {
            if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
            if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
        }
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
        assert( RetValue );
 
        // (!A v B)
        pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
        pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew);
        if ( p->pPars->fPolarFlip )
        {
            if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
            if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
        }
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
        assert( RetValue );
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_NodesAreEquiv()

int Ssw_NodesAreEquiv ( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )

extern

DECLARATIONS ///.

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

FileName [sswSat.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

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

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

Synopsis [Runs equivalence test for the two nodes.]

Description [Both nodes should be regular and different from each other.]

SideEffects []

SeeAlso []

Definition at line 45 of file sswSat.c.

{
    int nBTLimit = p->pPars->nBTLimit;
    int pLits[3], nLits, RetValue, RetValue1;
    abctime clk;//, status;
    p->nSatCalls++;
    p->pMSat->nSolverCalls++;
 
    // sanity checks
    assert( !Aig_IsComplement(pOld) );
    assert( !Aig_IsComplement(pNew) );
    assert( pOld != pNew );
    assert( p->pMSat != NULL );
 
    // if the nodes do not have SAT variables, allocate them
    Ssw_CnfNodeAddToSolver( p->pMSat, pOld );
    Ssw_CnfNodeAddToSolver( p->pMSat, pNew );
 
    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
    nLits = 2;
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
    pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase == pNew->fPhase );
    if ( p->iOutputLit > -1 )
        pLits[nLits++] = p->iOutputLit;
    if ( p->pPars->fPolarFlip )
    {
        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
    }
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
 
    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pMSat->pSat);
        //assert( RetValue != 0 );
    }
 
clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        if ( nLits == 2 )
        {
            pLits[0] = lit_neg( pLits[0] );
            pLits[1] = lit_neg( pLits[1] );
            RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
            assert( RetValue );
/*
            if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
            {
                RetValue = sat_solver_simplify(p->pMSat->pSat);
                assert( RetValue != 0 );
            }
*/
        }
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatFailsReal++;
        return -1;
    }
 
    // if the old node was constant 0, we already know the answer
    if ( pOld == Aig_ManConst1(p->pFrames) )
    {
        p->nSatProof++;
        return 1;
    }
 
    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
    nLits = 2;
    pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 1 );
    pLits[1] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), pOld->fPhase ^ pNew->fPhase );
    if ( p->iOutputLit > -1 )
        pLits[nLits++] = p->iOutputLit;
    if ( p->pPars->fPolarFlip )
    {
        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
    }
 
    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pMSat->pSat);
        //assert( RetValue != 0 );
    }
 
clk = Abc_Clock();
    RetValue1 = sat_solver_solve( p->pMSat->pSat, pLits, pLits + nLits, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        if ( nLits == 2 )
        {
            pLits[0] = lit_neg( pLits[0] );
            pLits[1] = lit_neg( pLits[1] );
            RetValue = sat_solver_addclause( p->pMSat->pSat, pLits, pLits + 2 );
            assert( RetValue );
/*
            if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
            {
                RetValue = sat_solver_simplify(p->pMSat->pSat);
                assert( RetValue != 0 );
            }
*/
        }
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatUndec += Abc_Clock() - clk;
        p->nSatFailsReal++;
        return -1;
    }
    // return SAT proof
    p->nSatProof++;
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SatStart()

Ssw_Sat_t * Ssw_SatStart ( int fPolarFlip )

extern

DECLARATIONS ///.

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

FileName [sswCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Computation of CNF.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Starts the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswCnf.c.

{
    Ssw_Sat_t * p;
    int Lit;
    p = ABC_ALLOC( Ssw_Sat_t, 1 );
    memset( p, 0, sizeof(Ssw_Sat_t) );
    p->pAig          = NULL;
    p->fPolarFlip    = fPolarFlip;
    p->vSatVars      = Vec_IntStart( 10000 );
    p->vFanins       = Vec_PtrAlloc( 100 );
    p->vUsedPis      = Vec_PtrAlloc( 100 );
    p->pSat          = sat_solver_new();
    sat_solver_setnvars( p->pSat, 1000 );
    // var 0 is not used
    // var 1 is reserved for const1 node - add the clause
    p->nSatVars = 1;
    Lit = toLit( p->nSatVars );
    if ( fPolarFlip )
        Lit = lit_neg( Lit );
    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
//    Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
    Vec_IntWriteEntry( p->vSatVars, 0, p->nSatVars++ );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SatStop()

void Ssw_SatStop ( Ssw_Sat_t * p )

extern

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

Synopsis [Stop the SAT manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 81 of file sswCnf.c.

{
//    Abc_Print( 1, "Recycling SAT solver with %d vars and %d restarts.\n", 
//        p->pSat->size, p->pSat->stats.starts );
    if ( p->pSat )
        sat_solver_delete( p->pSat );
    Vec_IntFree( p->vSatVars );
    Vec_PtrFree( p->vFanins );
    Vec_PtrFree( p->vUsedPis );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SignalCorrespondenceRefine()

Aig_Man_t * Ssw_SignalCorrespondenceRefine ( Ssw_Man_t * p )

extern

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

Synopsis [Performs computation of signal correspondence with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file sswCore.c.

{
    int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
    Aig_Man_t * pAigNew;
    int RetValue, nIter = -1, nPrev[4] = {0};
    abctime clk, clkTotal = Abc_Clock();
    // get the starting stats
    p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
    p->nRegsBeg  = Aig_ManRegNum(p->pAig);
    // refine classes using BMC
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Before BMC: " );
        Ssw_ClassesPrint( p->ppClasses, 0 );
    }
    if ( !p->pPars->fLatchCorr || p->pPars->nFramesK > 1 )
    {
        p->pMSat = Ssw_SatStart( 0 );
        if ( p->pPars->fConstrs )
            Ssw_ManSweepBmcConstr( p );
        else
            Ssw_ManSweepBmc( p );
        Ssw_SatStop( p->pMSat );
        p->pMSat = NULL;
        Ssw_ManCleanup( p );
    }
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "After  BMC: " );
        Ssw_ClassesPrint( p->ppClasses, 0 );
    }
    // apply semi-formal filtering
/*
    if ( p->pPars->fSemiFormal )
    {
        Aig_Man_t * pSRed;
        Ssw_FilterUsingSemi( p, 0, 2000, p->pPars->fVerbose );
//        Ssw_FilterUsingSemi( p, 1, 100000, p->pPars->fVerbose );
        pSRed = Ssw_SpeculativeReduction( p );
        Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
        Aig_ManStop( pSRed );
    }
*/
    if ( p->pPars->pFunc )
    {
        ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
        ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
    }
    if ( p->pPars->nStepsMax == 0 )
    {
        Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
        goto finalize;
    }
    // refine classes using induction
    nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
    for ( nIter = 0; ; nIter++ )
    {
        if ( p->pPars->nStepsMax == nIter )
        {
            Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter );
            goto finalize;
        }
        if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
        {
            Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
            Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
            Aig_ManStop( pSRed );
            Abc_Print( 1, "Iterative refinement is stopped before iteration %d.\n", nIter );
            Abc_Print( 1, "The network is reduced using candidate equivalences.\n" );
            Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
            Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" );
            break;
        }
 
clk = Abc_Clock();
        p->pMSat = Ssw_SatStart( 0 );
        if ( p->pPars->fLatchCorrOpt )
        {
            RetValue = Ssw_ManSweepLatch( p );
            if ( p->pPars->fVerbose )
            {
                Abc_Print( 1, "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. R =%4d. F =%4d. ",
                    nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
                    p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
                    p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
                ABC_PRT( "T", Abc_Clock() - clk );
            }
        }
        else
        {
            if ( p->pPars->fConstrs )
                RetValue = Ssw_ManSweepConstr( p );
            else if ( p->pPars->fDynamic )
                RetValue = Ssw_ManSweepDyn( p );
            else
                RetValue = Ssw_ManSweep( p );
 
            p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
            if ( p->pPars->fVerbose )
            {
                Abc_Print( 1, "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ",
                    nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
                    p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
                if ( p->pPars->fDynamic )
                {
                    Abc_Print( 1, "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
                    Abc_Print( 1, "R =%4d. ",   p->nRecycles-nRecycles );
                }
                Abc_Print( 1, "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal,
                    (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
                ABC_PRT( "T", Abc_Clock() - clk );
            }
//            if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
//                p->pPars->nBTLimit = 10000;
 
            if ( p->pPars->fStopWhenGone && Saig_ManPoNum(p->pAig) == 1 && !Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))) )
            {
                printf( "Iterative refinement is stopped after iteration %d\n", nIter );
                printf( "because the property output is no longer a candidate constant.\n" );
                // prepare to quit
                p->nLitsEnd  = p->nLitsBeg;
                p->nNodesEnd = p->nNodesBeg;
                p->nRegsEnd  = p->nRegsBeg;
                // cleanup
                Ssw_SatStop( p->pMSat );
                p->pMSat = NULL;
                Ssw_ManCleanup( p );
                // cleanup
                Aig_ManSetPhase( p->pAig );
                Aig_ManCleanMarkB( p->pAig );
                return Aig_ManDupSimple( p->pAig );
            }
        }
        nSatProof     = p->nSatProof;
        nSatCallsSat  = p->nSatCallsSat;
        nRecycles     = p->nRecycles;
        nSatFailsReal = p->nSatFailsReal;
        nUniques      = p->nUniques;
 
        p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
        p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
        Ssw_SatStop( p->pMSat );
        p->pMSat = NULL;
        Ssw_ManCleanup( p );
        if ( !RetValue )
            break;
        if ( p->pPars->pFunc )
            ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
        if ( p->pPars->nLimitMax )
        {
            int nCur = Ssw_ClassesCand1Num(p->ppClasses);
            if ( nIter > 4 && nPrev[0] - nCur <= 4*p->pPars->nLimitMax )
            {
                printf( "Iterative refinement is stopped after iteration %d\n", nIter );
                printf( "because the refinment is very slow.\n" );
                // prepare to quit
                p->nLitsEnd  = p->nLitsBeg;
                p->nNodesEnd = p->nNodesBeg;
                p->nRegsEnd  = p->nRegsBeg;
                // cleanup
                Aig_ManSetPhase( p->pAig );
                Aig_ManCleanMarkB( p->pAig );
                return Aig_ManDupSimple( p->pAig );
            }
            nPrev[0] = nPrev[1];
            nPrev[1] = nPrev[2];
            nPrev[2] = nPrev[3];
            nPrev[3] = nCur;
        }
    }
 
finalize:
    p->pPars->nIters = nIter + 1;
p->timeTotal = Abc_Clock() - clkTotal;
 
    Ssw_ManUpdateEquivs( p, p->pAig, p->pPars->fVerbose );
    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
    Aig_ManSeqCleanup( pAigNew );
//Ssw_ClassesPrint( p->ppClasses, 1 );
    // get the final stats
    p->nLitsEnd  = Ssw_ClassesLitNum( p->ppClasses );
    p->nNodesEnd = Aig_ManNodeNum(pAigNew);
    p->nRegsEnd  = Aig_ManRegNum(pAigNew);
    // cleanup
    Aig_ManSetPhase( p->pAig );
    Aig_ManCleanMarkB( p->pAig );
    return pAigNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SmlAssignDist1Plus()

void Ssw_SmlAssignDist1Plus ( Ssw_Sml_t * p, unsigned * pPat )

extern

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

Synopsis [Assings distance-1 simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 674 of file sswSim.c.

{
    Aig_Obj_t * pObj;
    int f, i, Limit;
    assert( p->nFrames > 0 );
 
    // copy the pattern into the primary inputs
    Aig_ManForEachCi( p->pAig, pObj, i )
        Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
 
    // set distance one PIs for the first frame
    Limit = Abc_MinInt( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
    for ( i = 0; i < Limit; i++ )
        Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ), i+1 );
 
    // create random info for the remaining timeframes
    for ( f = 1; f < p->nFrames; f++ )
        Saig_ManForEachPi( p->pAig, pObj, i )
            Ssw_SmlAssignRandomFrame( p, pObj, f );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SmlAssignRandomFrame()

void Ssw_SmlAssignRandomFrame ( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )

extern

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

Synopsis [Assigns random patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 538 of file sswSim.c.

{
    unsigned * pSims;
    int i;
    assert( iFrame < p->nFrames );
    assert( Aig_ObjIsCi(pObj) );
    pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
    for ( i = 0; i < p->nWordsFrame; i++ )
        pSims[i] = Ssw_ObjRandomSim();
}

Here is the caller graph for this function:

Ssw_SmlClean()

void Ssw_SmlClean ( Ssw_Sml_t * p )

extern

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1173 of file sswSim.c.

{
    memset( p->pData, 0, sizeof(unsigned) * Aig_ManObjNumMax(p->pAig) * p->nWordsTotal );
}

Here is the call graph for this function:

Ssw_SmlObjAssignConst()

void Ssw_SmlObjAssignConst ( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )

extern

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file sswSim.c.

{
    unsigned * pSims;
    int i;
    assert( iFrame < p->nFrames );
    assert( Aig_ObjIsCi(pObj) );
    pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
    for ( i = 0; i < p->nWordsFrame; i++ )
        pSims[i] = fConst1? ~(unsigned)0 : 0;
}

Here is the caller graph for this function:

Ssw_SmlObjHashWord()

unsigned Ssw_SmlObjHashWord ( Ssw_Sml_t * p, Aig_Obj_t * pObj )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes hash value of the node using its simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file sswSim.c.

{
    static int s_SPrimes[128] = {
        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
    };
    unsigned * pSims;
    unsigned uHash;
    int i;
//    assert( p->nWordsTotal <= 128 );
    uHash = 0;
    pSims = Ssw_ObjSim(p, pObj->Id);
    for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
        uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
    return uHash;
}

Here is the caller graph for this function:

Ssw_SmlObjIsConstBit()

int Ssw_SmlObjIsConstBit ( void * p, Aig_Obj_t * pObj )

extern

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

Synopsis [Returns 1 if the node appears to be constant 1 candidate.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file sswSim.c.

{
    return pObj->fPhase == pObj->fMarkB;
}

Here is the caller graph for this function:

Ssw_SmlObjIsConstWord()

int Ssw_SmlObjIsConstWord ( Ssw_Sml_t * p, Aig_Obj_t * pObj )

extern

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file sswSim.c.

{
    unsigned * pSims;
    int i;
    pSims = Ssw_ObjSim(p, pObj->Id);
    for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
        if ( pSims[i] )
            return 0;
    return 1;
}

Here is the caller graph for this function:

Ssw_SmlObjsAreEqualBit()

int Ssw_SmlObjsAreEqualBit ( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )

extern

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

Synopsis [Returns 1 if the nodes appear equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file sswSim.c.

{
    return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
}

Here is the caller graph for this function:

Ssw_SmlObjsAreEqualWord()

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

extern

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

Ssw_SmlObjSetWord()

void Ssw_SmlObjSetWord ( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame )

extern

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 603 of file sswSim.c.

{
    unsigned * pSims;
    assert( iFrame < p->nFrames );
    assert( Aig_ObjIsCi(pObj) );
    pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
    pSims[iWord] = Word;
}

Here is the caller graph for this function:

Ssw_SmlResimulateSeq()

void Ssw_SmlResimulateSeq ( Ssw_Sml_t * p )

extern

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

Synopsis [Performs next round of sequential simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1269 of file sswSim.c.

{
    Ssw_SmlReinitialize( p );
    Ssw_SmlSimulateOne( p );
    p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SmlSavePatternAig()

void Ssw_SmlSavePatternAig ( Ssw_Man_t * p, int f )

extern

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file sswSweep.c.

{
    Aig_Obj_t * pObj;
    int i;
    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
    Aig_ManForEachCi( p->pAig, pObj, i )
        if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
            Abc_InfoSetBit( p->pPatWords, i );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SmlSimulateOne()

void Ssw_SmlSimulateOne ( Ssw_Sml_t * p )

extern

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1005 of file sswSim.c.

{
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int f, i;
    abctime clk;
clk = Abc_Clock();
    for ( f = 0; f < p->nFrames; f++ )
    {
        // simulate the nodes
        Aig_ManForEachNode( p->pAig, pObj, i )
            Ssw_SmlNodeSimulate( p, pObj, f );
        // copy simulation info into outputs
        Saig_ManForEachPo( p->pAig, pObj, i )
            Ssw_SmlNodeCopyFanin( p, pObj, f );
        // copy simulation info into outputs
        Saig_ManForEachLi( p->pAig, pObj, i )
            Ssw_SmlNodeCopyFanin( p, pObj, f );
        // quit if this is the last timeframe
        if ( f == p->nFrames - 1 )
            break;
        // copy simulation info into the inputs
        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
            Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
    }
p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SmlSimulateOneDyn_rec()

void Ssw_SmlSimulateOneDyn_rec ( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pVisited, int nVisCounter )

extern

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1076 of file sswSim.c.

{
//    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
//        return;
//    Aig_ObjSetTravIdCurrent(p->pAig, pObj);
    if ( pVisited[p->nFrames*pObj->Id+f] == nVisCounter )
        return;
    pVisited[p->nFrames*pObj->Id+f] = nVisCounter;
    if ( Saig_ObjIsPi( p->pAig, pObj ) || Aig_ObjIsConst1(pObj) )
        return;
    if ( Saig_ObjIsLo( p->pAig, pObj ) )
    {
        if ( f == 0 )
            return;
        Ssw_SmlSimulateOneDyn_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1, pVisited, nVisCounter );
        Ssw_SmlNodeTransferNext( p, Saig_ObjLoToLi(p->pAig, pObj), pObj, f-1 );
        return;
    }
    if ( Saig_ObjIsLi( p->pAig, pObj ) )
    {
        Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
        Ssw_SmlNodeCopyFanin( p, pObj, f );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
    Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin1(pObj), f, pVisited, nVisCounter );
    Ssw_SmlNodeSimulate( p, pObj, f );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SmlSimulateOneFrame()

void Ssw_SmlSimulateOneFrame ( Ssw_Sml_t * p )

extern

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1117 of file sswSim.c.

{
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i;
    abctime clk;
clk = Abc_Clock();
    // simulate the nodes
    Aig_ManForEachNode( p->pAig, pObj, i )
        Ssw_SmlNodeSimulate( p, pObj, 0 );
    // copy simulation info into outputs
    Saig_ManForEachLi( p->pAig, pObj, i )
        Ssw_SmlNodeCopyFanin( p, pObj, 0 );
    // copy simulation info into the inputs
    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
        Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 );
p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SmlStart()

Ssw_Sml_t * Ssw_SmlStart ( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )

extern

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1148 of file sswSim.c.

{
    Ssw_Sml_t * p;
    p = (Ssw_Sml_t *)ABC_ALLOC( char, sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
    memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
    p->pAig        = pAig;
    p->nPref       = nPref;
    p->nFrames     = nPref + nFrames;
    p->nWordsFrame = nWordsFrame;
    p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
    p->nWordsPref  = nPref * nWordsFrame;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_SmlStop()

void Ssw_SmlStop ( Ssw_Sml_t * p )

extern

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

Synopsis [Deallocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1211 of file sswSim.c.

{
    ABC_FREE( p );
}

Ssw_SpeculativeReduction()

Aig_Man_t * Ssw_SpeculativeReduction ( Ssw_Man_t * p )

extern

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

Synopsis [Prepares the inductive case with speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 272 of file sswAig.c.

{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjNew;
    int i;
    assert( p->pFrames == NULL );
    assert( Aig_ManRegNum(p->pAig) > 0 );
    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
    p->nConstrTotal = p->nConstrReduced = 0;
 
    // start the fraig package
    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
    pFrames->pName = Abc_UtilStrsav( p->pAig->pName );
    // map constants and PIs
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // create latches for the first frame
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
    // set the constraints on the latch outputs
    Saig_ManForEachLo( p->pAig, pObj, i )
        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
    // add internal nodes of this frame
    Aig_ManForEachNode( p->pAig, pObj, i )
    {
        pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
        Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
    }
    // add the POs for the latch outputs of the last frame
    Saig_ManForEachLi( p->pAig, pObj, i )
        Aig_ObjCreateCo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
    // remove dangling nodes
    Aig_ManCleanup( pFrames );
    Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
//    Abc_Print( 1, "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", 
//        p->nConstrTotal, p->nConstrReduced );
    return pFrames;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ssw_UniqueRegisterPairInfo()

void Ssw_UniqueRegisterPairInfo ( Ssw_Man_t * p )

extern

DECLARATIONS ///.

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

FileName [sswSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [On-demand uniqueness constraints.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Performs computation of signal correspondence with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswUnique.c.

{
    Aig_Obj_t * pObjLo, * pObj0, * pObj1;
    int i, RetValue, Counter;
    if ( p->vDiffPairs == NULL )
        p->vDiffPairs = Vec_IntAlloc( Saig_ManRegNum(p->pAig) );
    Vec_IntClear( p->vDiffPairs );
    Saig_ManForEachLo( p->pAig, pObjLo, i )
    {
        pObj0 = Ssw_ObjFrame( p, pObjLo, 0 );
        pObj1 = Ssw_ObjFrame( p, pObjLo, 1 );
        if ( pObj0 == pObj1 )
            Vec_IntPush( p->vDiffPairs, 0 );
        else if ( pObj0 == Aig_Not(pObj1) )
            Vec_IntPush( p->vDiffPairs, 1 );
//        else
//            Vec_IntPush( p->vDiffPairs, 1 );
        else if ( Aig_ObjPhaseReal(pObj0) != Aig_ObjPhaseReal(pObj1) )
            Vec_IntPush( p->vDiffPairs, 1 );
        else
        {
            RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObj0), Aig_Regular(pObj1) );
            Vec_IntPush( p->vDiffPairs, RetValue!=1 );
        }
    }
    assert( Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
    // count the number of ones
    Counter = 0;
    Vec_IntForEachEntry( p->vDiffPairs, RetValue, i )
        Counter += RetValue;
//    Abc_Print( 1, "The number of different register pairs = %d.\n", Counter );
}

Here is the call graph for this function: