Version abc80228

3 files changed, 127 insertions, 83 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 2ee84f39..cc64b024 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -50,6 +50,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Fra_Par_t_   Fra_Par_t;
+typedef struct Fra_Ssw_t_   Fra_Ssw_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Sml_t_   Fra_Sml_t;
@@ -86,6 +87,25 @@ struct Fra_Par_t_
     int              fDontShowBar;      // does not show progressbar during fraiging
 };
 
+// seq SAT sweeping parametesr
+struct Fra_Ssw_t_
+{
+    int              nPartSize;         // size of the partition
+    int              nOverSize;         // size of the overlap between partitions
+    int              nFramesP;          // number of frames in the prefix
+    int              nFramesK;          // number of frames for induction (1=simple) 
+    int              nMaxImps;          // max implications to consider
+    int              nMaxLevs;          // max levels to consider
+    int              fUseImps;          // use implications  
+    int              fRewrite;          // enable rewriting of the specualatively reduced model
+    int              fFraiging;         // enable comb SAT sweeping as preprocessing 
+    int              fLatchCorr;        // perform register correspondence
+    int              fWriteImps;        // write implications into a file
+    int              fUse1Hot;          // use one-hotness constraints
+    int              fVerbose;          // enable verbose output 
+    int              nIters;            // the number of iterations performed
+};
+
 // FRAIG equivalence classes
 struct Fra_Cla_t_
 {
@@ -287,7 +307,7 @@ extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
 extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
 extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
 /*=== fraIndVer.c =====================================================*/
 extern int                 Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
 /*=== fraLcr.c ========================================================*/
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ea17706c..0715524e 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -234,7 +234,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs choicing of the AIG.]
+  Synopsis    [Performs partitioned sequential SAT sweepingG.]
 
   Description []
                
@@ -243,7 +243,77 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+{
+    int fPrintParts = 0;
+    char Buffer[100];
+    Aig_Man_t * pTemp, * pNew;
+    Vec_Ptr_t * vResult;
+    Vec_Int_t * vPart;
+    int * pMapBack;
+    int i, nCountPis, nCountRegs;
+    int nClasses, nPartSize, fVerbose;
+
+    // save parameters
+    nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
+    fVerbose  = pPars->fVerbose;  pPars->fVerbose = 0;
+    // generate partitions
+    vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
+//    vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); 
+//    vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
+    if ( fPrintParts )
+    {
+        // print partitions
+        printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+        Vec_PtrForEachEntry( vResult, vPart, i )
+        {
+            sprintf( Buffer, "part%03d.aig", i );
+            pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
+            Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
+            printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+            Aig_ManStop( pTemp );
+        }
+    }
+
+    // perform SSW with partitions
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    Vec_PtrForEachEntry( vResult, vPart, i )
+    {
+        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+        // run SSW
+        pNew = Fra_FraigInduction( pTemp, pPars );
+        nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
+        if ( fVerbose )
+            printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+        Aig_ManStop( pNew );
+        Aig_ManStop( pTemp );
+        free( pMapBack );
+    }
+    // remap the AIG
+    pNew = Aig_ManDupRepr( pAig, 0 );
+    Aig_ManSeqCleanup( pNew );
+//    Aig_ManPrintStats( pAig );
+//    Aig_ManPrintStats( pNew );
+    Vec_VecFree( (Vec_Vec_t *)vResult );
+    pPars->nPartSize = nPartSize;
+    pPars->fVerbose = fVerbose;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential SAT sweeping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -263,13 +333,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
-        if ( pnIter ) *pnIter = 0;
+        pParams->nIters = 0;
         return Aig_ManDup(pManAig, 1);
     }
     assert( Aig_ManLatchNum(pManAig) == 0 );
     assert( Aig_ManRegNum(pManAig) > 0 );
-    assert( nFramesK > 0 );
+    assert( pParams->nFramesK > 0 );
 //Aig_ManShow( pManAig, 0, NULL );
+
+    if ( pParams->fWriteImps && pParams->nPartSize > 0 )
+    {
+        pParams->nPartSize = 0;
+        printf( "Partitioning was disabled to allow implication writing.\n" );
+    }
+    // perform partitioning
+    if ( pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig) )
+        return Fra_FraigInductionPart( pManAig, pParams );
  
     nNodesBeg = Aig_ManNodeNum(pManAig);
     nRegsBeg  = Aig_ManRegNum(pManAig);
