Version abc80512

src/aig/aig/aig.h

@@ -478,6 +478,7 @@ extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepres( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepresDfs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
+extern Aig_Man_t *     Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );

src/aig/aig/aigDup.c

@@ -787,6 +787,50 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG with only one primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManRegNum(p) > 0 );
+    assert( iPoNum < Aig_ManPoNum(p)-Aig_ManRegNum(p) );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // set registers
+    pNew->nRegs    = p->nRegs;
+    pNew->nTruePis = p->nTruePis;
+    pNew->nTruePos = 1;
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create the PO
+    pObj = Aig_ManPo( p, iPoNum );
+    Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    // create register inputs with MUXes
+    Aig_ManForEachLiSeq( p, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/fra/fraLcr.c

@@ -542,7 +542,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
         if ( pnIter ) *pnIter = 0;
         return Aig_ManDupOrdered(pAig);
     }
-    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManRegNum(pAig) > 0 ); 
 
     // simulate the AIG 
 clk2 = clock();

src/aig/fra/fraSec.c

@@ -120,7 +120,7 @@ clk = clock();
     pNew = Aig_ManDupOrdered( pTemp = pNew );
 //    pNew = Aig_ManDupDfs( pTemp = pNew );
     Aig_ManStop( pTemp );
-    if ( TimeLimit )
+    if ( RetValue == -1 && TimeLimit )
     {
         TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
@@ -131,7 +131,7 @@ clk = clock();
             goto finish;
         }
     }
-    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter, TimeLeft );
+    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, fVeryVerbose, &nIter, TimeLeft );
     if ( pNew == NULL )
     {
         pNew = pTemp;
@@ -156,7 +156,7 @@ PRT( "Time", clock() - clk );
     }
     }
 
