00001
00021 #include "abc.h"
00022 #include "sim.h"
00023
00027
00031
00043 Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
00044 {
00045 Sym_Man_t * p;
00046 int i, v;
00047
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
00055 p->nSimWords = SIM_NUM_WORDS(p->nInputs);
00056 p->vSim = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
00057
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
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
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 }
00083
00095 void Sym_ManStop( Sym_Man_t * p )
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 }
00120
00132 void Sym_ManPrintStats( Sym_Man_t * p )
00133 {
00134
00135
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 }
00150
00151
00163 Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight )
00164 {
00165 Sim_Man_t * p;
00166
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
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
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
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
00189 p->vSuppTargs = Vec_VecStart( p->nInputs );
00190 }
00191 return p;
00192 }
00193
00205 void Sim_ManStop( Sim_Man_t * p )
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
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 }
00218
00230 void Sim_ManPrintStats( Sim_Man_t * p )
00231 {
00232
00233
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 }
00244
00245
00246
00258 Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p )
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 }
00267
00279 void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat )
00280 {
00281 Extra_MmFixedEntryRecycle( p->pMmPat, (char *)pPat );
00282 }
00283
00287
00288