src/opt/sim/sim.h File Reference

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

Go to the source code of this file.

Data Structures

struct  Sym_Man_t_
struct  Sim_Man_t_
struct  Sim_Pat_t_

Defines

#define SIM_NUM_WORDS(n)   (((n)>>5) + (((n)&31) > 0))
#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 struct Sym_Man_t_ Sym_Man_t
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)
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)
Vec_Ptr_t * Sim_SimulateSeqModel (Abc_Ntk_t *pNtk, int nFrames, int *pModel)
Vec_Ptr_t * Sim_ComputeStrSupp (Abc_Ntk_t *pNtk)
Vec_Ptr_t * Sim_ComputeFunSupp (Abc_Ntk_t *pNtk, int fVerbose)
int Sim_ComputeTwoVarSymms (Abc_Ntk_t *pNtk, int fVerbose)
int Sim_SymmsGetPatternUsingSat (Sym_Man_t *p, unsigned *pPattern)
void Sim_SymmsStructCompute (Abc_Ntk_t *pNtk, Vec_Ptr_t *vMatrs, Vec_Ptr_t *vSuppFun)
void Sim_SymmsSimulate (Sym_Man_t *p, unsigned *pPatRand, Vec_Ptr_t *vMatrsNonSym)
Vec_Ptr_t * Sim_UtilInfoAlloc (int nSize, int nWords, bool fClean)
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)
bool Sim_UtilInfoCompare (Sim_Man_t *p, Abc_Obj_t *pNode)
void Sim_UtilSimulate (Sim_Man_t *p, bool fFirst)
void Sim_UtilSimulateNode (Sim_Man_t *p, Abc_Obj_t *pNode, bool fType, bool fType1, bool 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)

Define Documentation

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

Definition at line 161 of file sim.h.

#define SIM_LAST_BITS ( n   )     ((((n)&31) > 0)? (n)&31 : 32)

Definition at line 147 of file sim.h.

#define SIM_MASK_BEG ( n   )     (SIM_MASK_FULL >> (32-n))

Definition at line 150 of file sim.h.

#define SIM_MASK_END ( n   )     (SIM_MASK_FULL << (n))

Definition at line 151 of file sim.h.

#define SIM_MASK_FULL   (0xFFFFFFFF)

Definition at line 149 of file sim.h.

#define SIM_NUM_WORDS ( n   )     (((n)>>5) + (((n)&31) > 0))

MACRO DEFINITIONS ///

Definition at line 146 of file sim.h.

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

Definition at line 156 of file sim.h.

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

Definition at line 152 of file sim.h.

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

Definition at line 153 of file sim.h.

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

Definition at line 159 of file sim.h.

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

Definition at line 170 of file sim.h.

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

Definition at line 169 of file sim.h.

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

Definition at line 168 of file sim.h.

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

Definition at line 167 of file sim.h.

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

Definition at line 166 of file sim.h.

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

Definition at line 165 of file sim.h.

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

Definition at line 164 of file sim.h.

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

Definition at line 160 of file sim.h.

Typedef Documentation

typedef struct Sim_Man_t_ Sim_Man_t

Definition at line 98 of file sim.h.

typedef struct Sim_Pat_t_ Sim_Pat_t

Definition at line 134 of file sim.h.

typedef struct Sym_Man_t_ Sym_Man_t

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

] INCLUDES /// PARAMETERS /// BASIC TYPES ///

Definition at line 46 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 100 of file simSupp.c.

00101 {
00102     Sim_Man_t * p;
00103     Vec_Ptr_t * vResult;
00104     int nSolved, i, clk = clock();
00105 
00106     srand( 0xABC );
00107 
00108     // start the simulation manager
00109     p = Sim_ManStart( pNtk, 0 );
00110 
00111     // compute functional support using one round of random simulation
00112     Sim_UtilAssignRandom( p );
00113     Sim_ComputeSuppRound( p, 0 );
00114 
00115     // set the support targets 
00116     Sim_ComputeSuppSetTargets( p );
00117 if ( fVerbose )
00118     printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
00119     if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
00120         goto exit;
00121 
00122     for ( i = 0; i < 1; i++ )
00123     {
00124         // compute patterns using one round of random simulation
00125         Sim_UtilAssignRandom( p );
00126         nSolved = Sim_ComputeSuppRound( p, 1 );
00127         if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
00128             goto exit;
00129 
00130 if ( fVerbose )
00131     printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", 
00132        Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
00133     }
00134 
00135     // try to solve the support targets
00136     while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
00137     {
00138         // solve targets until the first disproved one (which gives counter-example)
00139         Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
00140         // compute additional functional support
00141         Sim_UtilAssignFromFifo( p );
00142         nSolved = Sim_ComputeSuppRound( p, 1 );
00143 
00144 if ( fVerbose )
00145     printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
00146             Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
00147     }
00148 
00149 exit:
00150 p->timeTotal = clock() - clk;
00151     vResult = p->vSuppFun;  
00152     //  p->vSuppFun = NULL;
00153     Sim_ManStop( p );
00154     return vResult;
00155 }

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 54 of file simSupp.c.