-    if ( TimeLimit )
+    if ( RetValue == -1 && TimeLimit )
     {
         TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
@@ -189,7 +189,7 @@ PRT( "Time", clock() - clk );
     if ( RetValue >= 0 )
         goto finish;
 
-    if ( TimeLimit )
+    if ( RetValue == -1 && TimeLimit )
     {
         TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
@@ -226,7 +226,7 @@ PRT( "Time", clock() - clk );
     if ( RetValue == -1 )
     for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
-        if ( TimeLimit )
+        if ( RetValue == -1 && TimeLimit )
         {
             TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
             TimeLeft = AIG_MAX( TimeLeft, 0.0 );
@@ -327,13 +327,13 @@ PRT( "Time", clock() - clkTotal );
 
     // try interplation
 clk = clock();
-    if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
+    if ( RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
     {
         extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
         int Depth;
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Saig_Interpolate( pNew, 10000, 0, 1, 0, &Depth );
+        RetValue = Saig_Interpolate( pNew, 5000, 0, 1, fVeryVerbose, &Depth );
         if ( fVerbose )
         {
         if ( RetValue == 1 )
@@ -357,6 +357,53 @@ PRT( "Time", clock() - clk );
         RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
     }
 
+    // try one-output at a time
+    if ( RetValue == -1 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) > 1 )
+    {
+        Aig_Man_t * pNew2;
+        int i, TimeLimit2, RetValue2, fOneUnsolved = 0, iCount, Counter = 0;
+        // count unsolved outputs
+        for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
+            if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
+                Counter++;
+        printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n", 
+            Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
+        iCount = 0;
+        for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
+        {
+            // get the remaining time for this output
+            if ( TimeLimit )
+            {
+                TimeLeft = (float)TimeLimit - ((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC));
+                TimeLeft = AIG_MAX( TimeLeft, 0.0 );
+                if ( TimeLeft == 0.0 )
+                {
+                    printf( "Runtime limit exceeded.\n" );
+                    goto finish;
+                }
+                TimeLimit2 = 1 + (int)TimeLeft;
+            }
+            else
+                TimeLimit2 = 0;
+            if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
+                continue;
+            iCount++;
+            printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
+            pNew2 = Aig_ManDupOneOutput( pNew, i );
+            RetValue2 = Fra_FraigSec( pNew2, nFramesMax, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose, TimeLimit2 );
+            Aig_ManStop( pNew2 );
+            if ( RetValue2 == 0 )
+                goto finish;
+            if ( RetValue2 == -1 )
+                fOneUnsolved = 1;
+        }
+        if ( fOneUnsolved )
+            RetValue = -1;
+        else
+            RetValue = 1;
+        printf( "*** Finished running separate outputs of the miter.\n" );
+    }
+
 finish:
     // report the miter
     if ( RetValue == 1 )

src/aig/saig/saig.h

@@ -76,7 +76,7 @@ static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 ////////////////////////////////////////////////////////////////////////
 
 /*=== saigBmc.c ==========================================================*/
-extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
+extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
 /*=== saigInter.c ==========================================================*/

src/aig/saig/saigBmc.c

@@ -82,6 +82,90 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of internal nodes that are not counted yet.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( !Aig_ObjIsNode(pObj) )
+        return 0;
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return 0;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + 
+        Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for BMC.]
+
+  Description [The resulting manager is combinational. The primary inputs
+  corresponding to register outputs are ordered first. POs correspond to 
+  the property outputs in each time-frame.
+  The unrolling is stopped as soon as the number of nodes in the frames
+  exceeds the given maximum size.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
+    int i, f, Counter = 0;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    pFrames = Aig_ManStart( nSizeMax );
+    Aig_ManIncrementTravId( pFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ManConst0( pFrames );
+    // add timeframes
+    Counter = 0;
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+            Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
+            if ( Counter >= nSizeMax )
+            {
+                Aig_ManCleanup( pFrames );
+                return pFrames;
+            }
+        }
+        if ( f == nFrames - 1 )
+            break;
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs BMC for the given AIG.]
 
   Description []
@@ -91,7 +175,7 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
+int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
 {
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
@@ -101,7 +185,13 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fRewri
     *piFrame = -1;
     // derive the timeframes
     clk = clock();
-    pFrames = Saig_ManFramesBmc( pAig, nFrames );
+    if ( nSizeMax > 0 )
+    {
+        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
+        nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
+    }
+    else
+        pFrames = Saig_ManFramesBmc( pAig, nFrames );
     if ( fVerbose )
     {
         printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 

src/aig/saig/saigInter.c

@@ -566,6 +566,14 @@ p->timeCnf += clock() - clk;
         // iterate the interpolation procedure
         for ( i = 0; ; i++ )
         {
+            if ( p->nFrames + i >= 100 )
+            {
+                if ( fVerbose )
+                    printf( "Reached limit (%d) on the number of timeframes.\n", 100 );
+                p->timeTotal = clock() - clkTotal;
+                Saig_ManagerFree( p );
+                return -1;
+            }
             // perform interplation
             clk = clock();
             RetValue = Saig_PerformOneStep( p );

src/base/abci/abc.c

@@ -12713,6 +12713,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fWriteImps = 0;
     pPars->fUse1Hot   = 0;
     pPars->fVerbose   = 0;
+    pPars->TimeLimit  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
     {
@@ -14657,25 +14658,27 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int nFrames;
+    int nSizeMax;
     int nBTLimit;
     int fRewrite;
     int fNewAlgo;
     int fVerbose;
 
-    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose );
+    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames  = 10;
+    nFrames  = 20;
+    nSizeMax = 100000;
     nBTLimit = 10000;
     fRewrite = 0;
     fNewAlgo = 1;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCravh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FNCravh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14690,6 +14693,17 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames < 0 ) 
                 goto usage;
             break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nSizeMax < 0 ) 
+                goto usage;
+            break;
         case 'C':
             if ( globalUtilOptind >= argc )
             {
@@ -14731,13 +14745,14 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Does not work for combinational networks.\n" );
         return 0;
     }
-    Abc_NtkDarBmc( pNtk, nFrames, nBTLimit, fRewrite, fNewAlgo, fVerbose );
+    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nBTLimit, fRewrite, fNewAlgo, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: bmc [-F num] [-C num] [-ravh]\n" );
+    fprintf( pErr, "usage: bmc [-FNC num] [-ravh]\n" );
     fprintf( pErr, "\t         perform bounded model checking\n" );
     fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-a     : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
@@ -17069,6 +17084,7 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fWriteImps = 0;
     pPars->fUse1Hot   = 0;
     pPars->fVerbose   = 0;
+    pPars->TimeLimit  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
     {

src/base/abci/abcDar.c

@@ -1208,7 +1208,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose )
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue = -1, clk = clock();
@@ -1226,7 +1226,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in
     if ( fNewAlgo )
     {
         int iFrame;
-        RetValue = Saig_ManBmcSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose, &iFrame );
+        RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
         if ( RetValue == 1 )
             printf( "No output was asserted in %d frames. ", nFrames );
@@ -1337,7 +1337,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int fTryComb, int fTryBmc, int nFrames, i
     }
     if ( fTryBmc )
     {
-        RetValue = Abc_NtkDarBmc( pNtk, 10, 1000, 0, 1, 0 );
+        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, 1000, 0, 1, 0 );
         if ( RetValue == 0 )
             return RetValue;
     }

src/base/main/main.c

@@ -217,7 +217,7 @@ int main( int argc, char * argv[] )
                 break;
         }
     }
-    
+     
     // if the memory should be freed, quit packages
     if ( fStatus < 0 ) 
     {