sim.h File Reference

Go to the source code of this file.

Data Structures
struct	Sym_Man_t_
struct	Sim_Man_t_
struct	Sim_Pat_t_

Macros
#define	SIM_NUM_WORDS(n)   (((n)>>5) + (((n)&31) > 0))
	MACRO DEFINITIONS ///. More...
#define	SIM_LAST_BITS(n)   ((((n)&31) > 0)? (n)&31 : 32)
#define	SIM_MASK_FULL   (0xFFFFFFFF)
#define	SIM_MASK_BEG(n)   (SIM_MASK_FULL >> (32-n))
#define	SIM_MASK_END(n)   (SIM_MASK_FULL << (n))
#define	SIM_SET_0_FROM(m, n)   ((m) & ~SIM_MASK_BEG(n))
#define	SIM_SET_1_FROM(m, n)   ((m) | SIM_MASK_END(n))
#define	SIM_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
#define	Sim_SetBit(p, i)   ((p)[(i)>>5] |= (1<<((i) & 31)))
#define	Sim_XorBit(p, i)   ((p)[(i)>>5] ^= (1<<((i) & 31)))
#define	Sim_HasBit(p, i)   (((p)[(i)>>5] & (1<<((i) & 31))) > 0)
#define	Sim_SuppStrSetVar(vSupps, pNode, v)   Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define	Sim_SuppStrHasVar(vSupps, pNode, v)   Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define	Sim_SuppFunSetVar(vSupps, Output, v)   Sim_SetBit((unsigned*)(vSupps)->pArray[Output],(v))
#define	Sim_SuppFunHasVar(vSupps, Output, v)   Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v))
#define	Sim_SimInfoSetVar(vSupps, pNode, v)   Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define	Sim_SimInfoHasVar(vSupps, pNode, v)   Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
#define	Sim_SimInfoGet(vInfo, pNode)   ((unsigned *)((vInfo)->pArray[(pNode)->Id]))

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Sym_Man_t_	Sym_Man_t
	INCLUDES ///. More...
typedef struct Sim_Man_t_	Sim_Man_t
typedef struct Sim_Pat_t_	Sim_Pat_t

Functions
Sym_Man_t *	Sym_ManStart (Abc_Ntk_t *pNtk, int fVerbose)
	FUNCTION DECLARATIONS ///. More...
void	Sym_ManStop (Sym_Man_t *p)
void	Sym_ManPrintStats (Sym_Man_t *p)
Sim_Man_t *	Sim_ManStart (Abc_Ntk_t *pNtk, int fLightweight)
void	Sim_ManStop (Sim_Man_t *p)
void	Sim_ManPrintStats (Sim_Man_t *p)
Sim_Pat_t *	Sim_ManPatAlloc (Sim_Man_t *p)
void	Sim_ManPatFree (Sim_Man_t *p, Sim_Pat_t *pPat)
Vec_Ptr_t *	Sim_SimulateSeqRandom (Abc_Ntk_t *pNtk, int nFrames, int nWords)
	FUNCTION DEFINITIONS ///. More...
Vec_Ptr_t *	Sim_SimulateSeqModel (Abc_Ntk_t *pNtk, int nFrames, int *pModel)
Vec_Ptr_t *	Sim_ComputeStrSupp (Abc_Ntk_t *pNtk)
	FUNCTION DEFINITIONS ///. More...
Vec_Ptr_t *	Sim_ComputeFunSupp (Abc_Ntk_t *pNtk, int fVerbose)
int	Sim_ComputeTwoVarSymms (Abc_Ntk_t *pNtk, int fVerbose)
	DECLARATIONS ///. More...
int	Sim_SymmsGetPatternUsingSat (Sym_Man_t *p, unsigned *pPattern)
	FUNCTION DEFINITIONS ///. More...
void	Sim_SymmsStructCompute (Abc_Ntk_t *pNtk, Vec_Ptr_t *vMatrs, Vec_Ptr_t *vSuppFun)
	FUNCTION DEFINITIONS ///. More...
void	Sim_SymmsSimulate (Sym_Man_t *p, unsigned *pPatRand, Vec_Ptr_t *vMatrsNonSym)
	FUNCTION DEFINITIONS ///. More...
Vec_Ptr_t *	Sim_UtilInfoAlloc (int nSize, int nWords, int fClean)
	FUNCTION DEFINITIONS ///. More...
void	Sim_UtilInfoFree (Vec_Ptr_t *p)
void	Sim_UtilInfoAdd (unsigned *pInfo1, unsigned *pInfo2, int nWords)
void	Sim_UtilInfoDetectDiffs (unsigned *pInfo1, unsigned *pInfo2, int nWords, Vec_Int_t *vDiffs)
void	Sim_UtilInfoDetectNews (unsigned *pInfo1, unsigned *pInfo2, int nWords, Vec_Int_t *vDiffs)
void	Sim_UtilInfoFlip (Sim_Man_t *p, Abc_Obj_t *pNode)
int	Sim_UtilInfoCompare (Sim_Man_t *p, Abc_Obj_t *pNode)
void	Sim_UtilSimulate (Sim_Man_t *p, int fFirst)
void	Sim_UtilSimulateNode (Sim_Man_t *p, Abc_Obj_t *pNode, int fType, int fType1, int fType2)
void	Sim_UtilSimulateNodeOne (Abc_Obj_t *pNode, Vec_Ptr_t *vSimInfo, int nSimWords, int nOffset)
void	Sim_UtilTransferNodeOne (Abc_Obj_t *pNode, Vec_Ptr_t *vSimInfo, int nSimWords, int nOffset, int fShift)
int	Sim_UtilCountSuppSizes (Sim_Man_t *p, int fStruct)
int	Sim_UtilCountOnes (unsigned *pSimInfo, int nSimWords)
Vec_Int_t *	Sim_UtilCountOnesArray (Vec_Ptr_t *vInfo, int nSimWords)
void	Sim_UtilSetRandom (unsigned *pPatRand, int nSimWords)
void	Sim_UtilSetCompl (unsigned *pPatRand, int nSimWords)
void	Sim_UtilSetConst (unsigned *pPatRand, int nSimWords, int fConst1)
int	Sim_UtilInfoIsEqual (unsigned *pPats1, unsigned *pPats2, int nSimWords)
int	Sim_UtilInfoIsImp (unsigned *pPats1, unsigned *pPats2, int nSimWords)
int	Sim_UtilInfoIsClause (unsigned *pPats1, unsigned *pPats2, int nSimWords)
int	Sim_UtilCountAllPairs (Vec_Ptr_t *vSuppFun, int nSimWords, Vec_Int_t *vCounters)
void	Sim_UtilCountPairsAll (Sym_Man_t *p)
int	Sim_UtilMatrsAreDisjoint (Sym_Man_t *p)