00055 {
00056     Vec_Ptr_t * vSuppStr;
00057     Abc_Obj_t * pNode;
00058     unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
00059     int nSuppWords, i, k;
00060     // allocate room for structural supports
00061     nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) );
00062     vSuppStr   = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 );
00063     // assign the structural support to the PIs
00064     Abc_NtkForEachCi( pNtk, pNode, i )
00065         Sim_SuppStrSetVar( vSuppStr, pNode, i );
00066     // derive the structural supports of the internal nodes
00067     Abc_NtkForEachNode( pNtk, pNode, i )
00068     {
00069 //        if ( Abc_NodeIsConst(pNode) )
00070 //            continue;
00071         pSimmNode  = vSuppStr->pArray[ pNode->Id ];
00072         pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
00073         pSimmNode2 = vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
00074         for ( k = 0; k < nSuppWords; k++ )
00075             pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
00076     }
00077     // set the structural supports of the PO nodes
00078     Abc_NtkForEachCo( pNtk, pNode, i )
00079     {
00080         pSimmNode  = vSuppStr->pArray[ pNode->Id ];
00081         pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
00082         for ( k = 0; k < nSuppWords; k++ )
00083             pSimmNode[k] = pSimmNode1[k];
00084     }
00085     return vSuppStr;
00086 }

int Sim_ComputeTwoVarSymms ( Abc_Ntk_t *  pNtk,
int  fVerbose 
)

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

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

Synopsis [Computes two variable symmetries.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file simSym.c.

00044 {
00045     Sym_Man_t * p;
00046     Vec_Ptr_t * vResult;
00047     int Result;
00048     int i, clk, clkTotal = clock();
00049 
00050     srand( 0xABC );
00051 
00052     // start the simulation manager
00053     p = Sym_ManStart( pNtk, fVerbose );
00054     p->nPairsTotal = p->nPairsRem = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
00055     if ( fVerbose )
00056         printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
00057                p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
00058 
00059     // detect symmetries using circuit structure
00060 clk = clock();
00061     Sim_SymmsStructCompute( pNtk, p->vMatrSymms, p->vSuppFun );
00062 p->timeStruct = clock() - clk;
00063 
00064     Sim_UtilCountPairsAll( p );
00065     p->nPairsSymmStr = p->nPairsSymm;
00066     if ( fVerbose )
00067         printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
00068             p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
00069 
00070     // detect symmetries using simulation
00071     for ( i = 1; i <= 1000; i++ )
00072     {
00073         // simulate this pattern
00074         Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
00075         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
00076         if ( i % 50 != 0 )
00077             continue;
00078         // check disjointness
00079         assert( Sim_UtilMatrsAreDisjoint( p ) );
00080         // count the number of pairs
00081         Sim_UtilCountPairsAll( p );
00082         if ( i % 500 != 0 )
00083             continue;
00084         if ( fVerbose )
00085             printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
00086                 p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
00087     }
00088 
00089     // detect symmetries using SAT
00090     for ( i = 1; Sim_SymmsGetPatternUsingSat( p, p->uPatRand ); i++ )
00091     {
00092         // simulate this pattern in four polarities
00093         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
00094         Sim_XorBit( p->uPatRand, p->iVar1 );
00095         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
00096         Sim_XorBit( p->uPatRand, p->iVar2 );
00097         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
00098         Sim_XorBit( p->uPatRand, p->iVar1 );
00099         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
00100         Sim_XorBit( p->uPatRand, p->iVar2 );
00101 /*
00102         // try the previuos pair
00103         Sim_XorBit( p->uPatRand, p->iVar1Old );
00104         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
00105         Sim_XorBit( p->uPatRand, p->iVar2Old );
00106         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
00107         Sim_XorBit( p->uPatRand, p->iVar1Old );
00108         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
00109 */
00110         if ( i % 10 != 0 )
00111             continue;
00112         // check disjointness
00113         assert( Sim_UtilMatrsAreDisjoint( p ) );
00114         // count the number of pairs
00115         Sim_UtilCountPairsAll( p );
00116         if ( i % 50 != 0 )
00117             continue;
00118         if ( fVerbose )
00119             printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
00120                 p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
00121     }
00122 
00123     // count the number of pairs
00124     Sim_UtilCountPairsAll( p );
00125     if ( fVerbose )
00126         printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
00127             p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
00128 //    Sim_UtilCountPairsAllPrint( p );
00129 
00130     Result = p->nPairsSymm;
00131     vResult = p->vMatrSymms;  
00132 p->timeTotal = clock() - clkTotal;
00133     //  p->vMatrSymms = NULL;
00134     Sym_ManStop( p );
00135     return Result;
00136 }

Sim_Pat_t* Sim_ManPatAlloc ( Sim_Man_t *  p  ) 

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

Synopsis [Returns one simulation pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 258 of file simMan.c.

00259 {
00260     Sim_Pat_t * pPat;
00261     pPat = (Sim_Pat_t *)Extra_MmFixedEntryFetch( p->pMmPat );
00262     pPat->Output = -1;
00263     pPat->pData  = (unsigned *)((char *)pPat + sizeof(Sim_Pat_t));
00264     memset( pPat->pData, 0, p->nSuppWords * sizeof(unsigned) );
00265     return pPat;
00266 }

void Sim_ManPatFree ( Sim_Man_t *  p,
Sim_Pat_t *  pPat 
)

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

Synopsis [Returns one simulation pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file simMan.c.

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

void Sim_ManPrintStats ( Sim_Man_t *  p  ) 

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

Synopsis [Prints the manager statisticis.]

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file simMan.c.

00231 {
00232 //    printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", 
00233 //        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
00234     printf( "Total func supps   = %8d.\n", Sim_UtilCountSuppSizes(p, 0) );
00235     printf( "Total struct supps = %8d.\n", Sim_UtilCountSuppSizes(p, 1) );
00236     printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
00237     printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
00238     PRT( "Simulation  ", p->timeSim );
00239     PRT( "Traversal   ", p->timeTrav );
00240     PRT( "Fraiging    ", p->timeFraig );
00241     PRT( "SAT         ", p->timeSat );
00242     PRT( "TOTAL       ", p->timeTotal );
00243 }

Sim_Man_t* Sim_ManStart ( Abc_Ntk_t *  pNtk,
int  fLightweight 
)

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

Synopsis [Starts the simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file simMan.c.

00164 {
00165     Sim_Man_t * p;
00166     // start the manager
00167     p = ALLOC( Sim_Man_t, 1 );
00168     memset( p, 0, sizeof(Sim_Man_t) );
00169     p->pNtk = pNtk;
00170     p->nInputs    = Abc_NtkCiNum(p->pNtk);
00171     p->nOutputs   = Abc_NtkCoNum(p->pNtk);
00172     // internal simulation information
00173     p->nSimBits   = 2048;
00174     p->nSimWords  = SIM_NUM_WORDS(p->nSimBits);
00175     p->vSim0      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
00176     p->fLightweight = fLightweight;
00177     if (!p->fLightweight) {
00178         p->vSim1      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
00179         // support information
00180         p->nSuppBits  = Abc_NtkCiNum(pNtk);
00181         p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits);
00182         p->vSuppStr   = Sim_ComputeStrSupp( pNtk );
00183         p->vSuppFun   = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk),  p->nSuppWords, 1 );
00184         // other data
00185         p->pMmPat     = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) ); 
00186         p->vFifo      = Vec_PtrAlloc( 100 );
00187         p->vDiffs     = Vec_IntAlloc( 100 );
00188         // allocate support targets (array of unresolved outputs for each input)
00189         p->vSuppTargs = Vec_VecStart( p->nInputs );
00190     }
00191     return p;
00192 }

