From ce690b29075a23a07673d0a4727f0bf9557ec882 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 15 Sep 2008 08:01:00 -0700 Subject: Version abc80915 --- src/aig/fra/fraLcr.c | 9 +- src/aig/saig/module.make | 1 + src/aig/ssw/module.make | 1 + src/aig/ssw/ssw.h | 4 +- src/aig/ssw/sswClass.c | 67 ++++++++ src/aig/ssw/sswCore.c | 119 +++++++------ src/aig/ssw/sswInt.h | 4 + src/aig/ssw/sswPairs.c | 437 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/ssw/sswSweep.c | 2 +- src/base/abci/abc.c | 20 ++- src/base/abci/abcDar.c | 42 ++++- 11 files changed, 643 insertions(+), 63 deletions(-) create mode 100644 src/aig/ssw/sswPairs.c (limited to 'src') diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index 4b2383aa..f597e090 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -612,6 +612,7 @@ p->timePart += clock() - clk2; Vec_PtrClear( p->vFraigs ); Vec_PtrForEachEntry( p->vParts, vPart, i ) { + int clk3 = clock(); if ( TimeLimit != 0.0 && clock() > TimeToStop ) { Vec_PtrForEachEntry( p->vFraigs, pAigPart, i ) @@ -628,9 +629,15 @@ clk2 = clock(); pAigTemp = Fra_FraigEquivence( pAigPart, nConfMax, 0 ); p->timeFraig += clock() - clk2; Vec_PtrPush( p->vFraigs, pAigTemp ); + { + char Name[1000]; + sprintf( Name, "part%04d.blif", i ); + Aig_ManDumpBlif( pAigPart, Name, NULL, NULL ); + } Aig_ManStop( pAigPart ); -//intf( "finished part %d (out of %d)\n", i, Vec_PtrSize(p->vParts) ); +printf( "Finished part %4d (out of %4d). ", i, Vec_PtrSize(p->vParts) ); +PRT( "Time", clock() - clk3 ); } Fra_ClassNodesUnmark( p ); diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 5a0f98da..fcdb3de3 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -8,4 +8,5 @@ SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigRetMin.c \ src/aig/saig/saigRetStep.c \ src/aig/saig/saigScl.c \ + src/aig/saig/saigSynch.c \ src/aig/saig/saigTrans.c diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make index b176d4db..daf69370 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/sswCore.c \ src/aig/ssw/sswMan.c \ src/aig/ssw/sswPart.c \ + src/aig/ssw/sswPairs.c \ src/aig/ssw/sswSat.c \ src/aig/ssw/sswSim.c \ src/aig/ssw/sswSimSat.c \ diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index f76664ec..14c10f6a 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -82,7 +82,9 @@ extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ); extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars ); /*=== sswPart.c ==========================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); - +/*=== sswPairs.c ===================================================*/ +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 ); #ifdef __cplusplus } diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c index d06cce49..e186946a 100644 --- a/src/aig/ssw/sswClass.c +++ b/src/aig/ssw/sswClass.c @@ -88,6 +88,7 @@ static inline void Ssw_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pOb static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize ) { assert( p->pId2Class[pRepr->Id] == NULL ); + assert( pClass[0] == pRepr ); p->pId2Class[pRepr->Id] = pClass; assert( p->pClassSizes[pRepr->Id] == 0 ); assert( nSize > 1 ); @@ -644,6 +645,72 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax return p; } +/**Function************************************************************* + + Synopsis [Creates classes from the temporary representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ) +{ + Ssw_Cla_t * p; + Aig_Obj_t ** ppClassNew; + Aig_Obj_t * pObj, * pRepr, * pPrev; + int i, k, nTotalObjs, nEntries, Entry; + // start the classes + p = Ssw_ClassesStart( pAig ); + // count the number of entries in the classes + nTotalObjs = 0; + for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ ) + nTotalObjs += pvClasses[i] ? Vec_IntSize(pvClasses[i]) : 0; + // allocate memory for classes + p->pMemClasses = ALLOC( Aig_Obj_t *, nTotalObjs ); + // create constant-1 class + if ( pvClasses[0] ) + Vec_IntForEachEntry( pvClasses[0], Entry, i ) + { + assert( (i == 0) == (Entry == 0) ); + if ( i == 0 ) + continue; + pObj = Aig_ManObj( pAig, Entry ); + Ssw_ObjSetConst1Cand( pAig, pObj ); + p->nCands1++; + } + // create classes + nEntries = 0; + for ( i = 1; i < Aig_ManObjNumMax(pAig); i++ ) + { + if ( pvClasses[i] == NULL ) + continue; + // get room for storing the class + ppClassNew = p->pMemClasses + nEntries; + nEntries += Vec_IntSize( pvClasses[i] ); + // store the nodes of the class + pPrev = pRepr = Aig_ManObj( pAig, Vec_IntEntry(pvClasses[i],0) ); + ppClassNew[0] = pRepr; + Vec_IntForEachEntryStart( pvClasses[i], Entry, k, 1 ) + { + pObj = Aig_ManObj( pAig, Entry ); + assert( pPrev->Id < pObj->Id ); + pPrev = pObj; + ppClassNew[k] = pObj; + Aig_ObjSetRepr( pAig, pObj, pRepr ); + } + // create new class + Ssw_ObjAddClass( p, pRepr, ppClassNew, Vec_IntSize(pvClasses[i]) ); + } + // prepare room for new classes + p->pMemClassesFree = p->pMemClasses + nEntries; + Ssw_ClassesCheck( p ); +// Ssw_ClassesPrint( p, 0 ); + return p; +} + /**Function************************************************************* Synopsis [Iteratively refines the classes after simulation.] diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index b03a248e..8e3ab01a 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -66,65 +66,24 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) { Aig_Man_t * pAigNew; - Ssw_Man_t * p; - int RetValue, nIter, clk, clkTotal = clock(); - // reset random numbers - Aig_ManRandom( 1 ); - - // consider the case of empty AIG - if ( Aig_ManNodeNum(pAig) == 0 ) - { - pPars->nIters = 0; - // Ntl_ManFinalize() needs the following to satisfy an assertion - Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) ); - return Aig_ManDupOrdered(pAig); - } - - // check and update parameters - assert( Aig_ManRegNum(pAig) > 0 ); - assert( pPars->nFramesK > 0 ); - if ( pPars->nFramesK > 1 ) - pPars->fSkipCheck = 0; - - // perform partitioning - if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig)) - || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) - return Ssw_SignalCorrespondencePart( pAig, pPars ); - - // start the choicing manager - p = Ssw_ManCreate( pAig, pPars ); - // compute candidate equivalence classes -// p->pPars->nConstrs = 1; - if ( p->pPars->nConstrs == 0 ) - { - // perform one round of seq simulation and generate candidate equivalence classes - p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); - p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); - Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); - } - else - { - // create trivial equivalence classes with all nodes being candidates for constant 1 - p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); - Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); - } - + int RetValue, nIter; + int clk, clkTotal = clock(); // get the starting stats p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses ); - p->nNodesBeg = Aig_ManNodeNum(pAig); - p->nRegsBeg = Aig_ManRegNum(pAig); + p->nNodesBeg = Aig_ManNodeNum(p->pAig); + p->nRegsBeg = Aig_ManRegNum(p->pAig); // refine classes using BMC - if ( pPars->fVerbose ) + if ( p->pPars->fVerbose ) { printf( "Before BMC: " ); Ssw_ClassesPrint( p->ppClasses, 0 ); } Ssw_ManSweepBmc( p ); Ssw_ManCleanup( p ); - if ( pPars->fVerbose ) + if ( p->pPars->fVerbose ) { printf( "After BMC: " ); Ssw_ClassesPrint( p->ppClasses, 0 ); @@ -134,7 +93,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) { clk = clock(); RetValue = Ssw_ManSweep( p ); - if ( pPars->fVerbose ) + if ( p->pPars->fVerbose ) { printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), @@ -150,12 +109,72 @@ clk = clock(); } p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; - pAigNew = Aig_ManDupRepr( pAig, 0 ); + pAigNew = Aig_ManDupRepr( p->pAig, 0 ); Aig_ManSeqCleanup( pAigNew ); // get the final stats p->nLitsEnd = Ssw_ClassesLitNum( p->ppClasses ); p->nNodesEnd = Aig_ManNodeNum(pAigNew); p->nRegsEnd = Aig_ManRegNum(pAigNew); + return pAigNew; +} + +/**Function************************************************************* + + Synopsis [Performs computation of signal correspondence with constraints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) +{ + Ssw_Pars_t Pars; + Aig_Man_t * pAigNew; + Ssw_Man_t * p; + // reset random numbers + Aig_ManRandom( 1 ); + // if parameters are not given, create them + if ( pPars == NULL ) + Ssw_ManSetDefaultParams( pPars = &Pars ); + // consider the case of empty AIG + if ( Aig_ManNodeNum(pAig) == 0 ) + { + pPars->nIters = 0; + // Ntl_ManFinalize() needs the following to satisfy an assertion + Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) ); + return Aig_ManDupOrdered(pAig); + } + // check and update parameters + assert( Aig_ManRegNum(pAig) > 0 ); + assert( pPars->nFramesK > 0 ); + if ( pPars->nFramesK > 1 ) + pPars->fSkipCheck = 0; + // perform partitioning + if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig)) + || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0) ) + return Ssw_SignalCorrespondencePart( pAig, pPars ); + // start the induction manager + p = Ssw_ManCreate( pAig, pPars ); + // compute candidate equivalence classes +// p->pPars->nConstrs = 1; + if ( p->pPars->nConstrs == 0 ) + { + // perform one round of seq simulation and generate candidate equivalence classes + p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose ); + p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); + } + else + { + // create trivial equivalence classes with all nodes being candidates for constant 1 + p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs ); + Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex ); + } + // perform refinement of classes + pAigNew = Ssw_SignalCorrespondenceRefine( p ); // cleanup Ssw_ManStop( p ); return pAigNew; diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index c9dd1958..6824e239 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -150,6 +150,7 @@ extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ); extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ); extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose ); extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs ); +extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses ); 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 ); @@ -158,6 +159,8 @@ extern int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj ); extern int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); /*=== sswCnf.c ===================================================*/ extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); +/*=== sswCore.c ===================================================*/ +extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ); /*=== sswMan.c ===================================================*/ extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); extern void Ssw_ManCleanup( Ssw_Man_t * p ); @@ -184,6 +187,7 @@ extern void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pC extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); + #ifdef __cplusplus } #endif diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c new file mode 100644 index 00000000..92d3d91d --- /dev/null +++ b/src/aig/ssw/sswPairs.c @@ -0,0 +1,437 @@ +/**CFile**************************************************************** + + FileName [sswPairs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Inductive prover with constraints.] + + Synopsis [Calls to the SAT solver.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 1, 2008.] + + Revision [$Id: sswPairs.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sswInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Reports the status of the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose ) +{ + Aig_Obj_t * pObj, * pChild; + int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; +// if ( p->pData ) +// return 0; + Saig_ManForEachPo( p, pObj, i ) + { + pChild = Aig_ObjChild0(pObj); + // check if the output is constant 0 + if ( pChild == Aig_ManConst0(p) ) + { + CountConst0++; + continue; + } + // check if the output is constant 1 + if ( pChild == Aig_ManConst1(p) ) + { + CountNonConst0++; + continue; + } + // check if the output is a primary input + if ( p->nRegs == 0 && Aig_ObjIsPi(Aig_Regular(pChild)) ) + { + CountNonConst0++; + continue; + } + // check if the output can be not constant 0 + if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) + { + CountNonConst0++; + continue; + } + CountUndecided++; + } + + if ( fVerbose ) + { + printf( "Miter has %d outputs. ", Saig_ManPoNum(p) ); + printf( "Const0 = %d. ", CountConst0 ); + printf( "NonConst0 = %d. ", CountNonConst0 ); + printf( "Undecided = %d. ", CountUndecided ); + printf( "\n" ); + } + + if ( CountNonConst0 ) + return 0; + if ( CountUndecided ) + return -1; + return 1; +} + +/**Function************************************************************* + + Synopsis [Transfer equivalent pairs to the miter.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2 ) +{ + Vec_Int_t * vIds; + Aig_Obj_t * pObj1, * pObj2; + Aig_Obj_t * pObj1m, * pObj2m; + int i; + vIds = Vec_IntAlloc( 2 * Vec_IntSize(vIds1) ); + for ( i = 0; i < Vec_IntSize(vIds1); i++ ) + { + pObj1 = Aig_ManObj( pAig1, Vec_IntEntry(vIds1, i) ); + pObj2 = Aig_ManObj( pAig2, Vec_IntEntry(vIds2, i) ); + pObj1m = Aig_Regular(pObj1->pData); + pObj2m = Aig_Regular(pObj2->pData); + assert( pObj1m && pObj2m ); + if ( pObj1m == pObj2m ) + continue; + if ( pObj1m->Id < pObj2m->Id ) + { + Vec_IntPush( vIds, pObj1m->Id ); + Vec_IntPush( vIds, pObj2m->Id ); + } + else + { + Vec_IntPush( vIds, pObj2m->Id ); + Vec_IntPush( vIds, pObj1m->Id ); + } + } + return vIds; +} + +/**Function************************************************************* + + Synopsis [Transform pairs into class representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumMax ) +{ + Vec_Int_t ** pvClasses; // vector of classes + int * pReprs; // mapping nodes into their representatives + int Entry, idObj, idRepr, idReprObj, idReprRepr, i; + // allocate data-structures + pvClasses = CALLOC( Vec_Int_t *, nObjNumMax ); + pReprs = ALLOC( int, nObjNumMax ); + for ( i = 0; i < nObjNumMax; i++ ) + pReprs[i] = -1; + // consider pairs + for ( i = 0; i < Vec_IntSize(vPairs); i += 2 ) + { + // get both objects + idRepr = Vec_IntEntry( vPairs, i ); + idObj = Vec_IntEntry( vPairs, i+1 ); + assert( idObj > 0 ); + assert( (pReprs[idRepr] == -1) || (pvClasses[pReprs[idRepr]] != NULL) ); + assert( (pReprs[idObj] == -1) || (pvClasses[pReprs[idObj] ] != NULL) ); + // get representatives of both objects + idReprRepr = pReprs[idRepr]; + idReprObj = pReprs[idObj]; + // check different situations + if ( idReprRepr == -1 && idReprObj == -1 ) + { // they do not have classes + // create a class + pvClasses[idRepr] = Vec_IntAlloc( 4 ); + Vec_IntPush( pvClasses[idRepr], idRepr ); + Vec_IntPush( pvClasses[idRepr], idObj ); + pReprs[ idRepr ] = idRepr; + pReprs[ idObj ] = idRepr; + } + else if ( idReprRepr >= 0 && idReprObj == -1 ) + { // representative has a class + // add iObj to the same class + Vec_IntPushUniqueOrder( pvClasses[idReprRepr], idObj ); + pReprs[ idObj ] = idReprRepr; + } + else if ( idReprRepr == -1 && idReprObj >= 0 ) + { // object has a class + assert( idReprObj != idRepr ); + if ( idReprObj < idRepr ) + { // add idRepr to the same class + Vec_IntPushUniqueOrder( pvClasses[idReprObj], idRepr ); + pReprs[ idRepr ] = idReprObj; + } + else // if ( idReprObj > idRepr ) + { // make idRepr new representative + Vec_IntPushFirst( pvClasses[idReprObj], idRepr ); + pvClasses[idRepr] = pvClasses[idReprObj]; + pvClasses[idReprObj] = NULL; + // set correct representatives of each node + Vec_IntForEachEntry( pvClasses[idRepr], Entry, i ) + pReprs[ Entry ] = idRepr; + } + } + else // if ( idReprRepr >= 0 && idReprObj >= 0 ) + { // both have classes + if ( idReprRepr == idReprObj ) + { // the classes are the same + // nothing to do + } + else + { // the classes are different + // find the repr of the new class + if ( idReprRepr < idReprObj ) + { + Vec_IntForEachEntry( pvClasses[idReprObj], Entry, i ) + { + Vec_IntPushUniqueOrder( pvClasses[idReprRepr], Entry ); + pReprs[ Entry ] = idReprRepr; + } + Vec_IntFree( pvClasses[idReprObj] ); + pvClasses[idReprObj] = NULL; + } + else // if ( idReprRepr > idReprObj ) + { + Vec_IntForEachEntry( pvClasses[idReprRepr], Entry, i ) + { + Vec_IntPushUniqueOrder( pvClasses[idReprObj], Entry ); + pReprs[ Entry ] = idReprObj; + } + Vec_IntFree( pvClasses[idReprRepr] ); + pvClasses[idReprRepr] = NULL; + } + } + } + } + free( pReprs ); + return pvClasses; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax ) +{ + int i; + for ( i = 0; i < nObjNumMax; i++ ) + if ( pvClasses[i] ) + Vec_IntFree( pvClasses[i] ); + free( pvClasses ); +} + +/**Function************************************************************* + + Synopsis [Performs signal correspondence for the miter of two AIGs with node pairs defined.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ) +{ + Ssw_Man_t * p; + Aig_Man_t * pAigNew, * pMiter; + Ssw_Pars_t Pars; + Vec_Int_t * vPairs; + Vec_Int_t ** pvClasses; + assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) ); + // create sequential miter + pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 ); + // transfer information to the miter + vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 ); + // create representation of the classes + pvClasses = Ssw_TransformPairsIntoTempClasses( vPairs, Aig_ManObjNumMax(pMiter) ); + 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_ClassesPreparePairs( pMiter, pvClasses ); + p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 ); + Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual ); + // perform refinement of classes + pAigNew = Ssw_SignalCorrespondenceRefine( p ); + // cleanup + Ssw_FreeTempClasses( pvClasses, Aig_ManObjNumMax(pMiter) ); + Ssw_ManStop( p ); + Aig_ManStop( pMiter ); + return pAigNew; +} + +/**Function************************************************************* + + Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ) +{ + Aig_Man_t * pAigNew, * pAigRes; + Ssw_Pars_t Pars, * pPars = &Pars; + Vec_Int_t * vIds1, * vIds2; + Aig_Obj_t * pObj, * pRepr; + int RetValue, i, clk = clock(); + Ssw_ManSetDefaultParams( pPars ); + pPars->fVerbose = 1; + pAigNew = Ssw_SignalCorrespondence( pAig, pPars ); + // record pairs of equivalent nodes + vIds1 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) ); + vIds2 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) ); + Aig_ManForEachObj( pAig, pObj, i ) + { + pRepr = Aig_Regular(pObj->pData); + if ( pRepr == NULL ) + continue; + if ( Aig_ManObj(pAigNew, pRepr->Id) == NULL ) + continue; +/* + if ( Aig_ObjIsNode(pObj) ) + printf( "n " ); + else if ( Saig_ObjIsPi(pAig, pObj) ) + printf( "pi " ); + else if ( Saig_ObjIsLo(pAig, pObj) ) + printf( "lo " ); +*/ + Vec_IntPush( vIds1, Aig_ObjId(pObj) ); + Vec_IntPush( vIds2, Aig_ObjId(pRepr) ); + } + printf( "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) ); + // try the new AIGs + pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig, pAigNew, vIds1, vIds2, pPars ); + Vec_IntFree( vIds1 ); + Vec_IntFree( vIds2 ); + // report the results + RetValue = Ssw_MiterStatus( pAigRes, 1 ); + if ( RetValue == 1 ) + printf( "Verification successful. " ); + else if ( RetValue == 0 ) + printf( "Verification failed with the counter-example. " ); + else + printf( "Verification UNDECIDED. Remaining registers %d (total %d). ", + Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) ); + PRT( "Time", clock() - clk ); + // cleanup + Aig_ManStop( pAigNew ); + return pAigRes; +} + +/**Function************************************************************* + + Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ) +{ + Aig_Man_t * pAigRes; + int RetValue, clk = clock(); + assert( vIds1 != NULL && vIds2 != NULL ); + // try the new AIGs + printf( "Performing specialized verification with node pairs.\n" ); + pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars ); + // 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(pAig1) + Aig_ManRegNum(pAig2) ); + PRT( "Time", clock() - clk ); + // cleanup + Aig_ManStop( pAigRes ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Runs inductive SEC for the miter of two AIGs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) +{ + Aig_Man_t * pAigRes, * pMiter; + int RetValue, clk = clock(); + // try the new AIGs + printf( "Performing general verification without node pairs.\n" ); + pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 ); + pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); + Aig_ManStop( pMiter ); + // 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(pAig1) + Aig_ManRegNum(pAig2) ); + PRT( "Time", clock() - clk ); + // cleanup + Aig_ManStop( pAigRes ); + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c index 3dccc08d..1cf4b81b 100644 --- a/src/aig/ssw/sswSweep.c +++ b/src/aig/ssw/sswSweep.c @@ -149,7 +149,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc ) Ssw_SmlSavePatternAigPhase( p, f ); } else - { + { // if the fraiged nodes are the same, return if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) return; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0db761c7..a0d26e3b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7684,7 +7684,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; -// Abc_Ntk_t * pNtkRes; + Abc_Ntk_t * pNtkRes = NULL; int c; int fBmc; int nFrames; @@ -7712,6 +7712,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose ); extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk ); // extern void Aig_ProcedureTest(); + extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); @@ -7912,14 +7914,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*//* - - if ( argc != globalUtilOptind + 1 ) - goto usage; - pFileName = argv[globalUtilOptind]; - Nwk_ManLutMergeGraphTest( pFileName ); */ -// Aig_ProcedureTest(); + + pNtkRes = Abc_NtkDarTestNtk( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index f1e5efb0..388fc5df 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2351,20 +2351,58 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio ***********************************************************************/ void Abc_NtkDarTest( Abc_Ntk_t * pNtk ) { - Aig_Man_t * pMan; + extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ); + + Aig_Man_t * pMan, * pTemp; assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return; - +/* Aig_ManSetRegNum( pMan, pMan->nRegs ); Aig_ManPrintStats( pMan ); Saig_ManDumpBlif( pMan, "_temp_.blif" ); Aig_ManStop( pMan ); pMan = Saig_ManReadBlif( "_temp_.blif" ); Aig_ManPrintStats( pMan ); +*/ + Aig_ManSetRegNum( pMan, pMan->nRegs ); + pTemp = Ssw_SignalCorrespondeceTestPairs( pMan ); + Aig_ManStop( pTemp ); + Aig_ManStop( pMan ); +} +/**Function************************************************************* + + Synopsis [Performs BDD-based reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) +{ + extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ); + + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + + Aig_ManSetRegNum( pMan, pMan->nRegs ); + pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan ); + Aig_ManStop( pTemp ); + + pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig->pName = Extra_UtilStrsav(pNtk->pName); + pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec); Aig_ManStop( pMan ); + return pNtkAig; } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3