Macro Definition Documentation

#define Sim_HasBit	(		p,
			i
	)		(((p)[(i)>>5] & (1<<((i) & 31))) > 0)

Definition at line 163 of file sim.h.

#define SIM_LAST_BITS

(

n

)

((((n)&31) > 0)? (n)&31 : 32)

Definition at line 149 of file sim.h.

#define SIM_MASK_BEG

(

n

)

(SIM_MASK_FULL >> (32-n))

Definition at line 152 of file sim.h.

#define SIM_MASK_END

(

n

)

(SIM_MASK_FULL << (n))

Definition at line 153 of file sim.h.

#define SIM_MASK_FULL   (0xFFFFFFFF)

Definition at line 151 of file sim.h.

#define SIM_NUM_WORDS

(

n

)

(((n)>>5) + (((n)&31) > 0))

MACRO DEFINITIONS ///.

Definition at line 148 of file sim.h.

#define SIM_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))

Definition at line 158 of file sim.h.

#define SIM_SET_0_FROM	(		m,
			n
	)		((m) & ~SIM_MASK_BEG(n))

Definition at line 154 of file sim.h.

#define SIM_SET_1_FROM	(		m,
			n
	)		((m) | SIM_MASK_END(n))

Definition at line 155 of file sim.h.

#define Sim_SetBit	(		p,
			i
	)		((p)[(i)>>5] |= (1<<((i) & 31)))

Definition at line 161 of file sim.h.

#define Sim_SimInfoGet	(		vInfo,
			pNode
	)		((unsigned *)((vInfo)->pArray[(pNode)->Id]))

Definition at line 172 of file sim.h.

#define Sim_SimInfoHasVar	(		vSupps,
			pNode,
			v
	)		Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))

Definition at line 171 of file sim.h.

#define Sim_SimInfoSetVar	(		vSupps,
			pNode,
			v
	)		Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))

Definition at line 170 of file sim.h.

#define Sim_SuppFunHasVar	(		vSupps,
			Output,
			v
	)		Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v))

Definition at line 169 of file sim.h.

#define Sim_SuppFunSetVar	(		vSupps,
			Output,
			v
	)		Sim_SetBit((unsigned*)(vSupps)->pArray[Output],(v))

Definition at line 168 of file sim.h.

#define Sim_SuppStrHasVar	(		vSupps,
			pNode,
			v
	)		Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))

Definition at line 167 of file sim.h.

#define Sim_SuppStrSetVar	(		vSupps,
			pNode,
			v
	)		Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))

Definition at line 166 of file sim.h.

#define Sim_XorBit	(		p,
			i
	)		((p)[(i)>>5] ^= (1<<((i) & 31)))

Definition at line 162 of file sim.h.

Typedef Documentation

typedef struct Sim_Man_t_ Sim_Man_t

Definition at line 100 of file sim.h.

typedef struct Sim_Pat_t_ Sim_Pat_t

Definition at line 136 of file sim.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Sym_Man_t_ Sym_Man_t

INCLUDES ///.

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

FileName [sim.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Simulation package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]PARAMETERS ///BASIC TYPES ///

Definition at line 48 of file sim.h.

Function Documentation

Vec_Ptr_t* Sim_ComputeFunSupp	(	Abc_Ntk_t *	pNtk,
		int	fVerbose
	)

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

Synopsis [Compute functional supports.]

Description [Supports are returned as an array of bit strings, one for each CO.]

SideEffects []

SeeAlso []

Definition at line 103 of file simSupp.c.

{
    Sim_Man_t * p;
    Vec_Ptr_t * vResult;
    int nSolved, i;
    abctime clk = Abc_Clock();

    srand( 0xABC );

    // start the simulation manager
    p = Sim_ManStart( pNtk, 0 );

    // compute functional support using one round of random simulation
    Sim_UtilAssignRandom( p );
    Sim_ComputeSuppRound( p, 0 );

    // set the support targets 
    Sim_ComputeSuppSetTargets( p );
if ( fVerbose )
    printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
        goto exit;

    for ( i = 0; i < 1; i++ )
    {
        // compute patterns using one round of random simulation
        Sim_UtilAssignRandom( p );
        nSolved = Sim_ComputeSuppRound( p, 1 );
        if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
            goto exit;

if ( fVerbose )
    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", 
       Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
    }

    // try to solve the support targets
    while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
    {
        // solve targets until the first disproved one (which gives counter-example)
        Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
        // compute additional functional support
        Sim_UtilAssignFromFifo( p );
        nSolved = Sim_ComputeSuppRound( p, 1 );

if ( fVerbose )
    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
            Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
    }

exit:
p->timeTotal = Abc_Clock() - clk;
    vResult = p->vSuppFun;  
    //  p->vSuppFun = NULL;
    Sim_ManStop( p );
    return vResult;
}

Vec_Ptr_t* Sim_ComputeStrSupp

(

Abc_Ntk_t *

pNtk

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes structural supports.]

Description [Supports are returned as an array of bit strings, one for each CO.]

SideEffects []

SeeAlso []

Definition at line 57 of file simSupp.c.

{
    Vec_Ptr_t * vSuppStr;
    Abc_Obj_t * pNode;
    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
    int nSuppWords, i, k;
    // allocate room for structural supports
    nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) );
    vSuppStr   = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 );
    // assign the structural support to the PIs
    Abc_NtkForEachCi( pNtk, pNode, i )
        Sim_SuppStrSetVar( vSuppStr, pNode, i );
    // derive the structural supports of the internal nodes
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
//        if ( Abc_NodeIsConst(pNode) )
//            continue;
        pSimmNode  = (unsigned *)vSuppStr->pArray[ pNode->Id ];
        pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
        pSimmNode2 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
        for ( k = 0; k < nSuppWords; k++ )
            pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
    }
    // set the structural supports of the PO nodes
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        pSimmNode  = (unsigned *)vSuppStr->pArray[ pNode->Id ];
        pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
        for ( k = 0; k < nSuppWords; k++ )
            pSimmNode[k] = pSimmNode1[k];
    }
    return vSuppStr;
}