void Sim_ManStop ( Sim_Man_t *  p  ) 

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

Synopsis [Stops the simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file simMan.c.

00206 {
00207     Sim_ManPrintStats( p );
00208     if ( p->vSim0 )        Sim_UtilInfoFree( p->vSim0 );       
00209     if ( p->vSim1 )        Sim_UtilInfoFree( p->vSim1 );       
00210     if ( p->vSuppStr )     Sim_UtilInfoFree( p->vSuppStr );    
00211 //    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );    
00212     if ( p->vSuppTargs )   Vec_VecFree( p->vSuppTargs );
00213     if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat );
00214     if ( p->vFifo )        Vec_PtrFree( p->vFifo );
00215     if ( p->vDiffs )       Vec_IntFree( p->vDiffs );
00216     free( p );
00217 }

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 89 of file simSeq.c.

00090 {
00091     Vec_Ptr_t * vInfo;
00092     Abc_Obj_t * pNode;
00093     unsigned * pUnsigned;
00094     int i, k;
00095     vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nFrames, 0 );
00096     // set the constant data
00097     pNode = Abc_AigConst1(pNtk);
00098     Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nFrames, 1 );
00099     // set the random PI data
00100     Abc_NtkForEachPi( pNtk, pNode, i )
00101     {
00102         pUnsigned = Sim_SimInfoGet(vInfo,pNode);
00103         for ( k = 0; k < nFrames; k++ )
00104             pUnsigned[k] = pModel[k * Abc_NtkPiNum(pNtk) + i] ? ~((unsigned)0) : 0;
00105     }
00106     // set the initial state data
00107     Abc_NtkForEachLatch( pNtk, pNode, i )
00108     {
00109         pUnsigned = Sim_SimInfoGet(vInfo,pNode);
00110         if ( Abc_LatchIsInit0(pNode) )
00111             pUnsigned[0] = 0;
00112         else if ( Abc_LatchIsInit1(pNode) )
00113             pUnsigned[0] = ~((unsigned)0);
00114         else 
00115             pUnsigned[0] = SIM_RANDOM_UNSIGNED;
00116     }
00117     // simulate the nodes for the given number of timeframes
00118     for ( i = 0; i < nFrames; i++ )
00119         Sim_SimulateSeqFrame( vInfo, pNtk, i, 1, (int)(i < nFrames-1) );
00120 /*
00121     // print the simulated values
00122     for ( i = 0; i < nFrames; i++ )
00123     {
00124         printf( "Frame %d : ", i+1 );
00125         Abc_NtkForEachPi( pNtk, pNode, k )
00126             printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
00127         printf( " " );
00128         Abc_NtkForEachLatch( pNtk, pNode, k )
00129             printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
00130         printf( " " );
00131         Abc_NtkForEachPo( pNtk, pNode, k )
00132             printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
00133         printf( "\n" );
00134     }
00135     printf( "\n" );
00136 */
00137     return vInfo;
00138 }

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 48 of file simSeq.c.

