Version abc80721

1 files changed, 246 insertions, 18 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 264b1df4..b8a9cefe 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -200,6 +200,7 @@ static int Abc_CommandSec            ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandDSec           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSat            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDSat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPSat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDebug          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -218,6 +219,7 @@ static int Abc_CommandAbc8Write      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8WriteLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8ReadLut    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8PrintLut   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Check      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc8Ps         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Pfan       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -458,6 +460,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "dprove",        Abc_CommandDProve,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsat",          Abc_CommandDSat,             0 );
+    Cmd_CommandAdd( pAbc, "Verification", "psat",          Abc_CommandPSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
@@ -473,6 +476,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*wlogic",       Abc_CommandAbc8WriteLogic,   0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*rlut",         Abc_CommandAbc8ReadLut,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*plut",         Abc_CommandAbc8PrintLut,     0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*check",        Abc_CommandAbc8Check,        0 );
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*ps",           Abc_CommandAbc8Ps,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*pfan",         Abc_CommandAbc8Pfan,         0 );
@@ -6357,7 +6361,7 @@ int Abc_CommandTopAnd( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: topand [-h]\n" );
-    fprintf( pErr, "\t         AND-decomposition of single-output combinational miter\n" );
+    fprintf( pErr, "\t         performs AND-decomposition of single-output combinational miter\n" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\tname   : the node name\n");
     return 1;
@@ -14196,7 +14200,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPartition;
     int fMiter;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
     extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14850,14 +14854,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int RetValue;
-    int fFlipBits;
+    int fAlignPol;
     int fAndOuts;
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
     int clk;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14865,13 +14869,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fFlipBits  = 0;
+    fAlignPol  = 0;
     fAndOuts   = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIfavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14897,8 +14901,8 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nInsLimit < 0 ) 
                 goto usage;
             break;
-        case 'f':
-            fFlipBits ^= 1;
+        case 'p':
+            fAlignPol ^= 1;
             break;
         case 'a':
             fAndOuts ^= 1;
@@ -14937,7 +14941,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     clk = clock();
-    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fFlipBits, fAndOuts, fVerbose );
+    RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fAlignPol, fAndOuts, fVerbose );
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
@@ -14970,13 +14974,177 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dsat [-C num] [-I num] [-favh]\n" );
+    fprintf( pErr, "usage: dsat [-C num] [-I num] [-pavh]\n" );
     fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