int Sim_ComputeTwoVarSymms	(	Abc_Ntk_t *	pNtk,
		int	fVerbose
	)

DECLARATIONS ///.

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

FileName [simSym.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Simulation to determine two-variable symmetries.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Computes two variable symmetries.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file simSym.c.

{
    Sym_Man_t * p;
    Vec_Ptr_t * vResult;
    int Result;
    int i;
    abctime clk, clkTotal = Abc_Clock();

    srand( 0xABC );

    // start the simulation manager
    p = Sym_ManStart( pNtk, fVerbose );
    p->nPairsTotal = p->nPairsRem = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
    if ( fVerbose )
        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
               p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );

    // detect symmetries using circuit structure
clk = Abc_Clock();
    Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
p->timeStruct = Abc_Clock() - clk;

    Sim_UtilCountPairsAll( p );
    p->nPairsSymmStr = p->nPairsSymm;
    if ( fVerbose )
        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
            p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );

    // detect symmetries using simulation
    for ( i = 1; i <= 1000; i++ )
    {
        // simulate this pattern
        Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
        if ( i % 50 != 0 )
            continue;
        // check disjointness
        assert( Sim_UtilMatrsAreDisjoint( p ) );
        // count the number of pairs
        Sim_UtilCountPairsAll( p );
        if ( i % 500 != 0 )
            continue;
        if ( fVerbose )
            printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
                p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
    }

    // detect symmetries using SAT
    for ( i = 1; Sim_SymmsGetPatternUsingSat( p, p->uPatRand ); i++ )
    {
        // simulate this pattern in four polarities
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
        Sim_XorBit( p->uPatRand, p->iVar1 );
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
        Sim_XorBit( p->uPatRand, p->iVar2 );
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
        Sim_XorBit( p->uPatRand, p->iVar1 );
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
        Sim_XorBit( p->uPatRand, p->iVar2 );
/*
        // try the previuos pair
        Sim_XorBit( p->uPatRand, p->iVar1Old );
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
        Sim_XorBit( p->uPatRand, p->iVar2Old );
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
        Sim_XorBit( p->uPatRand, p->iVar1Old );
        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
*/
        if ( i % 10 != 0 )
            continue;
        // check disjointness
        assert( Sim_UtilMatrsAreDisjoint( p ) );
        // count the number of pairs
        Sim_UtilCountPairsAll( p );
        if ( i % 50 != 0 )
            continue;
        if ( fVerbose )
            printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
                p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
    }

    // count the number of pairs
    Sim_UtilCountPairsAll( p );
    if ( fVerbose )
        printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
            p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
//    Sim_UtilCountPairsAllPrint( p );

    Result = p->nPairsSymm;
    vResult = p->vMatrSymms;  
p->timeTotal = Abc_Clock() - clkTotal;
    //  p->vMatrSymms = NULL;
    Sym_ManStop( p );
    return Result;
}

Sim_Pat_t* Sim_ManPatAlloc

(

Sim_Man_t *

p

)

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

Synopsis [Returns one simulation pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file simMan.c.

{
    Sim_Pat_t * pPat;
    pPat = (Sim_Pat_t *)Extra_MmFixedEntryFetch( p->pMmPat );
    pPat->Output = -1;
    pPat->pData  = (unsigned *)((char *)pPat + sizeof(Sim_Pat_t));
    memset( pPat->pData, 0, p->nSuppWords * sizeof(unsigned) );
    return pPat;
}

void Sim_ManPatFree	(	Sim_Man_t *	p,
		Sim_Pat_t *	pPat
	)

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

Synopsis [Returns one simulation pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file simMan.c.

{
    Extra_MmFixedEntryRecycle( p->pMmPat, (char *)pPat );
}

void Sim_ManPrintStats

(

Sim_Man_t *

p

)

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

Synopsis [Prints the manager statisticis.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file simMan.c.

{
//    printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", 
//        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
    printf( "Total func supps   = %8d.\n", Sim_UtilCountSuppSizes(p, 0) );
    printf( "Total struct supps = %8d.\n", Sim_UtilCountSuppSizes(p, 1) );
    printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
    printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
    ABC_PRT( "Simulation  ", p->timeSim );
    ABC_PRT( "Traversal   ", p->timeTrav );
    ABC_PRT( "Fraiging    ", p->timeFraig );
    ABC_PRT( "SAT         ", p->timeSat );
    ABC_PRT( "TOTAL       ", p->timeTotal );
}

Sim_Man_t* Sim_ManStart	(	Abc_Ntk_t *	pNtk,
		int	fLightweight
	)

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

Synopsis [Starts the simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 166 of file simMan.c.

{
    Sim_Man_t * p;
    // start the manager
    p = ABC_ALLOC( Sim_Man_t, 1 );
    memset( p, 0, sizeof(Sim_Man_t) );
    p->pNtk = pNtk;
    p->nInputs    = Abc_NtkCiNum(p->pNtk);
    p->nOutputs   = Abc_NtkCoNum(p->pNtk);
    // internal simulation information
    p->nSimBits   = 2048;
    p->nSimWords  = SIM_NUM_WORDS(p->nSimBits);
    p->vSim0      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
    p->fLightweight = fLightweight;
    if (!p->fLightweight) {
        p->vSim1      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
        // support information
        p->nSuppBits  = Abc_NtkCiNum(pNtk);
        p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits);
        p->vSuppStr   = Sim_ComputeStrSupp( pNtk );
        p->vSuppFun   = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk),  p->nSuppWords, 1 );
        // other data
        p->pMmPat     = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) ); 
        p->vFifo      = Vec_PtrAlloc( 100 );
        p->vDiffs     = Vec_IntAlloc( 100 );
        // allocate support targets (array of unresolved outputs for each input)
        p->vSuppTargs = Vec_VecStart( p->nInputs );
    }
    return p;
}

void Sim_ManStop

(

Sim_Man_t *

p

)

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

