Version abc61007

1 files changed, 209 insertions, 32 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2427146c..b25ca2f7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -117,6 +117,7 @@ static int Abc_CommandSuperChoice    ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFpga           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFpgaFast       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPga            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandScut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -246,6 +247,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "SC mapping",   "scl",           Abc_CommandSuperChoiceLut,   1 );
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
+    Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga",         Abc_CommandFpgaFast,         1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
     Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
@@ -4007,6 +4009,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
         goto usage;
     }
 
+    pNodeCo = NULL;
     if ( argc == globalUtilOptind + 1 )
     {
         pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] );
@@ -4827,7 +4830,7 @@ usage:
 int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkRes;//, * pNtkTemp;
     int c;
     int nLutMax;
     int nPlaMax;
@@ -4844,13 +4847,13 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLutMax    = 6;
+    nLutMax    = 8;
     nPlaMax    = 128;
     RankCost   = 96000;
     fFastMode  = 1;
     fRewriting = 0;
     fSynthesis = 0;
-    fVerbose   = 1;
+    fVerbose   = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfrsvh" ) ) != EOF )
     {
@@ -4927,8 +4930,17 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
     // run the command
 //    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
-    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
-//    pNtkRes = NULL;
+/*
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtkRes = Abc_NtkPlayer( pNtkTemp, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+        Abc_NtkDelete( pNtkTemp );
+    }
+    else
+        pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
+*/
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5537,10 +5549,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fUpdateLevel, fVerbose;
+    int c, fProve, fVerbose;
     int nConfLimit;
 
-    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5548,10 +5560,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nConfLimit   = 100;   
-    fUpdateLevel = 1;
+    fProve       = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Clzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5566,8 +5578,8 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfLimit < 0 ) 
                 goto usage;
             break;
-        case 'l':
-            fUpdateLevel ^= 1;
+        case 'p':
+            fProve ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -5589,7 +5601,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fVerbose );
+    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fProve, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5600,10 +5612,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ifraig [-C num] [-vh]\n" );
+    fprintf( pErr, "usage: ifraig [-C num] [-pvh]\n" );
     fprintf( pErr, "\t         performs fraiging using a new method\n" );
-    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
-//    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+    fprintf( pErr, "\t-p     : toggle proving miter outputs [default = %s]\n", fProve? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -5622,29 +5634,31 @@ usage:
 ***********************************************************************/
 int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Prove_Params_t Params, * pParams = &Params;
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fUpdateLevel, fVerbose;
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    int c, clk, RetValue;
 
-    extern Abc_Ntk_t * Abc_NtkIvyProve( Abc_Ntk_t * pNtk );
+    extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fUpdateLevel = 1;
-    fVerbose     = 0;
+    Prove_ParamsSetDefault( pParams );
+    pParams->fUseRewriting = 1;
+    pParams->fVerbose      = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'l':
-            fUpdateLevel ^= 1;
+        case 'r':
+            pParams->fUseRewriting ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pParams->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -5663,21 +5677,43 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyProve( pNtk );
-    if ( pNtkRes == NULL )
+
+    clk = clock();
+
+    if ( Abc_NtkIsStrash(pNtk) )
+        pNtkTemp = Abc_NtkDup( pNtk );
+    else
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
+
+    RetValue = Abc_NtkIvyProve( &pNtkTemp, pParams );
+
+    // verify that the pattern is correct
+    if ( RetValue == 0 )
     {
-        fprintf( pErr, "Command has failed.\n" );
-        return 0;
+        int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel );
+        if ( pSimInfo[0] != 1 )
+            printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+        free( pSimInfo );
     }
+ 
+    if ( RetValue == -1 ) 
+        printf( "UNDECIDED      " );
+    else if ( RetValue == 0 )
+        printf( "SATISFIABLE    " );
+    else
+        printf( "UNSATISFIABLE  " );
+    //printf( "\n" );
+
+    PRT( "Time", clock() - clk );
     // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: iprove [-h]\n" );
+    fprintf( pErr, "usage: iprove [-rvh]\n" );
     fprintf( pErr, "\t         performs CEC using a new method\n" );
-//    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
-//    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", pParams->fUseRewriting? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -6932,6 +6968,147 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandFpgaFast( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    char Buffer[100];
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int fRecovery;
+    int fVerbose;
+    int nLutSize;
+    float DelayTarget;
+
+    extern Abc_Ntk_t * Abc_NtkFpgaFast( Abc_Ntk_t * pNtk, int nLutSize, int fRecovery, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fRecovery   = 1;
+    fVerbose    = 0;
+    DelayTarget =-1;
+    nLutSize    = 8;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "avhDK" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'a':
+            fRecovery ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            DelayTarget = (float)atof(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( DelayTarget <= 0.0 ) 
+                goto usage;
+            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Cannot FPGA map a sequential AIG.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        // strash and balance the network
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+        pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 );
+        Abc_NtkDelete( pNtkRes );
+        if ( pNtk == NULL )
+        {
+            fprintf( pErr, "Balancing before FPGA mapping has failed.\n" );
+            return 1;
+        }
+        fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" );
+        // get the new network
+        pNtkRes = Abc_NtkFpgaFast( pNtk, nLutSize, fRecovery, fVerbose );
+        if ( pNtkRes == NULL )
+        {
+            Abc_NtkDelete( pNtk );
+            fprintf( pErr, "FPGA mapping has failed.\n" );
+            return 1;
+        }
+        Abc_NtkDelete( pNtk );
+    }
+    else
+    {
+        // get the new network
+        pNtkRes = Abc_NtkFpgaFast( pNtk, nLutSize, fRecovery, fVerbose );
+        if ( pNtkRes == NULL )
+        {
+            fprintf( pErr, "FPGA mapping has failed.\n" );
+            return 1;
+        }
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    if ( DelayTarget == -1 ) 
+        sprintf( Buffer, "not used" );
+    else
+        sprintf( Buffer, "%.2f", DelayTarget );
+    fprintf( pErr, "usage: ffpga [-K num] [-avh]\n" );
+    fprintf( pErr, "\t           performs fast FPGA mapping of the current network\n" );
+    fprintf( pErr, "\t-a       : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
+//    fprintf( pErr, "\t-D float : sets the required time for the mapping [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < 32) [default = %d]\n", nLutSize );
+    fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h       : prints the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;