From 75d6d6abd1ccbfeb2ac6e156a015d9888a5727e7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 12 Sep 2008 08:01:00 -0700 Subject: Version abc80912 --- src/aig/fra/fraSec.c | 15 +- src/aig/saig/saig.h | 1 + src/aig/saig/saigMiter.c | 35 +++ src/aig/saig/saigSynch.c | 623 +++++++++++++++++++++++++++++++++++++++++++++ src/aig/ssw/sswCore.c | 5 +- src/aig/ssw/sswMan.c | 10 +- src/aig/ssw/sswSimSat.c | 21 +- src/aig/ssw/sswSweep.c | 8 +- src/base/abci/abc.c | 123 ++++++++- src/base/abci/abcDar.c | 65 +++++ src/base/io/ioReadBlifMv.c | 4 +- src/bdd/parse/parseCore.c | 21 +- 12 files changed, 911 insertions(+), 20 deletions(-) create mode 100644 src/aig/saig/saigSynch.c (limited to 'src') diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index b8f767df..9204c2a5 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -21,6 +21,7 @@ #include "fra.h" #include "ioa.h" #include "int.h" +#include "ssw.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -75,6 +76,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) ***********************************************************************/ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ) { + Ssw_Pars_t Pars2, * pPars2 = &Pars2; Fra_Ssw_t Pars, * pPars = &Pars; Fra_Sml_t * pSml; Aig_Man_t * pNew, * pTemp; @@ -89,6 +91,8 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ) if ( RetValue >= 0 ) goto finish; + // prepare parameters + Ssw_ManSetDefaultParams( pPars2 ); // prepare parameters memset( pPars, 0, sizeof(Fra_Ssw_t) ); pPars->fLatchCorr = fLatchCorr; @@ -288,12 +292,17 @@ PRT( "Time", clock() - clk ); goto finish; } } - + clk = clock(); pPars->nFramesK = nFrames; pPars->TimeLimit = TimeLeft; pPars->fSilent = pParSec->fSilent; - pNew = Fra_FraigInduction( pTemp = pNew, pPars ); +// pNew = Fra_FraigInduction( pTemp = pNew, pPars ); + + pPars2->nFramesK = nFrames; + pPars2->nBTLimit = 1000 * nFrames; + Aig_ManSetRegNum( pNew, pNew->nRegs ); + pNew = Ssw_SignalCorrespondence( pTemp = pNew, pPars2 ); if ( pNew == NULL ) { pNew = pTemp; @@ -306,7 +315,7 @@ clk = clock(); if ( pParSec->fVerbose ) { printf( "K-step (K=%2d,I=%3d): Latches = %5d. Nodes = %6d. ", - nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); + nFrames, pPars2->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } if ( RetValue != -1 ) diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 88cc2c2d..da194f49 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -89,6 +89,7 @@ extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); extern int Saig_Interpolate( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth ); /*=== saigMiter.c ==========================================================*/ extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ); +extern Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p ); /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 0c547257..5b18db6e 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -48,6 +48,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ) assert( Saig_ManPiNum(p1) == Saig_ManPiNum(p2) ); assert( Saig_ManPoNum(p1) == Saig_ManPoNum(p2) ); pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) ); + pNew->pName = Aig_UtilStrsav( "miter" ); // map constant nodes Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew); @@ -88,6 +89,40 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the AIG to have constant-0 initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i; + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Saig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Saig_ManForEachLo( p, pObj, i ) + pObj->pData = Aig_NotCond( Aig_ObjCreatePi( pNew ), pObj->fMarkA ); + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Saig_ManForEachPo( p, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Saig_ManForEachLi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), pObj->fMarkA ) ); + Aig_ManSetRegNum( pNew, Saig_ManRegNum(p) ); + assert( Aig_ManNodeNum(pNew) == Aig_ManNodeNum(p) ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c new file mode 100644 index 00000000..9dbbb420 --- /dev/null +++ b/src/aig/saig/saigSynch.c @@ -0,0 +1,623 @@ +/**CFile**************************************************************** + + FileName [saigSynch.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Computation of synchronizing sequence.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigSynch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// 0 1 x +// 00 01 11 +// 0 00 00 00 00 +// 1 01 00 01 11 +// x 11 00 11 11 + +static inline unsigned Saig_SynchNot( unsigned w ) +{ + return w^((~(w&(w>>1)))&0x55555555); +} +static inline unsigned Saig_SynchAnd( unsigned u, unsigned w ) +{ + return (u&w)|((((u&(u>>1)&w&~(w>>1))|(w&(w>>1)&u&~(u>>1)))&0x55555555)<<1); +} +static inline unsigned Saig_SynchRandomBinary() +{ + return Aig_ManRandom(0) & 0x55555555; +} +static inline unsigned Saig_SynchRandomTernary() +{ + unsigned w = Aig_ManRandom(0); + return w^((~w)&(w>>1)&0x55555555); +} +static inline unsigned Saig_SynchTernary( int v ) +{ + assert( v == 0 || v == 1 || v == 3 ); + return v? ((v==1)? 0x55555555 : 0xffffffff) : 0; +} + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Initializes registers to the ternary state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_SynchSetConstant1( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords ) +{ + Aig_Obj_t * pObj; + unsigned * pSim; + int w; + pObj = Aig_ManConst1( pAig ); + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + for ( w = 0; w < nWords; w++ ) + pSim[w] = 0x55555555; +} + +/**Function************************************************************* + + Synopsis [Initializes registers to the ternary state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_SynchInitRegsTernary( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords ) +{ + Aig_Obj_t * pObj; + unsigned * pSim; + int i, w; + Saig_ManForEachLo( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + for ( w = 0; w < nWords; w++ ) + pSim[w] = 0xffffffff; + } +} + +/**Function************************************************************* + + Synopsis [Initializes registers to the given binary state.] + + Description [The binary state is stored in pObj->fMarkA.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_SynchInitRegsBinary( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords ) +{ + Aig_Obj_t * pObj; + unsigned * pSim; + int i, w; + Saig_ManForEachLo( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchTernary( pObj->fMarkA ); + } +} + +/**Function************************************************************* + + Synopsis [Initializes random binary primary inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_SynchInitPisRandom( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords ) +{ + Aig_Obj_t * pObj; + unsigned * pSim; + int i, w; + Saig_ManForEachPi( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchRandomBinary(); + } +} + +/**Function************************************************************* + + Synopsis [Initializes random binary primary inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_SynchInitPisGiven( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, char * pValues ) +{ + Aig_Obj_t * pObj; + unsigned * pSim; + int i, w; + Saig_ManForEachPi( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchTernary( pValues[i] ); + } +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_SynchTernarySimulate( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords ) +{ + Aig_Obj_t * pObj; + unsigned * pSim0, * pSim1, * pSim; + int i, w; + // simulate nodes + Aig_ManForEachNode( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + pSim0 = Vec_PtrEntry( vSimInfo, Aig_ObjFaninId0(pObj) ); + pSim1 = Vec_PtrEntry( vSimInfo, Aig_ObjFaninId1(pObj) ); + if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) + { + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchAnd( Saig_SynchNot(pSim0[w]), Saig_SynchNot(pSim1[w]) ); + } + else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) + { + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchAnd( pSim0[w], Saig_SynchNot(pSim1[w]) ); + } + else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) + { + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchAnd( Saig_SynchNot(pSim0[w]), pSim1[w] ); + } + else // if ( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) + { + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchAnd( pSim0[w], pSim1[w] ); + } + } + // transfer values to register inputs + Saig_ManForEachLi( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + pSim0 = Vec_PtrEntry( vSimInfo, Aig_ObjFaninId0(pObj) ); + if ( Aig_ObjFaninC0(pObj) ) + { + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchNot( pSim0[w] ); + } + else + { + for ( w = 0; w < nWords; w++ ) + pSim[w] = pSim0[w]; + } + } +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_SynchTernaryTransferState( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords ) +{ + Aig_Obj_t * pObjLi, * pObjLo; + unsigned * pSim0, * pSim1; + int i, w; + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + pSim0 = Vec_PtrEntry( vSimInfo, pObjLi->Id ); + pSim1 = Vec_PtrEntry( vSimInfo, pObjLo->Id ); + for ( w = 0; w < nWords; w++ ) + pSim1[w] = pSim0[w]; + } +} + +/**Function************************************************************* + + Synopsis [Returns the number of Xs in the smallest ternary pattern.] + + Description [Returns the number of this pattern.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_SynchCountX( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int * piPat ) +{ + Aig_Obj_t * pObj; + unsigned * pSim; + int * pCounters, i, w, b; + int iPatBest, iTernMin; + // count the number of ternary values in each pattern + pCounters = CALLOC( int, nWords * 16 ); + Saig_ManForEachLi( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + for ( w = 0; w < nWords; w++ ) + for ( b = 0; b < 16; b++ ) + if ( ((pSim[w] >> (b << 1)) & 3) == 3 ) + pCounters[16 * w + b]++; + } + // get the best pattern + iPatBest = -1; + iTernMin = 1 + Saig_ManRegNum(pAig); + for ( b = 0; b < 16 * nWords; b++ ) + if ( iTernMin > pCounters[b] ) + { + iTernMin = pCounters[b]; + iPatBest = b; + if ( iTernMin == 0 ) + break; + } + free( pCounters ); + *piPat = iPatBest; + return iTernMin; +} + +/**Function************************************************************* + + Synopsis [Saves the best pattern found and initializes the registers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_SynchSavePattern( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, int nWords, int iPat, Vec_Str_t * vSequence ) +{ + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + unsigned * pSim; + int Counter, Value, i, w; + assert( iPat < 16 * nWords ); + Saig_ManForEachPi( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + Value = (pSim[iPat>>4] >> ((iPat&0xf) << 1)) & 3; + Vec_StrPush( vSequence, (char)Value ); +// printf( "%d ", Value ); + } +// printf( "\n" ); + Counter = 0; + Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObjLi->Id ); + Value = (pSim[iPat>>4] >> ((iPat&0xf) << 1)) & 3; + Counter += (Value == 3); + // save patern in the same register + pSim = Vec_PtrEntry( vSimInfo, pObjLo->Id ); + for ( w = 0; w < nWords; w++ ) + pSim[w] = Saig_SynchTernary( Value ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Implement synchronizing sequence.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_SynchSequenceRun( Aig_Man_t * pAig, Vec_Ptr_t * vSimInfo, Vec_Str_t * vSequence, int fTernary ) +{ + unsigned * pSim; + Aig_Obj_t * pObj; + int Counter, nIters, Value, i; + assert( Vec_StrSize(vSequence) % Saig_ManPiNum(pAig) == 0 ); + nIters = Vec_StrSize(vSequence) / Saig_ManPiNum(pAig); + Saig_SynchSetConstant1( pAig, vSimInfo, 1 ); + if ( fTernary ) + Saig_SynchInitRegsTernary( pAig, vSimInfo, 1 ); + else + Saig_SynchInitRegsBinary( pAig, vSimInfo, 1 ); + for ( i = 0; i < nIters; i++ ) + { + Saig_SynchInitPisGiven( pAig, vSimInfo, 1, Vec_StrArray(vSequence) + i * Saig_ManPiNum(pAig) ); + Saig_SynchTernarySimulate( pAig, vSimInfo, 1 ); + Saig_SynchTernaryTransferState( pAig, vSimInfo, 1 ); + } + // save the resulting state in the registers + Counter = 0; + Saig_ManForEachLo( pAig, pObj, i ) + { + pSim = Vec_PtrEntry( vSimInfo, pObj->Id ); + Value = pSim[0] & 3; + assert( Value != 2 ); + Counter += (Value == 3); + pObj->fMarkA = Value; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Determines synchronizing sequence using ternary simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Saig_SynchSequence( Aig_Man_t * pAig, int nWords ) +{ + int nStepsMax = 100; // the maximum number of simulation steps + int nTriesMax = 100; // the maximum number of attempts at each step + int fVerify = 1; // verify the resulting pattern + Vec_Str_t * vSequence; + Vec_Ptr_t * vSimInfo; + int nTerPrev, nTerCur, nTerCur2; + int iPatBest, RetValue, s, t; + assert( Saig_ManRegNum(pAig) > 0 ); + // reset random numbers + Aig_ManRandom( 1 ); + // start the sequence + vSequence = Vec_StrAlloc( 20 * Saig_ManRegNum(pAig) ); + // create sim info and init registers + vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords ); + Saig_SynchSetConstant1( pAig, vSimInfo, nWords ); + // iterate over the timeframes + nTerPrev = Saig_ManRegNum(pAig); + Saig_SynchInitRegsTernary( pAig, vSimInfo, nWords ); + for ( s = 0; s < nStepsMax && nTerPrev > 0; s++ ) + { + for ( t = 0; t < nTriesMax; t++ ) + { + Saig_SynchInitPisRandom( pAig, vSimInfo, nWords ); + Saig_SynchTernarySimulate( pAig, vSimInfo, nWords ); + nTerCur = Saig_SynchCountX( pAig, vSimInfo, nWords, &iPatBest ); + if ( nTerCur < nTerPrev ) + break; + } + if ( t == nTriesMax ) + break; + nTerCur2 = Saig_SynchSavePattern( pAig, vSimInfo, nWords, iPatBest, vSequence ); + assert( nTerCur == nTerCur2 ); + nTerPrev = nTerCur; + } + if ( nTerPrev > 0 ) + { + printf( "Count not initialize %d registers.\n", nTerPrev ); + Vec_PtrFree( vSimInfo ); + Vec_StrFree( vSequence ); + return NULL; + } + // verify that the sequence is correct + if ( fVerify ) + { + RetValue = Saig_SynchSequenceRun( pAig, vSimInfo, vSequence, 1 ); + assert( RetValue == 0 ); + Aig_ManCleanMarkA( pAig ); + } + Vec_PtrFree( vSimInfo ); + return vSequence; +} + +/**Function************************************************************* + + Synopsis [Determines synchronizing sequence using ternary simulation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose ) +{ + Aig_Man_t * pAigZero; + Vec_Str_t * vSequence; + Vec_Ptr_t * vSimInfo; + int RetValue, clk; + +clk = clock(); + // derive synchronization sequence + vSequence = Saig_SynchSequence( pAig, nWords ); + if ( vSequence == NULL ) + printf( "Design 1: Synchronizing sequence is not found. " ); + else if ( fVerbose ) + printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSequence) / Saig_ManPiNum(pAig) ); + if ( fVerbose ) + { + PRT( "Time", clock() - clk ); + } + else + printf( "\n" ); + if ( vSequence == NULL ) + { + printf( "Quitting synchronization.\n" ); + return NULL; + } + + // apply synchronization sequence + vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), 1 ); + RetValue = Saig_SynchSequenceRun( pAig, vSimInfo, vSequence, 1 ); + assert( RetValue == 0 ); + // duplicate + pAigZero = Saig_ManDupInitZero( pAig ); + // cleanup + Vec_PtrFree( vSimInfo ); + Vec_StrFree( vSequence ); + Aig_ManCleanMarkA( pAig ); + return pAigZero; +} + +/**Function************************************************************* + + Synopsis [Creates SEC miter for two designs without initial state.] + + Description [The designs (pAig1 and pAig2) are assumed to have ternary + initial state. Determines synchronizing sequences using ternary simulation. + Simulates the sequences on both designs to come up with equivalent binary + initial states. Create seq miter for the designs starting in these states.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose ) +{ + Aig_Man_t * pAig1z, * pAig2z, * pMiter; + Vec_Str_t * vSeq1, * vSeq2; + Vec_Ptr_t * vSimInfo; + int RetValue, clk; +/* + { + unsigned u = Saig_SynchRandomTernary(); + unsigned w = Saig_SynchRandomTernary(); + unsigned x = Saig_SynchNot( u ); + unsigned y = Saig_SynchNot( w ); + unsigned z = Saig_SynchAnd( x, y ); + + Extra_PrintBinary( stdout, &u, 32 ); printf( "\n" ); + Extra_PrintBinary( stdout, &w, 32 ); printf( "\n" ); printf( "\n" ); + Extra_PrintBinary( stdout, &x, 32 ); printf( "\n" ); + Extra_PrintBinary( stdout, &y, 32 ); printf( "\n" ); printf( "\n" ); + Extra_PrintBinary( stdout, &z, 32 ); printf( "\n" ); + } +*/ + // report statistics + if ( fVerbose ) + { + printf( "Design 1: " ); + Aig_ManPrintStats( pAig1 ); + printf( "Design 2: " ); + Aig_ManPrintStats( pAig2 ); + } + + // synchronize the first design + clk = clock(); + vSeq1 = Saig_SynchSequence( pAig1, nWords ); + if ( vSeq1 == NULL ) + printf( "Design 1: Synchronizing sequence is not found. " ); + else if ( fVerbose ) + printf( "Design 1: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq1) / Saig_ManPiNum(pAig1) ); + if ( fVerbose ) + { + PRT( "Time", clock() - clk ); + } + else + printf( "\n" ); + + // synchronize the first design + clk = clock(); + vSeq2 = Saig_SynchSequence( pAig2, nWords ); + if ( vSeq2 == NULL ) + printf( "Design 2: Synchronizing sequence is not found. " ); + else if ( fVerbose ) + printf( "Design 2: Synchronizing sequence of length %4d is found. ", Vec_StrSize(vSeq2) / Saig_ManPiNum(pAig2) ); + if ( fVerbose ) + { + PRT( "Time", clock() - clk ); + } + else + printf( "\n" ); + + // quit if one of the designs cannot be synchronized + if ( vSeq1 == NULL || vSeq2 == NULL ) + { + printf( "Quitting synchronization.\n" ); + if ( vSeq1 ) Vec_StrFree( vSeq1 ); + if ( vSeq2 ) Vec_StrFree( vSeq2 ); + return NULL; + } + clk = clock(); + vSimInfo = Vec_PtrAllocSimInfo( AIG_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 ); + + // process Design 1 + RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 ); + assert( RetValue == 0 ); + RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq2, 0 ); + assert( RetValue == 0 ); + + // process Design 2 + RetValue = Saig_SynchSequenceRun( pAig2, vSimInfo, vSeq2, 1 ); + assert( RetValue == 0 ); + + // duplicate designs + pAig1z = Saig_ManDupInitZero( pAig1 ); + pAig2z = Saig_ManDupInitZero( pAig2 ); + pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 ); + Aig_ManStop( pAig1z ); + Aig_ManStop( pAig2z ); + + // cleanup + Vec_PtrFree( vSimInfo ); + Vec_StrFree( vSeq1 ); + Vec_StrFree( vSeq2 ); + Aig_ManCleanMarkA( pAig1 ); + Aig_ManCleanMarkA( pAig2 ); + + if ( fVerbose ) + { + printf( "Miter of the synchronized designs is constructed. " ); + PRT( "Time", clock() - clk ); + } + return pMiter; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index e6096c54..b03a248e 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -139,8 +139,9 @@ clk = clock(); printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal ); - printf( "Use = %5d. Skip = %5d. ", - p->nRefUse, p->nRefSkip ); + if ( p->pPars->fSkipCheck ) + printf( "Use = %5d. Skip = %5d. ", + p->nRefUse, p->nRefSkip ); PRT( "T", clock() - clk ); } Ssw_ManCleanup( p ); diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c index f25cee45..559f7b6c 100644 --- a/src/aig/ssw/sswMan.c +++ b/src/aig/ssw/sswMan.c @@ -47,14 +47,14 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) Aig_ManFanoutStart( pAig ); Aig_ManSetPioNumbers( pAig ); // create interpolation manager - p = ALLOC( Ssw_Man_t, 1 ); + p = ALLOC( Ssw_Man_t, 1 ); memset( p, 0, sizeof(Ssw_Man_t) ); p->pPars = pPars; p->pAig = pAig; p->nFrames = pPars->nFramesK + 1; p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames ); // SAT solving - p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames ); + p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) ); p->vFanins = Vec_PtrAlloc( 100 ); p->vSimRoots = Vec_PtrAlloc( 1000 ); p->vSimClasses = Vec_PtrAlloc( 1000 ); @@ -99,8 +99,8 @@ void Ssw_ManPrintStats( Ssw_Man_t * p ) { double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20); - printf( "Parameters: Fr = %d. C-limit = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", - p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory ); + printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", + p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory ); printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n", Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), p->nSatVarsTotal/p->pPars->nIters ); @@ -149,7 +149,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p ) p->nSatVarsTotal += p->pSat->size; sat_solver_delete( p->pSat ); p->pSat = NULL; - memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * p->nFrames ); + memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) ); } p->nConstrTotal = 0; p->nConstrReduced = 0; diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c index 6ef5ec20..3fa39612 100644 --- a/src/aig/ssw/sswSimSat.c +++ b/src/aig/ssw/sswSimSat.c @@ -234,7 +234,6 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR // set the PI simulation information Aig_ManConst1(p->pAig)->fMarkB = 1; Aig_ManForEachPi( p->pAig, pObj, i ) -// pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f ); pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i ); // simulate internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) @@ -244,10 +243,18 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 ); RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 ); // make sure refinement happened - if ( Aig_ObjIsConst1(pRepr) ) + if ( Aig_ObjIsConst1(pRepr) ) + { assert( RetValue1 ); + if ( RetValue1 == 0 ) + printf( "\nSsw_ManResimulateCexTotal() Error: RetValue1 does not hold.\n" ); + } else + { assert( RetValue2 ); + if ( RetValue2 == 0 ) + printf( "\nSsw_ManResimulateCexTotal() Error: RetValue2 does not hold.\n" ); + } p->timeSimSat += clock() - clk; } @@ -266,8 +273,6 @@ p->timeSimSat += clock() - clk; void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f ) { int RetValue1, RetValue2, clk = clock(); - // save the counter-example -// Ssw_SmlSavePatternAig( p, f ); // set the PI simulation information Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords ); // simulate internal nodes @@ -277,9 +282,17 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 ); // make sure refinement happened if ( Aig_ObjIsConst1(pRepr) ) + { assert( RetValue1 ); + if ( RetValue1 == 0 ) + printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue1 does not hold.\n" ); + } else + { assert( RetValue2 ); + if ( RetValue2 == 0 ) + printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue2 does not hold.\n" ); + } p->timeSimSat += clock() - clk; } diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index 5ad6d78e..3dccc08d 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -222,6 +222,7 @@ clk = clock(); p->fRefined = 0; if ( p->pPars->fVerbose ) pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); + Ssw_ManStartSolver( p ); for ( f = 0; f < p->pPars->nFramesK; f++ ) { // map constants and PIs @@ -241,8 +242,13 @@ clk = clock(); if ( f == p->pPars->nFramesK - 1 ) break; // transfer latch input to the latch outputs + // build logic cones for register outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) - Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) ); + { + pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f); + Ssw_ObjSetFraig( p, pObjLo, f+1, pObjNew ); + Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) ); + } } if ( p->pPars->fVerbose ) Bar_ProgressStop( pProgress ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3c7314ef..0db761c7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -199,6 +199,7 @@ static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -463,6 +464,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "sim", Abc_CommandSim, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "phase", Abc_CommandDarPhase, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "synch", Abc_CommandSynch, 1 ); Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 ); @@ -4862,7 +4864,6 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) nArgcNew = argc - globalUtilOptind; if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; - // compute the miter pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize, fImplic, fMulti ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); @@ -14424,6 +14425,121 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSynch( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtkRes, * pNtk1, * pNtk2, * pNtk; + char ** pArgvNew; + int nArgcNew; + int fDelete1, fDelete2; + int c; + int nWords; + int fVerbose; + + extern Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nWords = 32; + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF ) + { + switch ( c ) + { + case 'W': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + nWords = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nWords <= 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( nArgcNew == 0 ) + { + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + pNtkRes = Abc_NtkDarSynchOne( pNtk, nWords, fVerbose ); + } + else + { + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + return 1; + if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 ) + { + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + printf( "The network has no latches..\n" ); + return 0; + } + + // modify the current network + pNtkRes = Abc_NtkDarSynch( pNtk1, pNtk2, nWords, fVerbose ); + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + } + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Synchronization has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: synch [-W ] [-vh] \n" ); + fprintf( pErr, "\t derives and applies synchronization sequence\n" ); + fprintf( pErr, "\t-W num : the number of simulation words [default = %d]\n", nWords ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tfile1 : (optional) the file with the first design\n"); + fprintf( pErr, "\tfile2 : (optional) the file with the second design\n\n"); + fprintf( pErr, "\t If no designs are given on the command line,\n" ); + fprintf( pErr, "\t assumes the current network has no initial state,\n" ); + fprintf( pErr, "\t derives synchronization sequence and applies it.\n\n" ); + fprintf( pErr, "\t If two designs are given on the command line\n" ); + fprintf( pErr, "\t assumes both of them have no initial state,\n" ); + fprintf( pErr, "\t derives sequences for both designs, synchorinizes\n" ); + fprintf( pErr, "\t them, and creates SEC miter comparing two designs.\n\n" ); + fprintf( pErr, "\t If only one design is given on the command line,\n" ); + fprintf( pErr, "\t considers the second design to be the current network,\n" ); + fprintf( pErr, "\t and derives SEC miter for them, as described above.\n" ); + return 1; +} /**Function************************************************************* @@ -14842,6 +14958,8 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 ) { + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); printf( "The network has no latches. Used combinational command \"cec\".\n" ); return 0; } @@ -14960,9 +15078,10 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) nArgcNew = argc - globalUtilOptind; if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; - if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 ) { + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); printf( "The network has no latches. Used combinational command \"cec\".\n" ); return 0; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 37cd6853..f1e5efb0 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2184,6 +2184,71 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in return pNtkAig; } +/**Function************************************************************* + + Synopsis [Performs phase abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose ) +{ + extern Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose ); + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Saig_SynchSequenceApply( pTemp = pMan, nWords, fVerbose ); + Aig_ManStop( pTemp ); + if ( pMan == NULL ) + return NULL; + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Performs phase abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose ) +{ + extern Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose ); + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan1, * pMan2, * pMan; + pMan1 = Abc_NtkToDar( pNtk1, 0, 1 ); + if ( pMan1 == NULL ) + return NULL; + pMan2 = Abc_NtkToDar( pNtk2, 0, 1 ); + if ( pMan2 == NULL ) + { + Aig_ManStop( pMan1 ); + return NULL; + } + pMan = Saig_Synchronize( pMan1, pMan2, nWords, fVerbose ); + Aig_ManStop( pMan1 ); + Aig_ManStop( pMan2 ); + if ( pMan == NULL ) + return NULL; + pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig->pName = Extra_UtilStrsav("miter"); + pNtkAig->pSpec = NULL; + Aig_ManStop( pMan ); + return pNtkAig; +} + /**Function************************************************************* Synopsis [Performs phase abstraction.] diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 52d7eb06..880c2b5f 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -146,7 +146,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) // start the file reader p = Io_MvAlloc(); p->fBlifMv = fBlifMv; - p->fUseReset = 0; + p->fUseReset = 1; p->pFileName = pFileName; p->pBuffer = Io_MvLoadFile( pFileName ); if ( p->pBuffer == NULL ) @@ -704,7 +704,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p ) int i, k; // iterate through the models Vec_PtrForEachEntry( p->vModels, pMod, i ) - { + { // check if there any MV lines if ( Vec_PtrSize(pMod->vMvs) > 0 ) Abc_NtkStartMvVars( pMod->pNtk ); diff --git a/src/bdd/parse/parseCore.c b/src/bdd/parse/parseCore.c index 0071fb5a..88888379 100644 --- a/src/bdd/parse/parseCore.c +++ b/src/bdd/parse/parseCore.c @@ -362,6 +362,7 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in default: // scan the next name +/* fFound = 0; for ( i = 0; pTemp[i] && pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n'; i++ ) { @@ -375,13 +376,31 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in if ( fFound ) break; } +*/ + // bug fix by SV (9/11/08) + fFound = 0; + for ( i = 0; pTemp[i] && pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' && + pTemp[i] != PARSE_SYM_AND1 && pTemp[i] != PARSE_SYM_AND2 && pTemp[i] != PARSE_SYM_XOR1 && + pTemp[i] != PARSE_SYM_XOR2 && pTemp[i] != PARSE_SYM_XOR3 && pTemp[i] != PARSE_SYM_XOR && + pTemp[i] != PARSE_SYM_OR1 && pTemp[i] != PARSE_SYM_OR2 && pTemp[i] != PARSE_SYM_CLOSE; + i++ ) + {} + for ( v = 0; v < nVars; v++ ) + { + if ( strncmp( pTemp, ppVarNames[v], i ) == 0 && strlen(ppVarNames[v]) == (unsigned)(i) ) + { + pTemp += i-1; + fFound = 1; + break; + } + } + if ( !fFound ) { fprintf( pOutput, "Parse_FormulaParser(): The parser cannot find var \"%s\" in the input var list.\n", pTemp ); Flag = PARSE_FLAG_ERROR; break; } - // assume operation AND, if vars follow one another if ( Flag == PARSE_FLAG_VAR ) Parse_StackOpPush( pStackOp, PARSE_OPER_AND ); -- cgit v1.2.3