@@ -279,16 +358,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
-    pPars->nFramesP   = nFramesP;
-    pPars->nFramesK   = nFramesK;
-    pPars->nMaxImps   = nMaxImps;
-    pPars->nMaxLevs   = nMaxLevs;
-    pPars->fVerbose   = fVerbose;
-    pPars->fRewrite   = fRewrite;
-    pPars->fLatchCorr = fLatchCorr;
-    pPars->fUseImps   = fUseImps;
-    pPars->fWriteImps = fWriteImps;
-    pPars->fUse1Hot   = fUse1Hot;
+    pPars->nFramesP   = pParams->nFramesP;
+    pPars->nFramesK   = pParams->nFramesK;
+    pPars->nMaxImps   = pParams->nMaxImps;
+    pPars->nMaxLevs   = pParams->nMaxLevs;
+    pPars->fVerbose   = pParams->fVerbose;
+    pPars->fRewrite   = pParams->fRewrite;
+    pPars->fLatchCorr = pParams->fLatchCorr;
+    pPars->fUseImps   = pParams->fUseImps;
+    pPars->fWriteImps = pParams->fWriteImps;
+    pPars->fUse1Hot   = pParams->fUse1Hot;
 
     assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
     assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
@@ -311,10 +390,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
         // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
         // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // refine the classes with more simulation rounds
-if ( fVerbose )
+if ( pPars->fVerbose )
 printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
         p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );  
-if ( fVerbose ) 
+if ( pPars->fVerbose ) 
 {
 PRT( "Time", clock() - clk );
 }
@@ -408,7 +487,7 @@ p->timeTrav += clock() - clk2;
             Fra_OneHotAssume( p, p->vOneHots );
 
         // report the intermediate results
-        if ( fVerbose )
+        if ( pPars->fVerbose )
         {
             printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  ", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
@@ -428,7 +507,7 @@ clk2 = clock();
         if ( p->pPars->fUse1Hot )
             Fra_OneHotCheck( p, p->vOneHots );
         Fra_FraigSweep( p );
-        if ( fVerbose )
+        if ( pPars->fVerbose )
         {
 //            PRT( "t", clock() - clk2 ); 
         } 
@@ -508,7 +587,7 @@ p->timeTotal = clock() - clk;
 //    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
 //        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
 //            printf( "Proved output constant 0.\n" );
-    if ( pnIter ) *pnIter = nIter;
+    pParams->nIters = nIter;
     return pManAigNew;
 }
 
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index a43d83b1..75d297cf 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,73 +40,17 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
-{
-    Aig_Man_t * pNew;
-    int nFrames, RetValue, nIter, clk, clkTotal = clock();
-    int fLatchCorr = 0;
-    if ( nFramesFix )
-    {
-        nFrames = nFramesFix;
-        // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
-    }
-    else
-    {
-        // perform seq sweeping while increasing the number of frames
-        for ( nFrames = 1; ; nFrames++ )
-        {
-clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
-            RetValue = Fra_FraigMiterStatus( pNew );
-            if ( fVerbose )
-            {
-                printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
-                if ( RetValue == 1 )
-                    printf( "UNSAT     " );
-                else
-                    printf( "UNDECIDED " );
-PRT( "Time", clock() - clk );
-            }
-            if ( RetValue != -1 )
-                break;
-            Aig_ManStop( pNew );
-        }
-    }
-
-    // get the miter status
-    RetValue = Fra_FraigMiterStatus( pNew );
-    Aig_ManStop( pNew );
-
-    // report the miter
-    if ( RetValue == 1 )
-        printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-    else if ( RetValue == 0 )
-        printf( "Networks are NOT EQUIVALENT. " );
-    else
-        printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-PRT( "Time", clock() - clkTotal );
-    return RetValue;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
 {
+    Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
+    // prepare parameters
+    memset( pPars, 0, sizeof(Fra_Ssw_t) );
+    pPars->fLatchCorr  = fLatchCorr;
+    pPars->fVerbose = fVeryVerbose;
 
     pNew = Aig_ManDup( p, 1 );
     if ( fVerbose )
@@ -185,13 +129,14 @@ PRT( "Time", clock() - clk );
     for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
 clk = clock();
-        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
+        pPars->nFramesK = nFrames;
+        pNew = Fra_FraigInduction( pTemp = pNew, pPars );
         Aig_ManStop( pTemp );
         RetValue = Fra_FraigMiterStatus( pNew );
         if ( fVerbose )
         { 
             printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
-                nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+                nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
         }
         if ( RetValue != -1 )