00049 {
00050     Vec_Ptr_t * vInfo;
00051     Abc_Obj_t * pNode;
00052     int i;
00053     assert( Abc_NtkIsStrash(pNtk) );
00054     vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nWords * nFrames, 0 );
00055     // set the constant data
00056     pNode = Abc_AigConst1(pNtk);
00057     Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames, 1 );
00058     // set the random PI data
00059     Abc_NtkForEachPi( pNtk, pNode, i )
00060         Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames );
00061     // set the initial state data
00062     Abc_NtkForEachLatch( pNtk, pNode, i )
00063         if ( Abc_LatchIsInit0(pNode) )
00064             Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 0 );
00065         else if ( Abc_LatchIsInit1(pNode) )
00066             Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 1 );
00067         else 
00068             Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords );
00069     // simulate the nodes for the given number of timeframes
00070     for ( i = 0; i < nFrames; i++ )
00071         Sim_SimulateSeqFrame( vInfo, pNtk, i, nWords, (int)(i < nFrames-1) );
00072     return vInfo;
00073 }

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 48 of file simSymSat.c.

00049 {
00050     Vec_Int_t * vSupport;
00051     Extra_BitMat_t * pMatSym, * pMatNonSym;
00052     int Index1, Index2, Index3, IndexU, IndexV;
00053     int v, u, i, k, b, out;
00054 
00055     // iterate through outputs
00056     for ( out = p->iOutput; out < p->nOutputs; out++ )
00057     {
00058         pMatSym    = Vec_PtrEntry( p->vMatrSymms,    out );
00059         pMatNonSym = Vec_PtrEntry( p->vMatrNonSymms, out );
00060 
00061         // go through the remaining variable pairs
00062         vSupport = Vec_VecEntry( p->vSupports, out );
00063         Vec_IntForEachEntry( vSupport, v, Index1 )
00064         Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
00065         {
00066             if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
00067                 continue;
00068             p->nSatRuns++;
00069 
00070             // collect the support variables that are symmetric with u and v
00071             Vec_IntClear( p->vVarsU );
00072             Vec_IntClear( p->vVarsV );
00073             Vec_IntForEachEntry( vSupport, b, Index3 )
00074             {
00075                 if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
00076                     Vec_IntPush( p->vVarsU, b );
00077                 if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
00078                     Vec_IntPush( p->vVarsV, b );
00079             }
00080 
00081             if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
00082             { // update the symmetric variable info            
00083                 p->nSatRunsUnsat++;
00084                 Vec_IntForEachEntry( p->vVarsU, i, IndexU )
00085                 Vec_IntForEachEntry( p->vVarsV, k, IndexV )
00086                 {
00087                     Extra_BitMatrixInsert1( pMatSym,  i, k );  // Theorem 1
00088                     Extra_BitMatrixInsert2( pMatSym,  i, k );  // Theorem 1
00089                     Extra_BitMatrixOrTwo( pMatNonSym, i, k );  // Theorem 2
00090                 }
00091             }
00092             else
00093             { // update the assymmetric variable info
00094                 p->nSatRunsSat++;
00095                 Vec_IntForEachEntry( p->vVarsU, i, IndexU )
00096                 Vec_IntForEachEntry( p->vVarsV, k, IndexV )
00097                 {
00098                     Extra_BitMatrixInsert1( pMatNonSym, i, k );   // Theorem 3
00099                     Extra_BitMatrixInsert2( pMatNonSym, i, k );   // Theorem 3
00100                 }
00101 
00102                 // remember the out
00103                 p->iOutput = out;
00104                 p->iVar1Old = p->iVar1;
00105                 p->iVar2Old = p->iVar2;
00106                 p->iVar1 = v;
00107                 p->iVar2 = u;
00108                 return 1;
00109 
00110             }
00111         }
00112         // make sure that the symmetry matrix contains only cliques
00113         assert( Extra_BitMatrixIsClique( pMatSym ) );
00114     }
00115 
00116     // mark that we finished all outputs
00117     p->iOutput = p->nOutputs;
00118     return 0;
00119 }

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 46 of file simSymSim.c.

00047 {
00048     Abc_Obj_t * pNode;
00049     int i, nPairsTotal, nPairsSym, nPairsNonSym;
00050     int clk;
00051 
00052     // create the simulation matrix
00053     Sim_SymmsCreateSquare( p, pPat );
00054     // simulate each node in the DFS order
00055 clk = clock();
00056     Vec_PtrForEachEntry( p->vNodes, pNode, i )
00057     {
00058 //        if ( Abc_NodeIsConst(pNode) )
00059 //            continue;
00060         Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
00061     }
00062 p->timeSim += clock() - clk;
00063     // collect info into the CO matrices
00064 clk = clock();
00065     Abc_NtkForEachCo( p->pNtk, pNode, i )
00066     {
00067         pNode = Abc_ObjFanin0(pNode);
00068 //        if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
00069 //            continue;
00070         nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
00071         nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
00072         nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
00073         assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
00074         if ( nPairsTotal == nPairsSym + nPairsNonSym )
00075             continue;
00076         Sim_SymmsDeriveInfo( p, pPat, pNode, vMatrsNonSym, i );
00077     }
00078 p->timeMatr += clock() - clk;
00079 }

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 58 of file simSymStr.c.