Synopsis [Stops the simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file simMan.c.

{
    Sim_ManPrintStats( p );
    if ( p->vSim0 )        Sim_UtilInfoFree( p->vSim0 );       
    if ( p->vSim1 )        Sim_UtilInfoFree( p->vSim1 );       
    if ( p->vSuppStr )     Sim_UtilInfoFree( p->vSuppStr );    
//    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );    
    if ( p->vSuppTargs )   Vec_VecFree( p->vSuppTargs );
    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat );
    if ( p->vFifo )        Vec_PtrFree( p->vFifo );
    if ( p->vDiffs )       Vec_IntFree( p->vDiffs );
    ABC_FREE( p );
}

Vec_Ptr_t* Sim_SimulateSeqModel	(	Abc_Ntk_t *	pNtk,
		int	nFrames,
		int *	pModel
	)

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

Synopsis [Simulates sequential circuit.]

Description [Takes sequential circuit (pNtk). Simulates the given number (nFrames) of the circuit with the given model. The model is assumed to contain values of PIs for each frame. The latches are initialized to the initial state. One word of data is simulated.]

SideEffects []

SeeAlso []

Definition at line 92 of file simSeq.c.

{
    Vec_Ptr_t * vInfo;
    Abc_Obj_t * pNode;
    unsigned * pUnsigned;
    int i, k;
    vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nFrames, 0 );
    // set the constant data
    pNode = Abc_AigConst1(pNtk);
    Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nFrames, 1 );
    // set the random PI data
    Abc_NtkForEachPi( pNtk, pNode, i )
    {
        pUnsigned = Sim_SimInfoGet(vInfo,pNode);
        for ( k = 0; k < nFrames; k++ )
            pUnsigned[k] = pModel[k * Abc_NtkPiNum(pNtk) + i] ? ~((unsigned)0) : 0;
    }
    // set the initial state data
    Abc_NtkForEachLatch( pNtk, pNode, i )
    {
        pUnsigned = Sim_SimInfoGet(vInfo,pNode);
        if ( Abc_LatchIsInit0(pNode) )
            pUnsigned[0] = 0;
        else if ( Abc_LatchIsInit1(pNode) )
            pUnsigned[0] = ~((unsigned)0);
        else 
            pUnsigned[0] = SIM_RANDOM_UNSIGNED;
    }
    // simulate the nodes for the given number of timeframes
    for ( i = 0; i < nFrames; i++ )
        Sim_SimulateSeqFrame( vInfo, pNtk, i, 1, (int)(i < nFrames-1) );
/*
    // print the simulated values
    for ( i = 0; i < nFrames; i++ )
    {
        printf( "Frame %d : ", i+1 );
        Abc_NtkForEachPi( pNtk, pNode, k )
            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
        printf( " " );
        Abc_NtkForEachLatch( pNtk, pNode, k )
            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
        printf( " " );
        Abc_NtkForEachPo( pNtk, pNode, k )
            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
        printf( "\n" );
    }
    printf( "\n" );
*/
    return vInfo;
}

Vec_Ptr_t* Sim_SimulateSeqRandom	(	Abc_Ntk_t *	pNtk,
		int	nFrames,
		int	nWords
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Simulates sequential circuit.]

Description [Takes sequential circuit (pNtk). Simulates the given number (nFrames) of the circuit with the given number of machine words (nWords) of random simulation data, starting from the initial state. If the initial state of some latches is a don't-care, uses random input for that latch.]

SideEffects []

SeeAlso []

Definition at line 51 of file simSeq.c.

{
    Vec_Ptr_t * vInfo;
    Abc_Obj_t * pNode;
    int i;
    assert( Abc_NtkIsStrash(pNtk) );
    vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nWords * nFrames, 0 );
    // set the constant data
    pNode = Abc_AigConst1(pNtk);
    Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames, 1 );
    // set the random PI data
    Abc_NtkForEachPi( pNtk, pNode, i )
        Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames );
    // set the initial state data
    Abc_NtkForEachLatch( pNtk, pNode, i )
        if ( Abc_LatchIsInit0(pNode) )
            Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 0 );
        else if ( Abc_LatchIsInit1(pNode) )
            Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 1 );
        else 
            Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords );
    // simulate the nodes for the given number of timeframes
    for ( i = 0; i < nFrames; i++ )
        Sim_SimulateSeqFrame( vInfo, pNtk, i, nWords, (int)(i < nFrames-1) );
    return vInfo;
}

int Sim_SymmsGetPatternUsingSat	(	Sym_Man_t *	p,
		unsigned *	pPattern
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Tries to prove the remaining pairs using SAT.]

Description [Continues to prove as long as it encounters symmetric pairs. Returns 1 if a non-symmetric pair is found (which gives a counter-example). Returns 0 if it finishes considering all pairs for all outputs.]

SideEffects []

SeeAlso []

Definition at line 51 of file simSymSat.c.

{
    Vec_Int_t * vSupport;
    Extra_BitMat_t * pMatSym, * pMatNonSym;
    int Index1, Index2, Index3, IndexU, IndexV;
    int v, u, i, k, b, out;

    // iterate through outputs
    for ( out = p->iOutput; out < p->nOutputs; out++ )
    {
        pMatSym    = (Extra_BitMat_t *)Vec_PtrEntry( p->vMatrSymms,    out );
        pMatNonSym = (Extra_BitMat_t *)Vec_PtrEntry( p->vMatrNonSymms, out );

        // go through the remaining variable pairs
        vSupport = Vec_VecEntryInt( p->vSupports, out );
        Vec_IntForEachEntry( vSupport, v, Index1 )
        Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
        {
            if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
                continue;
            p->nSatRuns++;

            // collect the support variables that are symmetric with u and v
            Vec_IntClear( p->vVarsU );
            Vec_IntClear( p->vVarsV );
            Vec_IntForEachEntry( vSupport, b, Index3 )
            {
                if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
                    Vec_IntPush( p->vVarsU, b );
                if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
                    Vec_IntPush( p->vVarsV, b );
            }

            if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
            { // update the symmetric variable info            
                p->nSatRunsUnsat++;
                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
                {
                    Extra_BitMatrixInsert1( pMatSym,  i, k );  // Theorem 1
                    Extra_BitMatrixInsert2( pMatSym,  i, k );  // Theorem 1
                    Extra_BitMatrixOrTwo( pMatNonSym, i, k );  // Theorem 2
                }
            }
            else
            { // update the assymmetric variable info
                p->nSatRunsSat++;
                Vec_IntForEachEntry( p->vVarsU, i, IndexU )
                Vec_IntForEachEntry( p->vVarsV, k, IndexV )
                {
                    Extra_BitMatrixInsert1( pMatNonSym, i, k );   // Theorem 3
                    Extra_BitMatrixInsert2( pMatNonSym, i, k );   // Theorem 3
                }

                // remember the out
                p->iOutput = out;
                p->iVar1Old = p->iVar1;
                p->iVar2Old = p->iVar2;
                p->iVar1 = v;
                p->iVar2 = u;
                return 1;

            }
        }
        // make sure that the symmetry matrix contains only cliques
        assert( Extra_BitMatrixIsClique( pMatSym ) );
    }

    // mark that we finished all outputs
    p->iOutput = p->nOutputs;
    return 0;
}

