summaryrefslogtreecommitdiffstats
path: root/src/aig/saig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/saig')
-rw-r--r--src/aig/saig/saig.h1
-rw-r--r--src/aig/saig/saigMiter.c35
-rw-r--r--src/aig/saig/saigSynch.c623
3 files changed, 659 insertions, 0 deletions
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 ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-07 19:19:58 +0000