Version abc80915

abc.dsp

@@ -3446,6 +3446,10 @@ SOURCE=.\src\aig\ssw\sswMan.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ssw\sswPairs.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ssw\sswPart.c
 # End Source File
 # Begin Source File

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 );

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

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 \

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
 }

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 );
@@ -646,6 +647,72 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
 
 /**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.]
 
   Description [Returns the number of refinements performed.]

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;

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

src/aig/ssw/sswPairs.c

+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+

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:

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;
 }
 
 ////////////////////////////////////////////////////////////////////////