void Sim_SymmsSimulate	(	Sym_Man_t *	p,
		unsigned *	pPat,
		Vec_Ptr_t *	vMatrsNonSym
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Detects non-symmetric pairs using one pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file simSymSim.c.

{
    Abc_Obj_t * pNode;
    int i, nPairsTotal, nPairsSym, nPairsNonSym;
    abctime clk;

    // create the simulation matrix
    Sim_SymmsCreateSquare( p, pPat );
    // simulate each node in the DFS order
clk = Abc_Clock();
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pNode, i )
    {
//        if ( Abc_NodeIsConst(pNode) )
//            continue;
        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
    }
p->timeSim += Abc_Clock() - clk;
    // collect info into the CO matrices
clk = Abc_Clock();
    Abc_NtkForEachCo( p->pNtk, pNode, i )
    {
        pNode = Abc_ObjFanin0(pNode);
//        if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
//            continue;
        nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
        nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
        nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
        if ( nPairsTotal == nPairsSym + nPairsNonSym )
            continue;
        Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i );
    }
p->timeMatr += Abc_Clock() - clk;
}

void Sim_SymmsStructCompute	(	Abc_Ntk_t *	pNtk,
		Vec_Ptr_t *	vMatrs,
		Vec_Ptr_t *	vSuppFun
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes symmetries for a single output function.]

Description []

SideEffects []

SeeAlso []

Definition at line 61 of file simSymStr.c.

{
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pTemp;
    int * pMap, i;

    assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) );

    // get the structural support
    pNtk->vSupps = Sim_ComputeStrSupp( pNtk );
    // set elementary info for the CIs
    Abc_NtkForEachCi( pNtk, pTemp, i )
        SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) );
    // create the map of CI ids into their numbers
    pMap = Sim_SymmsCreateMap( pNtk );
    // collect the nodes in the TFI cone of this output
    vNodes = Abc_NtkDfs( pNtk, 0 );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )
    {
//        if ( Abc_NodeIsConst(pTemp) )
//            continue;
        Sim_SymmsStructComputeOne( pNtk, pTemp, pMap );
    }
    // collect the results for the COs;
    Abc_NtkForEachCo( pNtk, pTemp, i )
    {
//printf( "Output %d:\n", i );
        pTemp = Abc_ObjFanin0(pTemp);
        if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) )
            continue;
        Sim_SymmsTransferToMatrix( (Extra_BitMat_t *)Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), (unsigned *)Vec_PtrEntry(vSuppFun, i) );
    }
    // clean the intermediate results
    Sim_UtilInfoFree( pNtk->vSupps );
    pNtk->vSupps = NULL;
    Abc_NtkForEachCi( pNtk, pTemp, i )
        Vec_IntFree( SIM_READ_SYMMS(pTemp) );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )
//        if ( !Abc_NodeIsConst(pTemp) )
            Vec_IntFree( SIM_READ_SYMMS(pTemp) );
    Vec_PtrFree( vNodes );
    ABC_FREE( pMap );
}

int Sim_UtilCountAllPairs	(	Vec_Ptr_t *	vSuppFun,
		int	nSimWords,
		Vec_Int_t *	vCounters
	)

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