00059 {
00060     Vec_Ptr_t * vNodes;
00061     Abc_Obj_t * pTemp;
00062     int * pMap, i;
00063 
00064     assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) );
00065 
00066     // get the structural support
00067     pNtk->vSupps = Sim_ComputeStrSupp( pNtk );
00068     // set elementary info for the CIs
00069     Abc_NtkForEachCi( pNtk, pTemp, i )
00070         SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) );
00071     // create the map of CI ids into their numbers
00072     pMap = Sim_SymmsCreateMap( pNtk );
00073     // collect the nodes in the TFI cone of this output
00074     vNodes = Abc_NtkDfs( pNtk, 0 );
00075     Vec_PtrForEachEntry( vNodes, pTemp, i )
00076     {
00077 //        if ( Abc_NodeIsConst(pTemp) )
00078 //            continue;
00079         Sim_SymmsStructComputeOne( pNtk, pTemp, pMap );
00080     }
00081     // collect the results for the COs;
00082     Abc_NtkForEachCo( pNtk, pTemp, i )
00083     {
00084 //printf( "Output %d:\n", i );
00085         pTemp = Abc_ObjFanin0(pTemp);
00086         if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) )
00087             continue;
00088         Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) );
00089     }
00090     // clean the intermediate results
00091     Sim_UtilInfoFree( pNtk->vSupps );
00092     pNtk->vSupps = NULL;
00093     Abc_NtkForEachCi( pNtk, pTemp, i )
00094         Vec_IntFree( SIM_READ_SYMMS(pTemp) );
00095     Vec_PtrForEachEntry( vNodes, pTemp, i )
00096 //        if ( !Abc_NodeIsConst(pTemp) )
00097             Vec_IntFree( SIM_READ_SYMMS(pTemp) );
00098     Vec_PtrFree( vNodes );
00099     free( pMap );
00100 }

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 560 of file simUtils.c.

00561 {
00562     unsigned * pSupp;
00563     int Counter, nOnes, nPairs, i;
00564     Counter = 0;
00565     Vec_PtrForEachEntry( vSuppFun, pSupp, i )
00566     {
00567         nOnes  = Sim_UtilCountOnes( pSupp, nSimWords );
00568         nPairs = nOnes * (nOnes - 1) / 2;
00569         Vec_IntWriteEntry( vCounters, i, nPairs );
00570         Counter += nPairs;
00571     }
00572     return Counter;
00573 }

int Sim_UtilCountOnes ( unsigned *  pSimInfo,
int  nSimWords 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 399 of file simUtils.c.

00400 {
00401     unsigned char * pBytes;
00402     int nOnes, nBytes, i;
00403     pBytes = (unsigned char *)pSimInfo;
00404     nBytes = 4 * nSimWords;
00405     nOnes  = 0;
00406     for ( i = 0; i < nBytes; i++ )
00407         nOnes += bit_count[ pBytes[i] ];
00408     return nOnes;    
00409 }

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 422 of file simUtils.c.

00423 {
00424     Vec_Int_t * vCounters;
00425     unsigned * pSimInfo;
00426     int i;
00427     vCounters = Vec_IntStart( Vec_PtrSize(vInfo) );
00428     Vec_PtrForEachEntry( vInfo, pSimInfo, i )
00429         Vec_IntWriteEntry( vCounters, i, Sim_UtilCountOnes(pSimInfo, nSimWords) );
00430     return vCounters;
00431 }

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 655 of file simUtils.c.

00656 {
00657     int nPairsTotal, nPairsSym, nPairsNonSym, i, clk;
00658 clk = clock();
00659     p->nPairsSymm    = 0;
00660     p->nPairsNonSymm = 0;
00661     for ( i = 0; i < p->nOutputs; i++ )
00662     {
00663         nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
00664         nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
00665         nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
00666         assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
00667         if ( nPairsTotal == nPairsSym + nPairsNonSym )
00668         {
00669             p->nPairsSymm    += nPairsSym;
00670             p->nPairsNonSymm += nPairsNonSym;
00671             continue;
00672         }
00673         nPairsSym    = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrSymms,   i), Vec_VecEntry(p->vSupports, i) );
00674         nPairsNonSym = Sim_UtilCountPairsOne( Vec_PtrEntry(p->vMatrNonSymms,i), Vec_VecEntry(p->vSupports, i) );
00675         assert( nPairsTotal >= nPairsSym + nPairsNonSym ); 
00676         Vec_IntWriteEntry( p->vPairsSym,    i, nPairsSym );
00677         Vec_IntWriteEntry( p->vPairsNonSym, i, nPairsNonSym );
00678         p->nPairsSymm    += nPairsSym;
00679         p->nPairsNonSymm += nPairsNonSym;
00680 //        printf( "%d ", nPairsTotal - nPairsSym - nPairsNonSym );
00681     }
00682 //printf( "\n" );
00683     p->nPairsRem = p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm;
00684 p->timeCount += clock() - clk;
00685 }

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 368 of file simUtils.c.

