abc70930: src/aig/fra/fraSim.c Source File

00001 
00021 #include "fra.h"
00022 
00026 
00030 
00042 int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize )
00043 {
00044     Fra_Man_t * p = pObj->pData;
00045     static int s_FPrimes[128] = { 
00046         1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
00047         1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
00048         2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
00049         2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
00050         3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
00051         3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
00052         4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
00053         4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
00054         5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
00055         6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
00056         6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
00057         7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
00058         8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
00059     };
00060     unsigned * pSims;
00061     unsigned uHash;
00062     int i;
00063 //    assert( p->pSml->nWordsTotal <= 128 );
00064     uHash = 0;
00065     pSims = Fra_ObjSim(p->pSml, pObj->Id);
00066     for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
00067         uHash ^= pSims[i] * s_FPrimes[i & 0x7F];
00068     return uHash % nTableSize;
00069 }
00070 
00082 int Fra_SmlNodeIsConst( Aig_Obj_t * pObj )
00083 {
00084     Fra_Man_t * p = pObj->pData;
00085     unsigned * pSims;
00086     int i;
00087     pSims = Fra_ObjSim(p->pSml, pObj->Id);
00088     for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
00089         if ( pSims[i] )
00090             return 0;
00091     return 1;
00092 }
00093 
00105 int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
00106 {
00107     Fra_Man_t * p = pObj0->pData;
00108     unsigned * pSims0, * pSims1;
00109     int i;
00110     pSims0 = Fra_ObjSim(p->pSml, pObj0->Id);
00111     pSims1 = Fra_ObjSim(p->pSml, pObj1->Id);
00112     for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
00113         if ( pSims0[i] != pSims1[i] )
00114             return 0;
00115     return 1;
00116 }
00117 
00129 int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
00130 {
00131     unsigned * pSimL, * pSimR;
00132     int k, Counter = 0;
00133     pSimL = Fra_ObjSim( p, Left );
00134     pSimR = Fra_ObjSim( p, Right );
00135     for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
00136         Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
00137     return Counter;
00138 }
00139 
00151 int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj )
00152 {
00153     unsigned * pSims;
00154     int i;
00155     pSims = Fra_ObjSim(p, pObj->Id);
00156     for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
00157         if ( pSims[i] )
00158             return 0;
00159     return 1;
00160 }
00161 
00162 
00163 
00175 void Fra_SmlSavePattern0( Fra_Man_t * p, int fInit )
00176 {
00177     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
00178 }
00179 
00191 void Fra_SmlSavePattern1( Fra_Man_t * p, int fInit )
00192 {
00193     Aig_Obj_t * pObj;
00194     int i, k, nTruePis;
00195     memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
00196     if ( !fInit )
00197         return;
00198     // clear the state bits to correspond to all-0 initial state
00199     nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
00200     k = 0;
00201     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
00202         Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
00203 }
00204 
00216 void Fra_SmlSavePattern( Fra_Man_t * p )
00217 {
00218     Aig_Obj_t * pObj;
00219     int i;
00220     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
00221     Aig_ManForEachPi( p->pManFraig, pObj, i )
00222         if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
00223             Aig_InfoSetBit( p->pPatWords, i );
00224 
00225     if ( p->vCex )
00226     {
00227         Vec_IntClear( p->vCex );
00228         for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
00229             Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
00230         for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
00231             Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
00232     }
00233 
00234 /*
00235     printf( "Pattern: " );
00236     Aig_ManForEachPi( p->pManFraig, pObj, i )
00237         printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
00238     printf( "\n" );
00239 */
00240 }
00241 
00242 
00243 
00255 void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
00256 { 
00257     unsigned * pSims;
00258     int i, k, BestPat, * pModel;
00259     // find the word of the pattern
00260     pSims = Fra_ObjSim(p->pSml, pObj->Id);
00261     for ( i = 0; i < p->pSml->nWordsTotal; i++ )
00262         if ( pSims[i] )
00263             break;
00264     assert( i < p->pSml->nWordsTotal );
00265     // find the bit of the pattern
00266     for ( k = 0; k < 32; k++ )
00267         if ( pSims[i] & (1 << k) )
00268             break;
00269     assert( k < 32 );
00270     // determine the best pattern
00271     BestPat = i * 32 + k;
00272     // fill in the counter-example data
00273     pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
00274     Aig_ManForEachPi( p->pManAig, pObj, i )
00275     {
00276         pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObj->Id), BestPat);
00277 //        printf( "%d", pModel[i] );
00278     }
00279 //    printf( "\n" );
00280     // set the model
00281     assert( p->pManFraig->pData == NULL );
00282     p->pManFraig->pData = pModel;
00283     return;
00284 }
00285 
00297 int Fra_SmlCheckOutput( Fra_Man_t * p )
00298 {
00299     Aig_Obj_t * pObj;
00300     int i;
00301     // make sure the reference simulation pattern does not detect the bug
00302     pObj = Aig_ManPo( p->pManAig, 0 );
00303     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
00304     Aig_ManForEachPo( p->pManAig, pObj, i )
00305     {
00306         if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
00307         {
00308             // create the counter-example from this pattern
00309             Fra_SmlCheckOutputSavePattern( p, Aig_ObjFanin0(pObj) );
00310             return 1;
00311         }
00312     }
00313     return 0;
00314 }
00315 
00316 
00317 
00329 void Fra_SmlAssignRandom( Fra_Sml_t * p, Aig_Obj_t * pObj )
00330 {
00331     unsigned * pSims;
00332     int i;
00333     assert( Aig_ObjIsPi(pObj) );
00334     pSims = Fra_ObjSim( p, pObj->Id );
00335     for ( i = 0; i < p->nWordsTotal; i++ )
00336         pSims[i] = Fra_ObjRandomSim();
00337 }
00338 
00350 void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
00351 {
00352     unsigned * pSims;
00353     int i;
00354     assert( Aig_ObjIsPi(pObj) );
00355     pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
00356     for ( i = 0; i < p->nWordsFrame; i++ )
00357         pSims[i] = fConst1? ~(unsigned)0 : 0;
00358 }
00359 
00371 void Fra_SmlInitialize( Fra_Sml_t * p, int fInit )
00372 {
00373     Aig_Obj_t * pObj;
00374     int i;
00375     if ( fInit )
00376     {
00377         assert( Aig_ManRegNum(p->pAig) > 0 );
00378         assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
00379         // assign random info for primary inputs
00380         Aig_ManForEachPiSeq( p->pAig, pObj, i )
00381             Fra_SmlAssignRandom( p, pObj );
00382         // assign the initial state for the latches
00383         Aig_ManForEachLoSeq( p->pAig, pObj, i )
00384             Fra_SmlAssignConst( p, pObj, 0, 0 );
00385     }
00386     else
00387     {
00388         Aig_ManForEachPi( p->pAig, pObj, i )
00389             Fra_SmlAssignRandom( p, pObj );
00390     }
00391 }
00392 
00404 void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
00405 {
00406     Aig_Obj_t * pObj;
00407     int f, i, k, Limit, nTruePis;
00408     assert( p->nFrames > 0 );
00409     if ( p->nFrames == 1 )
00410     {
00411         // copy the PI info 
00412         Aig_ManForEachPi( p->pAig, pObj, i )
00413             Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
00414         // flip one bit
00415         Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
00416         for ( i = 0; i < Limit; i++ )
00417             Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
00418     }
00419     else
00420     {
00421         int fUseDist1 = 0;
00422 
00423         // copy the PI info for each frame
00424         nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
00425         for ( f = 0; f < p->nFrames; f++ )
00426             Aig_ManForEachPiSeq( p->pAig, pObj, i )
00427                 Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
00428         // copy the latch info 
00429         k = 0;
00430         Aig_ManForEachLoSeq( p->pAig, pObj, i )
00431             Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
00432 //        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
00433 
00434         // flip one bit of the last frame
00435         if ( fUseDist1 ) //&& p->nFrames == 2 )
00436         {
00437             Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
00438             for ( i = 0; i < Limit; i++ )
00439                 Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
00440         }
00441     }
00442 }
00443 
00444 
00456 void Fra_SmlNodeSimulate( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
00457 {
00458     unsigned * pSims, * pSims0, * pSims1;
00459     int fCompl, fCompl0, fCompl1, i;
00460     assert( !Aig_IsComplement(pObj) );
00461     assert( Aig_ObjIsNode(pObj) );
00462     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
00463     // get hold of the simulation information
00464     pSims  = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
00465     pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
00466     pSims1 = Fra_ObjSim(p, Aig_ObjFanin1(pObj)->Id) + p->nWordsFrame * iFrame;
00467     // get complemented attributes of the children using their random info
00468     fCompl  = pObj->fPhase;
00469     fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
00470     fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
00471     // simulate
00472     if ( fCompl0 && fCompl1 )
00473     {
00474         if ( fCompl )
00475             for ( i = 0; i < p->nWordsFrame; i++ )
00476                 pSims[i] = (pSims0[i] | pSims1[i]);
00477         else
00478             for ( i = 0; i < p->nWordsFrame; i++ )
00479                 pSims[i] = ~(pSims0[i] | pSims1[i]);
00480     }
00481     else if ( fCompl0 && !fCompl1 )
00482     {
00483         if ( fCompl )
00484             for ( i = 0; i < p->nWordsFrame; i++ )
00485                 pSims[i] = (pSims0[i] | ~pSims1[i]);
00486         else
00487             for ( i = 0; i < p->nWordsFrame; i++ )
00488                 pSims[i] = (~pSims0[i] & pSims1[i]);
00489     }
00490     else if ( !fCompl0 && fCompl1 )
00491     {
00492         if ( fCompl )
00493             for ( i = 0; i < p->nWordsFrame; i++ )
00494                 pSims[i] = (~pSims0[i] | pSims1[i]);
00495         else
00496             for ( i = 0; i < p->nWordsFrame; i++ )
00497                 pSims[i] = (pSims0[i] & ~pSims1[i]);
00498     }
00499     else // if ( !fCompl0 && !fCompl1 )
00500     {
00501         if ( fCompl )
00502             for ( i = 0; i < p->nWordsFrame; i++ )
00503                 pSims[i] = ~(pSims0[i] & pSims1[i]);
00504         else
00505             for ( i = 0; i < p->nWordsFrame; i++ )
00506                 pSims[i] = (pSims0[i] & pSims1[i]);
00507     }
00508 }
00509 
00521 void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
00522 {
00523     unsigned * pSims, * pSims0;
00524     int fCompl, fCompl0, i;
00525     assert( !Aig_IsComplement(pObj) );
00526     assert( Aig_ObjIsPo(pObj) );
00527     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
00528     // get hold of the simulation information
00529     pSims  = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
00530     pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
00531     // get complemented attributes of the children using their random info
00532     fCompl  = pObj->fPhase;
00533     fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
00534     // copy information as it is
00535     if ( fCompl0 )
00536         for ( i = 0; i < p->nWordsFrame; i++ )
00537             pSims[i] = ~pSims0[i];
00538     else
00539         for ( i = 0; i < p->nWordsFrame; i++ )
00540             pSims[i] = pSims0[i];
00541 }
00542 
00554 void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
00555 {
00556     unsigned * pSims0, * pSims1;
00557     int i;
00558     assert( !Aig_IsComplement(pOut) );
00559     assert( !Aig_IsComplement(pIn) );
00560     assert( Aig_ObjIsPo(pOut) );
00561     assert( Aig_ObjIsPi(pIn) );
00562     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
00563     // get hold of the simulation information
00564     pSims0 = Fra_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
00565     pSims1 = Fra_ObjSim(p, pIn->Id) + p->nWordsFrame * (iFrame+1);
00566     // copy information as it is
00567     for ( i = 0; i < p->nWordsFrame; i++ )
00568         pSims1[i] = pSims0[i];
00569 }
00570 
00571 
00583 int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p )
00584 {
00585     Aig_Obj_t * pObj;
00586     int i;
00587     Aig_ManForEachPoSeq( p->pAig, pObj, i )
00588         if ( !Fra_SmlNodeIsZero(p, pObj) )
00589             return 1;
00590     return 0;
00591 }
00592 
00604 void Fra_SmlSimulateOne( Fra_Sml_t * p )
00605 {
00606     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
00607     int f, i, clk;
00608 clk = clock();
00609     for ( f = 0; f < p->nFrames; f++ )
00610     {
00611         // simulate the nodes
00612         Aig_ManForEachNode( p->pAig, pObj, i )
00613             Fra_SmlNodeSimulate( p, pObj, f );
00614         // copy simulation info into outputs
00615         Aig_ManForEachPoSeq( p->pAig, pObj, i )
00616             Fra_SmlNodeCopyFanin( p, pObj, f );
00617         // quit if this is the last timeframe
00618         if ( f == p->nFrames - 1 )
00619             break;
00620         // copy simulation info into outputs
00621         Aig_ManForEachLiSeq( p->pAig, pObj, i )
00622             Fra_SmlNodeCopyFanin( p, pObj, f );
00623         // copy simulation info into the inputs
00624         Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
00625             Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
00626     }
00627 p->timeSim += clock() - clk;
00628 p->nSimRounds++;
00629 }
00630 
00631 
00643 void Fra_SmlResimulate( Fra_Man_t * p )
00644 {
00645     int nChanges, clk;
00646     Fra_SmlAssignDist1( p->pSml, p->pPatWords );
00647     Fra_SmlSimulateOne( p->pSml );
00648 //    if ( p->pPars->fPatScores )
00649 //        Fra_CleanPatScores( p );
00650     if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
00651         return;
00652 clk = clock();
00653     nChanges = Fra_ClassesRefine( p->pCla );
00654     nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
00655     if ( p->pCla->vImps )
00656         nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
00657 p->timeRef += clock() - clk;
00658     if ( !p->pPars->nFramesK && nChanges < 1 )
00659         printf( "Error: A counter-example did not refine classes!\n" );
00660 //    assert( nChanges >= 1 );
00661 //printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
00662 }
00663 
00675 void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
00676 {
00677     int fVerbose = 0;
00678     int nChanges, nClasses, clk;
00679     assert( !fInit || Aig_ManRegNum(p->pManAig) );
00680     // start the classes
00681     Fra_SmlInitialize( p->pSml, fInit );
00682     Fra_SmlSimulateOne( p->pSml );
00683     Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
00684 //    Fra_ClassesPrint( p->pCla, 0 );
00685 if ( fVerbose )
00686 printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
00687 
00688 //return;
00689 
00690     // refine classes by walking 0/1 patterns
00691     Fra_SmlSavePattern0( p, fInit );
00692     Fra_SmlAssignDist1( p->pSml, p->pPatWords );
00693     Fra_SmlSimulateOne( p->pSml );
00694     if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
00695         return;
00696 clk = clock();
00697     nChanges = Fra_ClassesRefine( p->pCla );
00698     nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
00699 p->timeRef += clock() - clk;
00700 if ( fVerbose )
00701 printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
00702     Fra_SmlSavePattern1( p, fInit );
00703     Fra_SmlAssignDist1( p->pSml, p->pPatWords );
00704     Fra_SmlSimulateOne( p->pSml );
00705     if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
00706         return;
00707 clk = clock();
00708     nChanges = Fra_ClassesRefine( p->pCla );
00709     nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
00710 p->timeRef += clock() - clk;
00711 
00712 if ( fVerbose )
00713 printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
00714     // refine classes by random simulation
00715     do {
00716         Fra_SmlInitialize( p->pSml, fInit );
00717         Fra_SmlSimulateOne( p->pSml );
00718         nClasses = Vec_PtrSize(p->pCla->vClasses);
00719         if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
00720             return;
00721 clk = clock();
00722         nChanges = Fra_ClassesRefine( p->pCla );
00723         nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
00724 p->timeRef += clock() - clk;
00725 if ( fVerbose )
00726 printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
00727     } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
00728 
00729 //    if ( p->pPars->fVerbose )
00730 //    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
00731 //        Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
00732 //    Fra_ClassesPrint( p->pCla, 0 );
00733 }
00734  
00735 
00747 Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
00748 {
00749     Fra_Sml_t * p;
00750     p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
00751     memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
00752     p->pAig        = pAig;
00753     p->nPref       = nPref;
00754     p->nFrames     = nPref + nFrames;
00755     p->nWordsFrame = nWordsFrame;
00756     p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
00757     p->nWordsPref  = nPref * nWordsFrame;
00758     return p;
00759 }
00760 
00772 void Fra_SmlStop( Fra_Sml_t * p )
00773 {
00774     free( p );
00775 }
00776 
00777 
00789 Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
00790 {
00791     Fra_Sml_t * p;
00792     p = Fra_SmlStart( pAig, 0, 1, nWords );
00793     Fra_SmlInitialize( p, 0 );
00794     Fra_SmlSimulateOne( p );
00795     return p;
00796 }
00797 
00809 Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords )
00810 {
00811     Fra_Sml_t * p;
00812     p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
00813     Fra_SmlInitialize( p, 1 );
00814     Fra_SmlSimulateOne( p );
00815     p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
00816     return p;
00817 }
00818 
00822 
00823