-    fprintf( pErr, "\t-f     : flip polarity of SAT variables [default = %s]\n", fFlipBits? "yes": "no" );  
-    fprintf( pErr, "\t-a     : constrain each output of multi-output miter [default = %s]\n", fAndOuts? "yes": "no" );  
+    fprintf( pErr, "\t-p     : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );  
+    fprintf( pErr, "\t-a     : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int RetValue;
+    int c, clk;
+    int nAlgo;
+    int nPartSize;
+    int nConfPart;
+    int nConfTotal;
+    int fAlignPol;
+    int fSynthesize;
+    int fVerbose;
+
+    extern int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nAlgo       =        0;
+    nPartSize   =    10000;
+    nConfPart   =        0;
+    nConfTotal  =  1000000;
+    fAlignPol   =        1;
+    fSynthesize =        0;
+    fVerbose    =        1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "APCpsvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-A\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nAlgo = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nAlgo < 0 ) 
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPartSize < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfTotal = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfTotal < 0 ) 
+                goto usage;
+            break;
+        case 'p':
+            fAlignPol ^= 1;
+            break;
+        case 's':
+            fSynthesize ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+    {
+        fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
+        return 0;
+    } 
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+
+    clk = clock();
+    RetValue = Abc_NtkPartitionedSat( pNtk, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose );
+    // verify that the pattern is correct
+    if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
+    {
+        //int i;
+        //Abc_Obj_t * pObj;
+        int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
+        if ( pSimInfo[0] != 1 )
+            printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
+        free( pSimInfo );
+        /*
+        // print model
+        Abc_NtkForEachPi( pNtk, pObj, i )
+        {
+            printf( "%d", (int)(pNtk->pModel[i] > 0) );
+            if ( i == 70 )
+                break;
+        }
+        printf( "\n" );
+        */
+    }
+
+    if ( RetValue == -1 )
+        printf( "UNDECIDED      " );
+    else if ( RetValue == 0 )
+        printf( "SATISFIABLE    " );
+    else
+        printf( "UNSATISFIABLE  " );
+    //printf( "\n" );
+    PRT( "Time", clock() - clk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: psat [-APC num] [-psvh]\n" );
+    fprintf( pErr, "\t         solves the combinational miter using partitioning\n" );
+    fprintf( pErr, "\t         (derives CNF from the current network and leave it unchanged)\n" );
+    fprintf( pErr, "\t         for multi-output miters, tries to prove that the AND of POs is always 0\n" );
+    fprintf( pErr, "\t         (if POs should be ORed instead of ANDed, use command \"orpos\")\n" );
+    fprintf( pErr, "\t-A num : partitioning algorithm [default = %d]\n", nAlgo );
+    fprintf( pErr, "\t         0 : no partitioning\n" );
+    fprintf( pErr, "\t         1 : partitioning by level\n" );
+    fprintf( pErr, "\t         2 : DFS post-order\n" );
+    fprintf( pErr, "\t         3 : DFS pre-order\n" );
+    fprintf( pErr, "\t         4 : bit-slicing\n" );
+    fprintf( pErr, "\t         partitions are ordered by level (high level first)\n" );
+    fprintf( pErr, "\t-P num : limit on the partition size [default = %d]\n", nPartSize );
+    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfTotal );
+    fprintf( pErr, "\t-p     : align polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );  
+    fprintf( pErr, "\t-s     : apply logic synthesis to each partition [default = %s]\n", fSynthesize? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -15347,11 +15515,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fRewrite;
     int fTransLoop;
     int fUsePudlak;
+    int fUseOther;
+    int fUseMiniSat;
     int fCheckInd;
     int fCheckKstep;
     int fVerbose;
 
-    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fCheckKstep, int fVerbose );
+    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -15363,11 +15533,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     fRewrite   = 0;
     fTransLoop = 1;
     fUsePudlak = 0;
+    fUseOther  = 0;
+    fUseMiniSat= 0;
     fCheckInd  = 0;
     fCheckKstep= 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpikvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpomikvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15402,6 +15574,12 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fUsePudlak ^= 1;
             break;
+        case 'o':
+            fUseOther ^= 1;
+            break;
+        case 'm':
+            fUseMiniSat ^= 1;
+            break;
         case 'i':
             fCheckInd ^= 1;
             break;
@@ -15437,18 +15615,19 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
         return 0;
     }
-    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fCheckKstep, fVerbose );
+    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: int [-CF num] [-rtpikvh]\n" );
+    fprintf( pErr, "usage: int [-CF num] [-rtpomikvh]\n" );
     fprintf( pErr, "\t         uses interpolation to prove the property\n" );
     fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
     fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-t     : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
-//    fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
-    fprintf( pErr, "\t-p     : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-o     : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", fUseOther? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUseMiniSat? "yes": "no" );
     fprintf( pErr, "\t-i     : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
     fprintf( pErr, "\t-k     : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -16364,6 +16543,55 @@ usage:
     return 1;       /* error exit */
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Command procedure to read LUT libraries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc8Check( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    int c;
+    extern int Nwk_ManCheck( void * p );
+
+    // set the defaults
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind )
+    {
+        goto usage;
+    }
+
+    // set the new network
+    if ( pAbc->pAbc8Nwk == NULL )
+        printf( "Abc_CommandAbc8Check(): There is no mapped network.\n" );
+    else
+        Nwk_ManCheck( pAbc->pAbc8Nwk );
+    return 0;
+
+usage:
+    fprintf( stdout, "\nusage: *check [-h]\n");
+    fprintf( stdout, "\t          checks if the current mapped network has duplicated fanins\n" );  
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    return 1;       /* error exit */
+}
+
 
 /**Function*************************************************************