00369 {
00370     Abc_Obj_t * pNode, * pNodeCi;
00371     int i, v, Counter;
00372     Counter = 0;
00373     if ( fStruct )
00374     {
00375         Abc_NtkForEachCo( p->pNtk, pNode, i )
00376             Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
00377                 Counter += Sim_SuppStrHasVar( p->vSuppStr, pNode, v );
00378     }
00379     else
00380     {
00381         Abc_NtkForEachCo( p->pNtk, pNode, i )
00382             Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
00383                 Counter += Sim_SuppFunHasVar( p->vSuppFun, i, v );
00384     }
00385     return Counter;
00386 }

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file simUtils.c.

00098 {
00099     int w;
00100     for ( w = 0; w < nWords; w++ )
00101         pInfo1[w] |= pInfo2[w];
00102 }

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

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

Synopsis [Allocates simulation information for all nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file simUtils.c.

00055 {
00056     Vec_Ptr_t * vInfo;
00057     int i;
00058     assert( nSize > 0 && nWords > 0 );
00059     vInfo = Vec_PtrAlloc( nSize );
00060     vInfo->pArray[0] = ALLOC( unsigned, nSize * nWords );
00061     if ( fClean )
00062         memset( vInfo->pArray[0], 0, sizeof(unsigned) * nSize * nWords );
00063     for ( i = 1; i < nSize; i++ )
00064         vInfo->pArray[i] = ((unsigned *)vInfo->pArray[i-1]) + nWords;
00065     vInfo->nSize = nSize;
00066     return vInfo;
00067 }

bool 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 182 of file simUtils.c.

00183 {
00184     unsigned * pSimInfo1, * pSimInfo2;
00185     int k;
00186     pSimInfo1 = p->vSim0->pArray[pNode->Id];
00187     pSimInfo2 = p->vSim1->pArray[pNode->Id];
00188     for ( k = 0; k < p->nSimWords; k++ )
00189         if ( pSimInfo2[k] != pSimInfo1[k] )
00190             return 0;
00191     return 1;
00192 }

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 115 of file simUtils.c.

00116 {
00117     int w, b;
00118     unsigned uMask;
00119     vDiffs->nSize = 0;
00120     for ( w = 0; w < nWords; w++ )
00121         if ( uMask = (pInfo2[w] ^ pInfo1[w]) )
00122             for ( b = 0; b < 32; b++ )
00123                 if ( uMask & (1 << b) )
00124                     Vec_IntPush( vDiffs, 32*w + b );
00125 }

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 138 of file simUtils.c.

00139 {
00140     int w, b;
00141     unsigned uMask;
00142     vDiffs->nSize = 0;
00143     for ( w = 0; w < nWords; w++ )
00144         if ( uMask = (pInfo2[w] & ~pInfo1[w]) )
00145             for ( b = 0; b < 32; b++ )
00146                 if ( uMask & (1 << b) )
00147                     Vec_IntPush( vDiffs, 32*w + b );
00148 }

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 161 of file simUtils.c.

00162 {
00163     unsigned * pSimInfo1, * pSimInfo2;
00164     int k;
00165     pSimInfo1 = p->vSim0->pArray[pNode->Id];
00166     pSimInfo2 = p->vSim1->pArray[pNode->Id];
00167     for ( k = 0; k < p->nSimWords; k++ )
00168         pSimInfo2[k] = ~pSimInfo1[k];
00169 }

void Sim_UtilInfoFree ( Vec_Ptr_t *  p  ) 

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

Synopsis [Allocates simulation information for all nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file simUtils.c.

00081 {
00082     free( p->pArray[0] );
00083     Vec_PtrFree( p );
00084 }

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 540 of file simUtils.c.

00541 {
00542     int k;
00543     for ( k = 0; k < nSimWords; k++ )
00544         if ( ~pPats1[k] & ~pPats2[k] )
00545             return 0;
00546     return 1;
00547 }

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

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

Synopsis [Returns 1 if equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 500 of file simUtils.c.

00501 {
00502     int k;
00503     for ( k = 0; k < nSimWords; k++ )
00504         if ( pPats1[k] != pPats2[k] )
00505             return 0;
00506     return 1;
00507 }

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

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

Synopsis [Returns 1 if Node1 implies Node2.]

Description []

SideEffects []

SeeAlso []

Definition at line 520 of file simUtils.c.

00521 {
00522     int k;
00523     for ( k = 0; k < nSimWords; k++ )
00524         if ( pPats1[k] & ~pPats2[k] )
00525             return 0;
00526     return 1;
00527 }

int Sim_UtilMatrsAreDisjoint ( Sym_Man_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 698 of file simUtils.c.

00699 {
00700     int i;
00701     for ( i = 0; i < p->nOutputs; i++ )
00702         if ( !Extra_BitMatrixIsDisjoint( Vec_PtrEntry(p->vMatrSymms,i), Vec_PtrEntry(p->vMatrNonSymms,i) ) )
00703             return 0;
00704     return 1;
00705 }

void Sim_UtilSetCompl ( unsigned *  pPatRand,
int  nSimWords 
)

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

Synopsis [Returns complemented patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 462 of file simUtils.c.

00463 {
00464     int k;
00465     for ( k = 0; k < nSimWords; k++ )
00466         pPatRand[k] = ~pPatRand[k];
00467 }

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

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

Synopsis [Returns constant patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file simUtils.c.

00481 {
00482     int k;
00483     for ( k = 0; k < nSimWords; k++ )
00484         pPatRand[k] = 0;
00485     if ( fConst1 )
00486         Sim_UtilSetCompl( pPatRand, nSimWords );
00487 }

void Sim_UtilSetRandom ( unsigned *  pPatRand,
int  nSimWords 
)

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

Synopsis [Returns random patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 444 of file simUtils.c.

00445 {
00446     int k;
00447     for ( k = 0; k < nSimWords; k++ )
00448         pPatRand[k] = SIM_RANDOM_UNSIGNED;
00449 }

void Sim_UtilSimulate ( Sim_Man_t *  p,
bool  fType 
)

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

Synopsis [Simulates the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file simUtils.c.

00206 {
00207     Abc_Obj_t * pNode;
00208     int i;
00209     // simulate the internal nodes
00210     Abc_NtkForEachNode( p->pNtk, pNode, i )
00211         Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
00212     // assign simulation info of the CO nodes
00213     Abc_NtkForEachCo( p->pNtk, pNode, i )
00214         Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
00215 }

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

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 228 of file simUtils.c.

00229 {
00230     unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
00231     int k, fComp1, fComp2;
00232     // simulate the internal nodes
00233     if ( Abc_ObjIsNode(pNode) )
00234     {
00235         if ( fType )
00236             pSimmNode  = p->vSim1->pArray[ pNode->Id ];
00237         else
00238             pSimmNode  = p->vSim0->pArray[ pNode->Id ];
00239 
00240         if ( fType1 )
00241             pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
00242         else
00243             pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];
00244 
00245         if ( fType2 )
00246             pSimmNode2 = p->vSim1->pArray[ Abc_ObjFaninId1(pNode) ];
00247         else
00248             pSimmNode2 = p->vSim0->pArray[ Abc_ObjFaninId1(pNode) ];
00249 
00250         fComp1 = Abc_ObjFaninC0(pNode);
00251         fComp2 = Abc_ObjFaninC1(pNode);
00252         if ( fComp1 && fComp2 )
00253             for ( k = 0; k < p->nSimWords; k++ )
00254                 pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
00255         else if ( fComp1 && !fComp2 )
00256             for ( k = 0; k < p->nSimWords; k++ )
00257                 pSimmNode[k] = ~pSimmNode1[k] &  pSimmNode2[k];
00258         else if ( !fComp1 && fComp2 )
00259             for ( k = 0; k < p->nSimWords; k++ )
00260                 pSimmNode[k] =  pSimmNode1[k] & ~pSimmNode2[k];
00261         else // if ( fComp1 && fComp2 )
00262             for ( k = 0; k < p->nSimWords; k++ )
00263                 pSimmNode[k] =  pSimmNode1[k] &  pSimmNode2[k];
00264     }
00265     else 
00266     {
00267         assert( Abc_ObjFaninNum(pNode) == 1 );
00268         if ( fType )
00269             pSimmNode  = p->vSim1->pArray[ pNode->Id ];
00270         else
00271             pSimmNode  = p->vSim0->pArray[ pNode->Id ];
00272 
00273         if ( fType1 )
00274             pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
00275         else
00276             pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];
00277 
00278         fComp1 = Abc_ObjFaninC0(pNode);
00279         if ( fComp1 )
00280             for ( k = 0; k < p->nSimWords; k++ )
00281                 pSimmNode[k] = ~pSimmNode1[k];
00282         else 
00283             for ( k = 0; k < p->nSimWords; k++ )
00284                 pSimmNode[k] =  pSimmNode1[k];
00285     }
00286 }

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 299 of file simUtils.c.

00300 {
00301     unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
00302     int k, fComp1, fComp2;
00303     // simulate the internal nodes
00304     assert( Abc_ObjIsNode(pNode) );
00305     pSimmNode  = Vec_PtrEntry(vSimInfo, pNode->Id);
00306     pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
00307     pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
00308     pSimmNode  += nOffset;
00309     pSimmNode1 += nOffset;
00310     pSimmNode2 += nOffset;
00311     fComp1 = Abc_ObjFaninC0(pNode);
00312     fComp2 = Abc_ObjFaninC1(pNode);
00313     if ( fComp1 && fComp2 )
00314         for ( k = 0; k < nSimWords; k++ )
00315             pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
00316     else if ( fComp1 && !fComp2 )
00317         for ( k = 0; k < nSimWords; k++ )
00318             pSimmNode[k] = ~pSimmNode1[k] &  pSimmNode2[k];
00319     else if ( !fComp1 && fComp2 )
00320         for ( k = 0; k < nSimWords; k++ )
00321             pSimmNode[k] =  pSimmNode1[k] & ~pSimmNode2[k];
00322     else // if ( fComp1 && fComp2 )
00323         for ( k = 0; k < nSimWords; k++ )
00324             pSimmNode[k] =  pSimmNode1[k] &  pSimmNode2[k];
00325 }

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 338 of file simUtils.c.

00339 {
00340     unsigned * pSimmNode, * pSimmNode1;
00341     int k, fComp1;
00342     // simulate the internal nodes
00343     assert( Abc_ObjIsCo(pNode) );
00344     pSimmNode  = Vec_PtrEntry(vSimInfo, pNode->Id);
00345     pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
00346     pSimmNode  += nOffset + (fShift > 0)*nSimWords;
00347     pSimmNode1 += nOffset;
00348     fComp1 = Abc_ObjFaninC0(pNode);
00349     if ( fComp1 )
00350         for ( k = 0; k < nSimWords; k++ )
00351             pSimmNode[k] = ~pSimmNode1[k];
00352     else 
00353         for ( k = 0; k < nSimWords; k++ )
00354             pSimmNode[k] =  pSimmNode1[k];
00355 }

void Sym_ManPrintStats ( Sym_Man_t *  p  ) 

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

Synopsis [Prints the manager statisticis.]

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file simMan.c.

00133 {
00134 //    printf( "Inputs = %5d. Outputs = %5d. Sim words = %5d.\n", 
00135 //        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
00136     printf( "Total symm         = %8d.\n", p->nPairsSymm );
00137     printf( "Structural symm    = %8d.\n", p->nPairsSymmStr );
00138     printf( "Total non-sym      = %8d.\n", p->nPairsNonSymm );
00139     printf( "Total var pairs    = %8d.\n", p->nPairsTotal );
00140     printf( "Sat runs SAT       = %8d.\n", p->nSatRunsSat );
00141     printf( "Sat runs UNSAT     = %8d.\n", p->nSatRunsUnsat );
00142     PRT( "Structural  ", p->timeStruct );
00143     PRT( "Simulation  ", p->timeSim );
00144     PRT( "Matrix      ", p->timeMatr );
00145     PRT( "Counting    ", p->timeCount );
00146     PRT( "Fraiging    ", p->timeFraig );
00147     PRT( "SAT         ", p->timeSat );
00148     PRT( "TOTAL       ", p->timeTotal );
00149 }

Sym_Man_t* Sym_ManStart ( Abc_Ntk_t *  pNtk,
int  fVerbose 
)

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

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

Synopsis [Starts the simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file simMan.c.

00044 {
00045     Sym_Man_t * p;
00046     int i, v; 
00047     // start the manager
00048     p = ALLOC( Sym_Man_t, 1 );
00049     memset( p, 0, sizeof(Sym_Man_t) );
00050     p->pNtk = pNtk;
00051     p->vNodes     = Abc_NtkDfs( pNtk, 0 );
00052     p->nInputs    = Abc_NtkCiNum(p->pNtk);
00053     p->nOutputs   = Abc_NtkCoNum(p->pNtk);
00054     // internal simulation information
00055     p->nSimWords  = SIM_NUM_WORDS(p->nInputs);
00056     p->vSim       = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
00057     // symmetry info for each output
00058     p->vMatrSymms    = Vec_PtrStart( p->nOutputs );
00059     p->vMatrNonSymms = Vec_PtrStart( p->nOutputs );
00060     p->vPairsTotal   = Vec_IntStart( p->nOutputs );
00061     p->vPairsSym     = Vec_IntStart( p->nOutputs );
00062     p->vPairsNonSym  = Vec_IntStart( p->nOutputs );
00063     for ( i = 0; i < p->nOutputs; i++ )
00064     {
00065         p->vMatrSymms->pArray[i]    = Extra_BitMatrixStart( p->nInputs );
00066         p->vMatrNonSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs );
00067     }
00068     // temporary patterns
00069     p->uPatRand = ALLOC( unsigned, p->nSimWords );
00070     p->uPatCol  = ALLOC( unsigned, p->nSimWords );
00071     p->uPatRow  = ALLOC( unsigned, p->nSimWords );
00072     p->vVarsU   = Vec_IntStart( 100 );
00073     p->vVarsV   = Vec_IntStart( 100 );
00074     // compute supports
00075     p->vSuppFun  = Sim_ComputeFunSupp( pNtk, fVerbose );
00076     p->vSupports = Vec_VecStart( p->nOutputs );
00077     for ( i = 0; i < p->nOutputs; i++ )
00078         for ( v = 0; v < p->nInputs; v++ )
00079             if ( Sim_SuppFunHasVar( p->vSuppFun, i, v ) )
00080                 Vec_VecPush( p->vSupports, i, (void *)v );
00081     return p;
00082 }

void Sym_ManStop ( Sym_Man_t *  p  ) 

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

Synopsis [Stops the simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file simMan.c.

00096 {
00097     int i;
00098     Sym_ManPrintStats( p );
00099     if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );   
00100     if ( p->vSim )         Sim_UtilInfoFree( p->vSim );   
00101     if ( p->vNodes )       Vec_PtrFree( p->vNodes );
00102     if ( p->vSupports )    Vec_VecFree( p->vSupports );
00103     for ( i = 0; i < p->nOutputs; i++ )
00104     {
00105         Extra_BitMatrixStop( p->vMatrSymms->pArray[i] );
00106         Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] );
00107     }
00108     Vec_IntFree( p->vVarsU );
00109     Vec_IntFree( p->vVarsV );
00110     Vec_PtrFree( p->vMatrSymms );
00111     Vec_PtrFree( p->vMatrNonSymms );
00112     Vec_IntFree( p->vPairsTotal );
00113     Vec_IntFree( p->vPairsSym );
00114     Vec_IntFree( p->vPairsNonSym );
00115     FREE( p->uPatRand );
00116     FREE( p->uPatCol );
00117     FREE( p->uPatRow );
00118     free( p );
00119 }

Generated on Tue Jan 5 12:19:35 2010 for abc70930 by  doxygen 1.6.1