From 942600414dba2e32bf2529517e17eaee5991d29c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 24 Aug 2012 11:12:51 -0700 Subject: Added simulation of comb circuits with user-specified patterns in command 'sim'. --- src/proof/fra/fra.h | 3 +- src/proof/fra/fraClass.c | 2 +- src/proof/fra/fraClaus.c | 6 +- src/proof/fra/fraImp.c | 6 +- src/proof/fra/fraSim.c | 153 ++++++++++++++++++++++++++++++++++++++++++++++- 5 files changed, 159 insertions(+), 11 deletions(-) (limited to 'src/proof/fra') diff --git a/src/proof/fra/fra.h b/src/proof/fra/fra.h index 1690b463..b1fdb539 100644 --- a/src/proof/fra/fra.h +++ b/src/proof/fra/fra.h @@ -371,8 +371,9 @@ extern void Fra_SmlSimulate( Fra_Man_t * p, int fInit ); extern void Fra_SmlResimulate( Fra_Man_t * p ); extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ); extern void Fra_SmlStop( Fra_Sml_t * p ); +extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter ); +extern Fra_Sml_t * Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose ); extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords, int fCheckMiter ); -extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); extern Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); extern Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); diff --git a/src/proof/fra/fraClass.c b/src/proof/fra/fraClass.c index cef2f673..47a9e7a0 100644 --- a/src/proof/fra/fraClass.c +++ b/src/proof/fra/fraClass.c @@ -645,7 +645,7 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) Aig_Obj_t * pObj, * pRepr, ** ppClass; int * pWeights, WeightMax = 0, i, k, c; // perform combinational simulation - pComb = Fra_SmlSimulateComb( p->pAig, 32 ); + pComb = Fra_SmlSimulateComb( p->pAig, 32, 0 ); // compute the weight of each node in the classes pWeights = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) ); memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) ); diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c index 95ab0c99..c4f50559 100644 --- a/src/proof/fra/fraClaus.c +++ b/src/proof/fra/fraClaus.c @@ -668,7 +668,7 @@ ABC_PRT( "Infoseq", clock() - clk ); clk = clock(); // srand( 0xAABBAABB ); Aig_ManRandom(1); - pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref ); + pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 ); if ( p->fVerbose ) { ABC_PRT( "Sim-cmb", clock() - clk ); @@ -753,7 +753,7 @@ if ( p->fVerbose ) clk = clock(); // srand( 0xAABBAABB ); Aig_ManRandom(1); - pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref ); + pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 ); if ( p->fVerbose ) { //ABC_PRT( "Sim-cmb", clock() - clk ); @@ -1628,7 +1628,7 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p ) // simulate the circuit with nCombSimWords * 32 = 64K patterns // srand( 0xAABBAABB ); Aig_ManRandom(1); - pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords ); + pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords, 0 ); // create mapping from SAT vars to node IDs pVar2Id = ABC_ALLOC( int, p->pCnf->nVars ); memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars ); diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c index 4d33717a..809ad8e4 100644 --- a/src/proof/fra/fraImp.c +++ b/src/proof/fra/fraImp.c @@ -332,8 +332,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) ); assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); // normalize both managers - pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); - pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 ); + pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 ); + pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 ); // get the nodes sorted by the number of 1s vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr ); // count the total number of implications @@ -635,7 +635,7 @@ double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p ) if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) return Ratio; // simulate the AIG manager with combinational patterns - pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); + pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 ); // go through the implications and collect where they do not hold pResult = Fra_ObjSim( pComb, 0 ); assert( pResult[0] == 0 ); diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c index 76e0a132..b85107d7 100644 --- a/src/proof/fra/fraSim.c +++ b/src/proof/fra/fraSim.c @@ -380,7 +380,7 @@ void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFram { unsigned * pSims; int i; - assert( Aig_ObjIsCi(pObj) ); + assert( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) ); pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; for ( i = 0; i < p->nWordsFrame; i++ ) pSims[i] = fConst1? ~(unsigned)0 : 0; @@ -590,6 +590,7 @@ void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) fCompl = pObj->fPhase; fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); // copy information as it is +// if ( Aig_ObjFaninC0(pObj) ) if ( fCompl0 ) for ( i = 0; i < p->nWordsFrame; i++ ) pSims[i] = ~pSims0[i]; @@ -820,6 +821,7 @@ Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFr p->nWordsFrame = nWordsFrame; p->nWordsTotal = (nPref + nFrames) * nWordsFrame; p->nWordsPref = nPref * nWordsFrame; + // constant 1 is initialized to 0 because we store values modulus phase (pObj->fPhase) return p; } @@ -851,12 +853,157 @@ void Fra_SmlStop( Fra_Sml_t * p ) SeeAlso [] ***********************************************************************/ -Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ) +Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords, int fCheckMiter ) { Fra_Sml_t * p; p = Fra_SmlStart( pAig, 0, 1, nWords ); Fra_SmlInitialize( p, 0 ); Fra_SmlSimulateOne( p ); + if ( fCheckMiter ) + p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Reads simulation patterns from file.] + + Description [Each pattern contains the given number (nInputs) of binary digits. + No other symbols (except spaces and line endings) are allowed in the file.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Fra_SmlSimulateReadFile( char * pFileName ) +{ + Vec_Str_t * vRes; + FILE * pFile; + int c; + pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" with simulation patterns.\n", pFileName ); + return NULL; + } + vRes = Vec_StrAlloc( 1000 ); + while ( (c = fgetc(pFile)) != EOF ) + { + if ( c == '0' || c == '1' ) + Vec_StrPush( vRes, (char)(c - '0') ); + else if ( c != ' ' && c != '\r' && c != '\n' && c != '\t' ) + { + printf( "File \"%s\" contains symbol (%c) other than \'0\' or \'1\'.\n", c ); + Vec_StrFreeP( &vRes ); + break; + } + } + fclose( pFile ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Assigns simulation patters derived from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_SmlInitializeGiven( Fra_Sml_t * p, Vec_Str_t * vSimInfo ) +{ + Aig_Obj_t * pObj; + unsigned * pSims; + int i, k, nPats = Vec_StrSize(vSimInfo) / Aig_ManCiNum(p->pAig); + int nPatsPadded = p->nWordsTotal * 32; + assert( Aig_ManRegNum(p->pAig) == 0 ); + assert( Vec_StrSize(vSimInfo) % Aig_ManCiNum(p->pAig) == 0 ); + assert( nPats <= nPatsPadded ); + Aig_ManForEachCi( p->pAig, pObj, i ) + { + pSims = Fra_ObjSim( p, pObj->Id ); + // clean data + for ( k = 0; k < p->nWordsTotal; k++ ) + pSims[k] = 0; + // load patterns + for ( k = 0; k < nPats; k++ ) + if ( Vec_StrEntry(vSimInfo, k * Aig_ManCiNum(p->pAig) + i) ) + Abc_InfoSetBit( pSims, k ); + // pad the remaining bits with the value of the last pattern + for ( ; k < nPatsPadded; k++ ) + if ( Vec_StrEntry(vSimInfo, (nPats-1) * Aig_ManCiNum(p->pAig) + i) ) + Abc_InfoSetBit( pSims, k ); + } +} + +/**Function************************************************************* + + Synopsis [Prints output values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_SmlPrintOutputs( Fra_Sml_t * p, int nPatterns ) +{ + Aig_Obj_t * pObj; + unsigned * pSims; + int i, k; + for ( k = 0; k < nPatterns; k++ ) + { + Aig_ManForEachCo( p->pAig, pObj, i ) + { + pSims = Fra_ObjSim( p, pObj->Id ); + printf( "%d", Abc_InfoHasBit( pSims, k ) ); + } + printf( "\n" ); ; + } +} + +/**Function************************************************************* + + Synopsis [Assigns simulation patters derived from file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fra_Sml_t * Fra_SmlSimulateCombGiven( Aig_Man_t * pAig, char * pFileName, int fCheckMiter, int fVerbose ) +{ + Vec_Str_t * vSimInfo; + Fra_Sml_t * p; + int nPatterns; + assert( Aig_ManRegNum(pAig) == 0 ); + // read comb patterns from file + vSimInfo = Fra_SmlSimulateReadFile( pFileName ); + if ( vSimInfo == NULL ) + return NULL; + if ( Vec_StrSize(vSimInfo) % Aig_ManCiNum(pAig) != 0 ) + { + printf( "File \"%s\": The number of binary digits (%d) is not divisible by the number of primary inputs (%d).\n", + pFileName, Vec_StrSize(vSimInfo), Aig_ManCiNum(pAig) ); + Vec_StrFree( vSimInfo ); + return NULL; + } + p = Fra_SmlStart( pAig, 0, 1, Abc_BitWordNum(Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig)) ); + Fra_SmlInitializeGiven( p, vSimInfo ); + nPatterns = Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig); + Vec_StrFree( vSimInfo ); + Fra_SmlSimulateOne( p ); + if ( fCheckMiter ) + p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p ); + if ( fVerbose ) + Fra_SmlPrintOutputs( p, nPatterns ); return p; } @@ -878,7 +1025,7 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW Fra_SmlInitialize( p, 1 ); Fra_SmlSimulateOne( p ); if ( fCheckMiter ) - p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p ); + p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p ); return p; } -- cgit v1.2.3