summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/module.make1
-rw-r--r--src/aig/ssw/ssw.h1
-rw-r--r--src/aig/ssw/sswClass.c52
-rw-r--r--src/aig/ssw/sswInt.h1
-rw-r--r--src/aig/ssw/sswIslands.c382
-rw-r--r--src/aig/ssw/sswPairs.c2
6 files changed, 434 insertions, 5 deletions
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index a7d940b4..1e79c955 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -4,6 +4,7 @@ SRC += src/aig/ssw/sswAig.c \
src/aig/ssw/sswCnf.c \
src/aig/ssw/sswCore.c \
src/aig/ssw/sswDyn.c \
+ src/aig/ssw/sswIslands.c \
src/aig/ssw/sswLcorr.c \
src/aig/ssw/sswMan.c \
src/aig/ssw/sswPart.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 73226dbe..4bb2356a 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -104,6 +104,7 @@ extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
+extern int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose );
extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index f234a58f..3dfee28b 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -446,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
assert( p->pId2Class[pObj->Id] == NULL );
pRepr = Aig_ObjRepr( p->pAig, pObj );
assert( pRepr != NULL );
- Vec_PtrPush( p->vRefined, pObj );
+// Vec_PtrPush( p->vRefined, pObj );
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
{
assert( p->pClassSizes[pRepr->Id] == 0 );
@@ -455,7 +455,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
p->nCands1--;
return;
}
- Vec_PtrPush( p->vRefined, pRepr );
+// Vec_PtrPush( p->vRefined, pRepr );
Aig_ObjSetRepr( p->pAig, pObj, NULL );
assert( p->pId2Class[pRepr->Id][0] == pRepr );
assert( p->pClassSizes[pRepr->Id] >= 2 );
@@ -793,6 +793,48 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
/**Function*************************************************************
+ Synopsis [Creates classes from the temporary representation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs )
+{
+ Ssw_Cla_t * p;
+ Aig_Obj_t ** ppClassNew;
+ Aig_Obj_t * pObj, * pRepr;
+ int i;
+ // start the classes
+ p = Ssw_ClassesStart( pMiter );
+ // allocate memory for classes
+ p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
+ // create classes
+ for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
+ {
+ pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
+ pObj = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
+ assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
+ Aig_ObjSetRepr( pMiter, pObj, pRepr );
+ // get room for storing the class
+ ppClassNew = p->pMemClasses + i;
+ ppClassNew[0] = pRepr;
+ ppClassNew[1] = pObj;
+ // create new class
+ Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
+ }
+ // prepare room for new classes
+ p->pMemClassesFree = NULL;
+ Ssw_ClassesCheck( p );
+// Ssw_ClassesPrint( p, 0 );
+ return p;
+}
+
+/**Function*************************************************************
+
Synopsis [Iteratively refines the classes after simulation.]
Description [Returns the number of refinements performed.]
@@ -820,8 +862,8 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
// remember that this class is refined
- Ssw_ClassForEachNode( p, pReprOld, pObj, i )
- Vec_PtrPush( p->vRefined, pObj );
+// Ssw_ClassForEachNode( p, pReprOld, pObj, i )
+// Vec_PtrPush( p->vRefined, pObj );
// get the new representative
pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
@@ -944,7 +986,7 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
{
Vec_PtrPush( p->vClassNew, pObj );
- Vec_PtrPush( p->vRefined, pObj );
+// Vec_PtrPush( p->vRefined, pObj );
}
}
// check if there is a new class
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 8d8d3265..90c1367f 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -205,6 +205,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int n
extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
+extern Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c
new file mode 100644
index 00000000..5a5783f7
--- /dev/null
+++ b/src/aig/ssw/sswIslands.c
@@ -0,0 +1,382 @@
+/**CFile****************************************************************
+
+ FileName [sswIslands.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Inductive prover with constraints.]
+
+ Synopsis [Detection of islands of difference.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 1, 2008.]
+
+ Revision [$Id: sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Aig_ObjChild0Copy2( Aig_Obj_t * pObj ) { return Aig_ObjFanin0(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; }
+static inline Aig_Obj_t * Aig_ObjChild1Copy2( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Creates pair of structurally equivalent nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+ pObj0->pData = pObj1;
+ pObj1->pData = pObj0;
+ Vec_IntPush( vPairs, pObj0->Id );
+ Vec_IntPush( vPairs, pObj1->Id );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detects islands of common logic and returns them as pairs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Ssw_DetectIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose )
+{
+ Vec_Int_t * vPairs;
+ Aig_Obj_t * pObj0, * pObj1, * pFanin0, * pFanin1;
+ int i;
+ assert( Aig_ManRegNum(p0) > 0 );
+ assert( Aig_ManRegNum(p1) > 0 );
+ assert( Aig_ManRegNum(p0) >= nCommonFlops );
+ assert( Aig_ManRegNum(p1) >= nCommonFlops );
+ assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
+ assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
+ Aig_ManCleanData( p0 );
+ Aig_ManCleanData( p1 );
+ // start structural equivalence
+ vPairs = Vec_IntAlloc( 1000 );
+ Ssw_CreatePair( vPairs, Aig_ManConst1(p0), Aig_ManConst1(p1) );
+ Saig_ManForEachPi( p0, pObj0, i )
+ Ssw_CreatePair( vPairs, pObj0, Aig_ManPi(p1, i) );
+ Saig_ManForEachLo( p0, pObj0, i )
+ {
+ if ( i == nCommonFlops )
+ break;
+ Ssw_CreatePair( vPairs, pObj0, Saig_ManLo(p1, i) );
+ }
+ // find structurally equivalent nodes
+ Aig_ManForEachNode( p0, pObj0, i )
+ {
+ pFanin0 = Aig_ObjChild0Copy2( pObj0 );
+ pFanin1 = Aig_ObjChild1Copy2( pObj0 );
+ if ( pFanin0 == NULL || pFanin1 == NULL )
+ continue;
+ pObj1 = Aig_TableLookupTwo( p1, pFanin0, pFanin1 );
+ if ( pObj1 == NULL )
+ continue;
+ Ssw_CreatePair( vPairs, pObj0, pObj1 );
+ }
+ return vPairs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects additional Lis and Los.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_CollectExtraLiLo( Aig_Man_t * p, int nCommonFlops, Vec_Ptr_t * vLis, Vec_Ptr_t * vLos )
+{
+ Aig_Obj_t * pObjLo, * pObjLi;
+ int i;
+ Saig_ManForEachLiLo( p, pObjLo, pObjLi, i )
+ {
+ if ( i < nCommonFlops )
+ continue;
+ Vec_PtrPush( vLis, pObjLi );
+ Vec_PtrPush( vLos, pObjLo );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Overlays and extends the pairs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_OverlayIslands( Aig_Man_t * pTo, Aig_Man_t * pFrom, Vec_Ptr_t * vLisFrom, Vec_Ptr_t * vLosFrom, Vec_Int_t * vPairs, int nCommonFlops, int fToGoesFirst )
+{
+ Aig_Obj_t * pObjFrom, * pObjTo, * pFanin0To, * pFanin1To;
+ int i;
+ // create additional register outputs of From in To
+ Vec_PtrForEachEntry( vLosFrom, pObjFrom, i )
+ {
+ pObjTo = Aig_ObjCreatePi( pTo );
+ if( fToGoesFirst )
+ Ssw_CreatePair( vPairs, pObjTo, pObjFrom );
+ else
+ Ssw_CreatePair( vPairs, pObjFrom, pObjTo );
+ }
+ // create additional nodes of From in To
+ Aig_ManForEachNode( pFrom, pObjFrom, i )
+ {
+ if ( pObjFrom->pData != NULL )
+ continue;
+ pFanin0To = Aig_ObjChild0Copy2( pObjFrom );
+ pFanin1To = Aig_ObjChild1Copy2( pObjFrom );
+ assert( pFanin0To != NULL && pFanin1To != NULL );
+ pObjTo = Aig_And( pTo, pFanin0To, pFanin1To );
+ if( fToGoesFirst )
+ Ssw_CreatePair( vPairs, pObjTo, pObjFrom );
+ else
+ Ssw_CreatePair( vPairs, pObjFrom, pObjTo );
+ }
+ // finally recreate additional register inputs
+ Vec_PtrForEachEntry( vLisFrom, pObjFrom, i )
+ {
+ pFanin0To = Aig_ObjChild0Copy2( pObjFrom );
+ Aig_ObjCreatePo( pTo, pFanin0To );
+ }
+ // update the number of registers
+ Aig_ManSetRegNum( pTo, Aig_ManRegNum(pTo) + Vec_PtrSize(vLisFrom) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Overlays and extends the pairs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManMiterWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, Aig_Man_t ** ppMiter, Vec_Int_t * vPairs )
+{
+ Aig_Man_t * pMiter;
+ Vec_Int_t * vPairsNew;
+ Aig_Obj_t * pObj0, * pObj1;
+ int i;
+ vPairsNew = Vec_IntAlloc( 1000 );
+ pMiter = Saig_ManCreateMiter( p0, p1, 0 );
+ for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
+ {
+ pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
+ pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
+ pObj0 = pObj0->pData;
+ pObj1 = pObj1->pData;
+ assert( !Aig_IsComplement(pObj0) );
+ assert( !Aig_IsComplement(pObj1) );
+ if ( pObj0 == pObj1 )
+ continue;
+ assert( pObj0->Id < pObj1->Id );
+ Vec_IntPush( vPairsNew, pObj0->Id );
+ Vec_IntPush( vPairsNew, pObj1->Id );
+ }
+ *ppMiter = pMiter;
+ return vPairsNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solves SEC using structural similarity.]
+
+ Description [Modifies both p0 and p1 by adding extra logic.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SecWithIslandsInternal( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars )
+{
+ Ssw_Man_t * p;
+ Ssw_Pars_t Pars;
+ Vec_Int_t * vPairs, * vPairsMiter;
+ Aig_Man_t * pMiter, * pAigNew;
+ Vec_Ptr_t * vLis0, * vLos0, * vLis1, * vLos1;
+ int nNodes, nRegs;
+ assert( Aig_ManRegNum(p0) > 0 );
+ assert( Aig_ManRegNum(p1) > 0 );
+ assert( Aig_ManRegNum(p0) >= nCommonFlops );
+ assert( Aig_ManRegNum(p1) >= nCommonFlops );
+ assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
+ assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
+ // derive pairs
+ vPairs = Ssw_DetectIslands( p0, p1, nCommonFlops, fVerbose );
+ if ( fVerbose )
+ {
+ printf( "Original managers:\n" );
+ Aig_ManPrintStats( p0 );
+ Aig_ManPrintStats( p1 );
+ printf( "Detected %d PI pairs, %d LO pairs, and %d node pairs.\n",
+ Saig_ManPiNum(p0), nCommonFlops, Vec_IntSize(vPairs)/2 - Saig_ManPiNum(p0) - nCommonFlops - 1 );
+ }
+ // complete the manager with islands
+ vLis0 = Vec_PtrAlloc( 100 );
+ vLos0 = Vec_PtrAlloc( 100 );
+ vLis1 = Vec_PtrAlloc( 100 );
+ vLos1 = Vec_PtrAlloc( 100 );
+ Ssw_CollectExtraLiLo( p0, nCommonFlops, vLis0, vLos0 );
+ Ssw_CollectExtraLiLo( p1, nCommonFlops, vLis1, vLos1 );
+
+ nRegs = Saig_ManRegNum(p0);
+ nNodes = Aig_ManNodeNum(p0);
+ Ssw_OverlayIslands( p0, p1, vLis1, vLos1, vPairs, nCommonFlops, 1 );
+ if ( fVerbose )
+ printf( "Completed p0 with %d registers and %d nodes.\n",
+ Saig_ManRegNum(p0) - nRegs, Aig_ManNodeNum(p0) - nNodes );
+
+ nRegs = Saig_ManRegNum(p1);
+ nNodes = Aig_ManNodeNum(p1);
+ Ssw_OverlayIslands( p1, p0, vLis0, vLos0, vPairs, nCommonFlops, 0 );
+ if ( fVerbose )
+ printf( "Completed p1 with %d registers and %d nodes.\n",
+ Saig_ManRegNum(p1) - nRegs, Aig_ManNodeNum(p1) - nNodes );
+ if ( fVerbose )
+ {
+ printf( "Modified managers:\n" );
+ Aig_ManPrintStats( p0 );
+ Aig_ManPrintStats( p1 );
+ }
+
+ Vec_PtrFree( vLis0 );
+ Vec_PtrFree( vLos0 );
+ Vec_PtrFree( vLis1 );
+ Vec_PtrFree( vLos1 );
+ // create sequential miter
+ vPairsMiter = Saig_ManMiterWithIslands( p0, p1, &pMiter, vPairs );
+ Vec_IntFree( vPairs );
+ // if parameters are not given, create them
+ if ( pPars == NULL )
+ Ssw_ManSetDefaultParams( pPars = &Pars );
+ // start the induction manager
+ p = Ssw_ManCreate( pMiter, pPars );
+ // create equivalence classes using these IDs
+ p->ppClasses = Ssw_ClassesFromIslands( pMiter, vPairsMiter );
+ p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
+ Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+ // perform refinement of classes
+ pAigNew = Ssw_SignalCorrespondenceRefine( p );
+ // cleanup
+ Ssw_ManStop( p );
+ Aig_ManStop( pMiter );
+ Vec_IntFree( vPairsMiter );
+ return pAigNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solves SEC using structural similarity.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SecWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars )
+{
+ Aig_Man_t * pAigRes;
+ Aig_Man_t * p0New, * p1New;
+ int RetValue, clk = clock();
+ // try the new AIGs
+// printf( "Performing verification using structural similarity.\n" );
+ p0New = Aig_ManDupSimple( p0 );
+ p1New = Aig_ManDupSimple( p1 );
+ pAigRes = Ssw_SecWithIslandsInternal( p0New, p1New, nCommonFlops, fVerbose, pPars );
+ Aig_ManStop( p0New );
+ Aig_ManStop( p1New );
+ // report the results
+ RetValue = Ssw_MiterStatus( pAigRes, 1 );
+ if ( RetValue == 1 )
+ printf( "Verification successful. " );
+ else if ( RetValue == 0 )
+ printf( "Verification failed with a counter-example. " );
+ else
+ printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
+ Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0New)+Aig_ManRegNum(p1New) );
+ PRT( "Time", clock() - clk );
+ // cleanup
+ Aig_ManStop( pAigRes );
+ return RetValue;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Solves SEC using structural similarity for the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SecWithIslandsMiter( Aig_Man_t * pMiter, int nCommonFlops, int fVerbose )
+{
+ Aig_Man_t * pPart0, * pPart1;
+ int RetValue;
+ if ( fVerbose )
+ Aig_ManPrintStats( pMiter );
+ // demiter the miter
+ if ( !Saig_ManDemiterSimpleDiff( pMiter, &pPart0, &pPart1 ) )
+ {
+ printf( "Demitering has failed.\n" );
+ return -1;
+ }
+ if ( fVerbose )
+ {
+// Aig_ManPrintStats( pPart0 );
+// Aig_ManPrintStats( pPart1 );
+// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
+// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
+// printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
+ }
+ RetValue = Ssw_SecWithIslands( pPart0, pPart1, nCommonFlops, fVerbose, NULL );
+ Aig_ManStop( pPart0 );
+ Aig_ManStop( pPart1 );
+ return RetValue;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c
index c77ad30d..1af357f9 100644
--- a/src/aig/ssw/sswPairs.c
+++ b/src/aig/ssw/sswPairs.c
@@ -276,6 +276,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) );
// create sequential miter
pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
+ Aig_ManCleanup( pMiter );
// transfer information to the miter
vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 );
// create representation of the classes
@@ -413,6 +414,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
// try the new AIGs
printf( "Performing general verification without node pairs.\n" );
pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
+ Aig_ManCleanup( pMiter );
pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
Aig_ManStop( pMiter );
// report the results
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 12:04:21 +0000