diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-25 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-25 08:01:00 -0700 |
commit | d2b735f794575ce0f10f01bba1255cf1dc3b8aaf (patch) | |
tree | baac975efb3057f03506f165acbd36d2e67341b6 /src/aig/ssw | |
parent | 2418d9b08d0b49c675f02dc2351e2230079174af (diff) | |
download | abc-d2b735f794575ce0f10f01bba1255cf1dc3b8aaf.tar.gz abc-d2b735f794575ce0f10f01bba1255cf1dc3b8aaf.tar.bz2 abc-d2b735f794575ce0f10f01bba1255cf1dc3b8aaf.zip |
Version abc81025
Diffstat (limited to 'src/aig/ssw')
-rw-r--r-- | src/aig/ssw/module.make | 1 | ||||
-rw-r--r-- | src/aig/ssw/ssw.h | 1 | ||||
-rw-r--r-- | src/aig/ssw/sswClass.c | 52 | ||||
-rw-r--r-- | src/aig/ssw/sswInt.h | 1 | ||||
-rw-r--r-- | src/aig/ssw/sswIslands.c | 382 | ||||
-rw-r--r-- | src/aig/ssw/sswPairs.c | 2 |
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 |