Synopsis [Counts the total number of pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 563 of file simUtils.c.

{
    unsigned * pSupp;
    int Counter, nOnes, nPairs, i;
    Counter = 0;
    Vec_PtrForEachEntry( unsigned *, vSuppFun, pSupp, i )
    {
        nOnes  = Sim_UtilCountOnes( pSupp, nSimWords );
        nPairs = nOnes * (nOnes - 1) / 2;
        Vec_IntWriteEntry( vCounters, i, nPairs );
        Counter += nPairs;
    }
    return Counter;
}

int Sim_UtilCountOnes	(	unsigned *	pSimInfo,
		int	nSimWords
	)

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

Synopsis [Counts the number of 1's in the bitstring.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file simUtils.c.

{
    unsigned char * pBytes;
    int nOnes, nBytes, i;
    pBytes = (unsigned char *)pSimInfo;
    nBytes = 4 * nSimWords;
    nOnes  = 0;
    for ( i = 0; i < nBytes; i++ )
        nOnes += bit_count[ pBytes[i] ];
    return nOnes;    
}

Vec_Int_t* Sim_UtilCountOnesArray	(	Vec_Ptr_t *	vInfo,
		int	nSimWords
	)

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

Synopsis [Counts the number of 1's in the bitstring.]

Description []

SideEffects []

SeeAlso []

Definition at line 425 of file simUtils.c.

{
    Vec_Int_t * vCounters;
    unsigned * pSimInfo;
    int i;
    vCounters = Vec_IntStart( Vec_PtrSize(vInfo) );
    Vec_PtrForEachEntry( unsigned *, vInfo, pSimInfo, i )
        Vec_IntWriteEntry( vCounters, i, Sim_UtilCountOnes(pSimInfo, nSimWords) );
    return vCounters;
}

void Sim_UtilCountPairsAll

(

Sym_Man_t *

p

)

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

Synopsis [Counts the number of entries in the array of matrices.]

Description []

SideEffects []

SeeAlso []

Definition at line 659 of file simUtils.c.

{
    int nPairsTotal, nPairsSym, nPairsNonSym, i;
    abctime clk;
clk = Abc_Clock();
    p->nPairsSymm    = 0;
    p->nPairsNonSymm = 0;
    for ( i = 0; i < p->nOutputs; i++ )
    {
        nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
        nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
        nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
        if ( nPairsTotal == nPairsSym + nPairsNonSym )
        {
            p->nPairsSymm    += nPairsSym;
            p->nPairsNonSymm += nPairsNonSym;
            continue;
        }
        nPairsSym    = Sim_UtilCountPairsOne( (Extra_BitMat_t *)Vec_PtrEntry(p->vMatrSymms,   i), Vec_VecEntryInt(p->vSupports, i) );
        nPairsNonSym = Sim_UtilCountPairsOne( (Extra_BitMat_t *)Vec_PtrEntry(p->vMatrNonSymms,i), Vec_VecEntryInt(p->vSupports, i) );
        assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
        Vec_IntWriteEntry( p->vPairsSym,    i, nPairsSym );
        Vec_IntWriteEntry( p->vPairsNonSym, i, nPairsNonSym );
        p->nPairsSymm    += nPairsSym;
        p->nPairsNonSymm += nPairsNonSym;
//        printf( "%d ", nPairsTotal - nPairsSym - nPairsNonSym );
    }
//printf( "\n" );
    p->nPairsRem = p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm;
p->timeCount += Abc_Clock() - clk;
}

int Sim_UtilCountSuppSizes	(	Sim_Man_t *	p,
		int	fStruct
	)

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

Synopsis [Returns 1 if the simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 371 of file simUtils.c.

{
    Abc_Obj_t * pNode, * pNodeCi;
    int i, v, Counter;
    Counter = 0;
    if ( fStruct )
    {
        Abc_NtkForEachCo( p->pNtk, pNode, i )
            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
                Counter += Sim_SuppStrHasVar( p->vSuppStr, pNode, v );
    }
    else
    {
        Abc_NtkForEachCo( p->pNtk, pNode, i )
            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
                Counter += Sim_SuppFunHasVar( p->vSuppFun, i, v );
    }
    return Counter;
}

void Sim_UtilInfoAdd	(	unsigned *	pInfo1,
		unsigned *	pInfo2,
		int	nWords
	)

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

Synopsis [Adds the second supp-info the first.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file simUtils.c.

{
    int w;
    for ( w = 0; w < nWords; w++ )
        pInfo1[w] |= pInfo2[w];
}

Vec_Ptr_t* Sim_UtilInfoAlloc	(	int	nSize,
		int	nWords,
		int	fClean
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates simulation information for all nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 57 of file simUtils.c.

{
    Vec_Ptr_t * vInfo;
    int i;
    assert( nSize > 0 && nWords > 0 );
    vInfo = Vec_PtrAlloc( nSize );
    vInfo->pArray[0] = ABC_ALLOC( unsigned, nSize * nWords );
    if ( fClean )
        memset( vInfo->pArray[0], 0, sizeof(unsigned) * nSize * nWords );
    for ( i = 1; i < nSize; i++ )
        vInfo->pArray[i] = ((unsigned *)vInfo->pArray[i-1]) + nWords;
    vInfo->nSize = nSize;
    return vInfo;
}

int Sim_UtilInfoCompare	(	Sim_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Returns 1 if the simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file simUtils.c.

{
    unsigned * pSimInfo1, * pSimInfo2;
    int k;
    pSimInfo1 = (unsigned *)p->vSim0->pArray[pNode->Id];
    pSimInfo2 = (unsigned *)p->vSim1->pArray[pNode->Id];
    for ( k = 0; k < p->nSimWords; k++ )
        if ( pSimInfo2[k] != pSimInfo1[k] )
            return 0;
    return 1;
}

void Sim_UtilInfoDetectDiffs	(	unsigned *	pInfo1,
		unsigned *	pInfo2,
		int	nWords,
		Vec_Int_t *	vDiffs
	)

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

Synopsis [Returns the positions where pInfo2 is 1 while pInfo1 is 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file simUtils.c.

{
    int w, b;
    unsigned uMask;
    vDiffs->nSize = 0;
    for ( w = 0; w < nWords; w++ )
        if ( (uMask = (pInfo2[w] ^ pInfo1[w])) )
            for ( b = 0; b < 32; b++ )
                if ( uMask & (1 << b) )
                    Vec_IntPush( vDiffs, 32*w + b );
}

void Sim_UtilInfoDetectNews	(	unsigned *	pInfo1,
		unsigned *	pInfo2,
		int	nWords,
		Vec_Int_t *	vDiffs
	)

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

Synopsis [Returns the positions where pInfo2 is 1 while pInfo1 is 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file simUtils.c.

{
    int w, b;
    unsigned uMask;
    vDiffs->nSize = 0;
    for ( w = 0; w < nWords; w++ )
        if ( (uMask = (pInfo2[w] & ~pInfo1[w])) )
            for ( b = 0; b < 32; b++ )
                if ( uMask & (1 << b) )
                    Vec_IntPush( vDiffs, 32*w + b );
}

void Sim_UtilInfoFlip	(	Sim_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Flips the simulation info of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file simUtils.c.

{
    unsigned * pSimInfo1, * pSimInfo2;
    int k;
    pSimInfo1 = (unsigned *)p->vSim0->pArray[pNode->Id];
    pSimInfo2 = (unsigned *)p->vSim1->pArray[pNode->Id];
    for ( k = 0; k < p->nSimWords; k++ )
        pSimInfo2[k] = ~pSimInfo1[k];
}

void Sim_UtilInfoFree

(

Vec_Ptr_t *

p

)

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

Synopsis [Allocates simulation information for all nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 83 of file simUtils.c.

{
    ABC_FREE( p->pArray[0] );
    Vec_PtrFree( p );
}

int Sim_UtilInfoIsClause	(	unsigned *	pPats1,
		unsigned *	pPats2,
		int	nSimWords
	)

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

Synopsis [Returns 1 if Node1 v Node2 is always true.]

Description []

SideEffects []

SeeAlso []

Definition at line 543 of file simUtils.c.

{
    int k;
    for ( k = 0; k < nSimWords; k++ )
        if ( ~pPats1[k] & ~pPats2[k] )
            return 0;
    return 1;
}

int Sim_UtilInfoIsEqual	(	unsigned *	pPats1,
		unsigned *	pPats2,
		int	nSimWords
	)

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

Synopsis [Returns 1 if equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 503 of file simUtils.c.

{
    int k;
    for ( k = 0; k < nSimWords; k++ )
        if ( pPats1[k] != pPats2[k] )
            return 0;
    return 1;
}

int Sim_UtilInfoIsImp	(	unsigned *	pPats1,
		unsigned *	pPats2,
		int	nSimWords
	)

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

Synopsis [Returns 1 if Node1 implies Node2.]

Description []

SideEffects []

SeeAlso []

Definition at line 523 of file simUtils.c.

{
    int k;
    for ( k = 0; k < nSimWords; k++ )
        if ( pPats1[k] & ~pPats2[k] )
            return 0;
    return 1;
}

int Sim_UtilMatrsAreDisjoint

(

Sym_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 703 of file simUtils.c.

{
    int i;
    for ( i = 0; i < p->nOutputs; i++ )
        if ( !Extra_BitMatrixIsDisjoint( (Extra_BitMat_t *)Vec_PtrEntry(p->vMatrSymms,i), (Extra_BitMat_t *)Vec_PtrEntry(p->vMatrNonSymms,i) ) )
            return 0;
    return 1;
}

void Sim_UtilSetCompl	(	unsigned *	pPatRand,
		int	nSimWords
	)

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

Synopsis [Returns complemented patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 465 of file simUtils.c.

{
    int k;
    for ( k = 0; k < nSimWords; k++ )
        pPatRand[k] = ~pPatRand[k];
}

void Sim_UtilSetConst	(	unsigned *	pPatRand,
		int	nSimWords,
		int	fConst1
	)

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

Synopsis [Returns constant patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 483 of file simUtils.c.

{
    int k;
    for ( k = 0; k < nSimWords; k++ )
        pPatRand[k] = 0;
    if ( fConst1 )
        Sim_UtilSetCompl( pPatRand, nSimWords );
}

void Sim_UtilSetRandom	(	unsigned *	pPatRand,
		int	nSimWords
	)

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

Synopsis [Returns random patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 447 of file simUtils.c.

{
    int k;
    for ( k = 0; k < nSimWords; k++ )
        pPatRand[k] = SIM_RANDOM_UNSIGNED;
}

void Sim_UtilSimulate	(	Sim_Man_t *	p,
		int	fType
	)

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

Synopsis [Simulates the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file simUtils.c.

{
    Abc_Obj_t * pNode;
    int i;
    // simulate the internal nodes
    Abc_NtkForEachNode( p->pNtk, pNode, i )
        Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
    // assign simulation info of the CO nodes
    Abc_NtkForEachCo( p->pNtk, pNode, i )
        Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
}

void Sim_UtilSimulateNode	(	Sim_Man_t *	p,
		Abc_Obj_t *	pNode,
		int	fType,
		int	fType1,
		int	fType2
	)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 231 of file simUtils.c.

{
    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
    int k, fComp1, fComp2;
    // simulate the internal nodes
    if ( Abc_ObjIsNode(pNode) )
    {
        if ( fType )
            pSimmNode  = (unsigned *)p->vSim1->pArray[ pNode->Id ];
        else
            pSimmNode  = (unsigned *)p->vSim0->pArray[ pNode->Id ];

        if ( fType1 )
            pSimmNode1 = (unsigned *)p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
        else
            pSimmNode1 = (unsigned *)p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];

        if ( fType2 )
            pSimmNode2 = (unsigned *)p->vSim1->pArray[ Abc_ObjFaninId1(pNode) ];
        else
            pSimmNode2 = (unsigned *)p->vSim0->pArray[ Abc_ObjFaninId1(pNode) ];

        fComp1 = Abc_ObjFaninC0(pNode);
        fComp2 = Abc_ObjFaninC1(pNode);
        if ( fComp1 && fComp2 )
            for ( k = 0; k < p->nSimWords; k++ )
                pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
        else if ( fComp1 && !fComp2 )
            for ( k = 0; k < p->nSimWords; k++ )
                pSimmNode[k] = ~pSimmNode1[k] &  pSimmNode2[k];
        else if ( !fComp1 && fComp2 )
            for ( k = 0; k < p->nSimWords; k++ )
                pSimmNode[k] =  pSimmNode1[k] & ~pSimmNode2[k];
        else // if ( fComp1 && fComp2 )
            for ( k = 0; k < p->nSimWords; k++ )
                pSimmNode[k] =  pSimmNode1[k] &  pSimmNode2[k];
    }
    else 
    {
        assert( Abc_ObjFaninNum(pNode) == 1 );
        if ( fType )
            pSimmNode  = (unsigned *)p->vSim1->pArray[ pNode->Id ];
        else
            pSimmNode  = (unsigned *)p->vSim0->pArray[ pNode->Id ];

        if ( fType1 )
            pSimmNode1 = (unsigned *)p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
        else
            pSimmNode1 = (unsigned *)p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];

        fComp1 = Abc_ObjFaninC0(pNode);
        if ( fComp1 )
            for ( k = 0; k < p->nSimWords; k++ )
                pSimmNode[k] = ~pSimmNode1[k];
        else 
            for ( k = 0; k < p->nSimWords; k++ )
                pSimmNode[k] =  pSimmNode1[k];
    }
}

void Sim_UtilSimulateNodeOne	(	Abc_Obj_t *	pNode,
		Vec_Ptr_t *	vSimInfo,
		int	nSimWords,
		int	nOffset
	)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 302 of file simUtils.c.

{
    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
    int k, fComp1, fComp2;
    // simulate the internal nodes
    assert( Abc_ObjIsNode(pNode) );
    pSimmNode  = (unsigned *)Vec_PtrEntry(vSimInfo, pNode->Id);
    pSimmNode1 = (unsigned *)Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
    pSimmNode2 = (unsigned *)Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
    pSimmNode  += nOffset;
    pSimmNode1 += nOffset;
    pSimmNode2 += nOffset;
    fComp1 = Abc_ObjFaninC0(pNode);
    fComp2 = Abc_ObjFaninC1(pNode);
    if ( fComp1 && fComp2 )
        for ( k = 0; k < nSimWords; k++ )
            pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
    else if ( fComp1 && !fComp2 )
        for ( k = 0; k < nSimWords; k++ )
            pSimmNode[k] = ~pSimmNode1[k] &  pSimmNode2[k];
    else if ( !fComp1 && fComp2 )
        for ( k = 0; k < nSimWords; k++ )
            pSimmNode[k] =  pSimmNode1[k] & ~pSimmNode2[k];
    else // if ( fComp1 && fComp2 )
        for ( k = 0; k < nSimWords; k++ )
            pSimmNode[k] =  pSimmNode1[k] &  pSimmNode2[k];
}

void Sim_UtilTransferNodeOne	(	Abc_Obj_t *	pNode,
		Vec_Ptr_t *	vSimInfo,
		int	nSimWords,
		int	nOffset,
		int	fShift
	)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 341 of file simUtils.c.

{
    unsigned * pSimmNode, * pSimmNode1;
    int k, fComp1;
    // simulate the internal nodes
    assert( Abc_ObjIsCo(pNode) );
    pSimmNode  = (unsigned *)Vec_PtrEntry(vSimInfo, pNode->Id);
    pSimmNode1 = (unsigned *)Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
    pSimmNode  += nOffset + (fShift > 0)*nSimWords;
    pSimmNode1 += nOffset;
    fComp1 = Abc_ObjFaninC0(pNode);
    if ( fComp1 )
        for ( k = 0; k < nSimWords; k++ )
            pSimmNode[k] = ~pSimmNode1[k];
    else 
        for ( k = 0; k < nSimWords; k++ )
            pSimmNode[k] =  pSimmNode1[k];
}

void Sym_ManPrintStats

(

Sym_Man_t *

p

)

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

Synopsis [Prints the manager statisticis.]

Description []

SideEffects []

SeeAlso []

Definition at line 135 of file simMan.c.

{
//    printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", 
//        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
    printf( "Total symm         = %8d.\n", p->nPairsSymm );
    printf( "Structural symm    = %8d.\n", p->nPairsSymmStr );
    printf( "Total non-sym      = %8d.\n", p->nPairsNonSymm );
    printf( "Total var pairs    = %8d.\n", p->nPairsTotal );
    printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
    printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
    ABC_PRT( "Structural  ", p->timeStruct );
    ABC_PRT( "Simulation  ", p->timeSim );
    ABC_PRT( "Matrix      ", p->timeMatr );
    ABC_PRT( "Counting    ", p->timeCount );
    ABC_PRT( "Fraiging    ", p->timeFraig );
    ABC_PRT( "SAT         ", p->timeSat );
    ABC_PRT( "TOTAL       ", p->timeTotal );
}

Sym_Man_t* Sym_ManStart	(	Abc_Ntk_t *	pNtk,
		int	fVerbose
	)

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

FileName [simMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Simulation manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Starts the simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file simMan.c.

{
    Sym_Man_t * p;
    int i, v; 
    // start the manager
    p = ABC_ALLOC( Sym_Man_t, 1 );
    memset( p, 0, sizeof(Sym_Man_t) );
    p->pNtk = pNtk;
    p->vNodes     = Abc_NtkDfs( pNtk, 0 );
    p->nInputs    = Abc_NtkCiNum(p->pNtk);
    p->nOutputs   = Abc_NtkCoNum(p->pNtk);
    // internal simulation information
    p->nSimWords  = SIM_NUM_WORDS(p->nInputs);
    p->vSim       = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
    // symmetry info for each output
    p->vMatrSymms    = Vec_PtrStart( p->nOutputs );
    p->vMatrNonSymms = Vec_PtrStart( p->nOutputs );
    p->vPairsTotal   = Vec_IntStart( p->nOutputs );
    p->vPairsSym     = Vec_IntStart( p->nOutputs );
    p->vPairsNonSym  = Vec_IntStart( p->nOutputs );
    for ( i = 0; i < p->nOutputs; i++ )
    {
        p->vMatrSymms->pArray[i]    = Extra_BitMatrixStart( p->nInputs );
        p->vMatrNonSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs );
    }
    // temporary patterns
    p->uPatRand = ABC_ALLOC( unsigned, p->nSimWords );
    p->uPatCol  = ABC_ALLOC( unsigned, p->nSimWords );
    p->uPatRow  = ABC_ALLOC( unsigned, p->nSimWords );
    p->vVarsU   = Vec_IntStart( 100 );
    p->vVarsV   = Vec_IntStart( 100 );
    // compute supports
    p->vSuppFun  = Sim_ComputeFunSupp( pNtk, fVerbose );
    p->vSupports = Vec_VecStart( p->nOutputs );
    for ( i = 0; i < p->nOutputs; i++ )
        for ( v = 0; v < p->nInputs; v++ )
            if ( Sim_SuppFunHasVar( p->vSuppFun, i, v ) )
                Vec_VecPush( p->vSupports, i, (void *)(ABC_PTRUINT_T)v );
    return p;
}

void Sym_ManStop

(

Sym_Man_t *

p

)

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

Synopsis [Stops the simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file simMan.c.

{
    int i;
    Sym_ManPrintStats( p );
    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );   
    if ( p->vSim )         Sim_UtilInfoFree( p->vSim );   
    if ( p->vNodes )       Vec_PtrFree( p->vNodes );
    if ( p->vSupports )    Vec_VecFree( p->vSupports );
    for ( i = 0; i < p->nOutputs; i++ )
    {
        Extra_BitMatrixStop( (Extra_BitMat_t *)p->vMatrSymms->pArray[i] );
        Extra_BitMatrixStop( (Extra_BitMat_t *)p->vMatrNonSymms->pArray[i] );
    }
    Vec_IntFree( p->vVarsU );
    Vec_IntFree( p->vVarsV );
    Vec_PtrFree( p->vMatrSymms );
    Vec_PtrFree( p->vMatrNonSymms );
    Vec_IntFree( p->vPairsTotal );
    Vec_IntFree( p->vPairsSym );
    Vec_IntFree( p->vPairsNonSym );
    ABC_FREE( p->uPatRand );
    ABC_FREE( p->uPatCol );
    ABC_FREE( p->uPatRow );
    ABC_FREE( p );
}