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 +- 8 files changed, 703 insertions(+), 15 deletions(-) create mode 100644 src/aig/saig/saigSynch.c (limited to 'src/aig') 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 ); -- cgit v1.2.3