src/aig/fra/fraSim.c File Reference

#include "fra.h"
Include dependency graph for fraSim.c:

Go to the source code of this file.

Functions

int Fra_SmlNodeHash (Aig_Obj_t *pObj, int nTableSize)
int Fra_SmlNodeIsConst (Aig_Obj_t *pObj)
int Fra_SmlNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
int Fra_SmlNodeNotEquWeight (Fra_Sml_t *p, int Left, int Right)
int Fra_SmlNodeIsZero (Fra_Sml_t *p, Aig_Obj_t *pObj)
void Fra_SmlSavePattern0 (Fra_Man_t *p, int fInit)
void Fra_SmlSavePattern1 (Fra_Man_t *p, int fInit)
void Fra_SmlSavePattern (Fra_Man_t *p)
void Fra_SmlCheckOutputSavePattern (Fra_Man_t *p, Aig_Obj_t *pObj)
int Fra_SmlCheckOutput (Fra_Man_t *p)
void Fra_SmlAssignRandom (Fra_Sml_t *p, Aig_Obj_t *pObj)
void Fra_SmlAssignConst (Fra_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
void Fra_SmlInitialize (Fra_Sml_t *p, int fInit)
void Fra_SmlAssignDist1 (Fra_Sml_t *p, unsigned *pPat)
void Fra_SmlNodeSimulate (Fra_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
void Fra_SmlNodeCopyFanin (Fra_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
void Fra_SmlNodeTransferNext (Fra_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
int Fra_SmlCheckNonConstOutputs (Fra_Sml_t *p)
void Fra_SmlSimulateOne (Fra_Sml_t *p)
void Fra_SmlResimulate (Fra_Man_t *p)
void Fra_SmlSimulate (Fra_Man_t *p, int fInit)
Fra_Sml_t * Fra_SmlStart (Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
void Fra_SmlStop (Fra_Sml_t *p)
Fra_Sml_t * Fra_SmlSimulateComb (Aig_Man_t *pAig, int nWords)
Fra_Sml_t * Fra_SmlSimulateSeq (Aig_Man_t *pAig, int nPref, int nFrames, int nWords)

Function Documentation

void Fra_SmlAssignConst ( Fra_Sml_t *  p,
Aig_Obj_t *  pObj,
int  fConst1,
int  iFrame 
)

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file fraSim.c.

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 }

void Fra_SmlAssignDist1 ( Fra_Sml_t *  p,
unsigned *  pPat 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 404 of file fraSim.c.

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 }

void Fra_SmlAssignRandom ( Fra_Sml_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Assigns random patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 329 of file fraSim.c.

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 }

int Fra_SmlCheckNonConstOutputs ( Fra_Sml_t *  p  ) 

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

Synopsis [Check if any of the POs becomes non-constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 583 of file fraSim.c.

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 }

int Fra_SmlCheckOutput ( Fra_Man_t *  p  ) 

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

Synopsis [Returns 1 if the one of the output is already non-constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 297 of file fraSim.c.

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 }

void Fra_SmlCheckOutputSavePattern ( Fra_Man_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Creates the counter-example from the successful pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file fraSim.c.

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 }

void Fra_SmlInitialize ( Fra_Sml_t *  p,
int  fInit 
)

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

Synopsis [Assings random simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 371 of file fraSim.c.

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 }

void Fra_SmlNodeCopyFanin ( Fra_Sml_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 521 of file fraSim.c.

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 }

int Fra_SmlNodeHash ( Aig_Obj_t *  pObj,
int  nTableSize 
)

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

FileName [fraSim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id
fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file fraSim.c.

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 }

int Fra_SmlNodeIsConst ( Aig_Obj_t *  pObj  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file fraSim.c.

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 }

int Fra_SmlNodeIsZero ( Fra_Sml_t *  p,
Aig_Obj_t *  pObj 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file fraSim.c.

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 }

int Fra_SmlNodeNotEquWeight ( Fra_Sml_t *  p,
int  Left,
int  Right 
)

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

Synopsis [Counts the number of 1s in the XOR of simulation data.]

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file fraSim.c.

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 }

int Fra_SmlNodesAreEqual ( Aig_Obj_t *  pObj0,
Aig_Obj_t *  pObj1 
)

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file fraSim.c.

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 }

void Fra_SmlNodeSimulate ( Fra_Sml_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 456 of file fraSim.c.

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 }

void Fra_SmlNodeTransferNext ( Fra_Sml_t *  p,
Aig_Obj_t *  pOut,
Aig_Obj_t *  pIn,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 554 of file fraSim.c.

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 }

void Fra_SmlResimulate ( Fra_Man_t *  p  ) 

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

Synopsis [Resimulates fraiging manager after finding a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 643 of file fraSim.c.

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 }

void Fra_SmlSavePattern ( Fra_Man_t *  p  ) 

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file fraSim.c.

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 }

void Fra_SmlSavePattern0 ( Fra_Man_t *  p,
int  fInit 
)

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

Synopsis [Generated const 0 pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file fraSim.c.

00176 {
00177     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
00178 }

void Fra_SmlSavePattern1 ( Fra_Man_t *  p,
int  fInit 
)

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

Synopsis [[Generated const 1 pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file fraSim.c.

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 }

void Fra_SmlSimulate ( Fra_Man_t *  p,
int  fInit 
)

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

Synopsis [Performs simulation of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 675 of file fraSim.c.

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 }

Fra_Sml_t* Fra_SmlSimulateComb ( Aig_Man_t *  pAig,
int  nWords 
)

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

Synopsis [Performs simulation of the uninitialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 789 of file fraSim.c.

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 }

void Fra_SmlSimulateOne ( Fra_Sml_t *  p  ) 

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

Synopsis [Simulates AIG manager.]

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

SideEffects []

SeeAlso []

Definition at line 604 of file fraSim.c.

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 }

Fra_Sml_t* Fra_SmlSimulateSeq ( Aig_Man_t *  pAig,
int  nPref,
int  nFrames,
int  nWords 
)

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

Synopsis [Performs simulation of the initialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 809 of file fraSim.c.

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 }

Fra_Sml_t* Fra_SmlStart ( Aig_Man_t *  pAig,
int  nPref,
int  nFrames,
int  nWordsFrame 
)

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 747 of file fraSim.c.

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 }

void Fra_SmlStop ( Fra_Sml_t *  p  ) 

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

Synopsis [Deallocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 772 of file fraSim.c.

00773 {
00774     free( p );
00775 }

Generated on Tue Jan 5 12:18:20 2010 for abc70930 by  doxygen 1.6.1