Version abc50915

5 files changed, 105 insertions, 20 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4745273e..16be21fd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -86,6 +86,7 @@ static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandPga          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -163,6 +164,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
     Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
@@ -949,9 +951,9 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsStrash(pNtk) )
+    if ( !Abc_NtkHasAig(pNtk) )
     {
-        fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\").\n" );
+        fprintf( pErr, "Visualizing AIG can only be done for AIGs (run \"strash\" or \"seq\").\n" );
         return 1;
     }
     Abc_NtkShowAig( pNtk );
@@ -3906,7 +3908,6 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-    extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3931,8 +3932,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    printf( "This command is not yet implemented.\n" );
-    return 0;
+//    printf( "This command is not yet implemented.\n" );
+//    return 0;
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
@@ -3959,7 +3960,81 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: seq [-h]\n" );
-    fprintf( pErr, "\t        converts AIG into sequential AIG (while sweeping latches)\n" );
+    fprintf( pErr, "\t        converts AIG into sequential AIG\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int fShare;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fShare = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 's':
+            fShare ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
+        return 1;
+    }
+
+    // share the latches on the fanout edges
+    if ( fShare )
+        Abc_NtkSeqShareFanouts(pNtk);
+
+    // get the new network
+    pNtkRes = Abc_NtkSeqToLogicSop( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Converting sequential AIG into an SOP logic network has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: unseq [-sh]\n" );
+    fprintf( pErr, "\t        converts sequential AIG into an SOP logic network\n" );
+    fprintf( pErr, "\t-s    : toggle sharing latches [default = %s]\n", fShare? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -3991,7 +4066,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fForward  = 0;
+    fForward  = 1;
     fBackward = 0;
     fInitial  = 0;
     util_getopt_reset();
@@ -4021,10 +4096,6 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    printf( "This command is not yet implemented.\n" );
-    return 0;
-
-
     if ( !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pErr, "Works only for sequential AIG.\n" );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 20f41c56..01317d1d 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -501,7 +501,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
                 pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) );
         }
         if ( Counter )
-            printf( "Warning: %d uninitialized latches are replaced by free variables.\n", Counter );
+            printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
     }
     
     // create the timeframes
@@ -521,12 +521,18 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
         Abc_NtkForEachLatch( pNtk, pLatch, i )
         {
             pLatchNew = Abc_NtkLatch(pNtkFrames, i);
-            Abc_ObjAddFanin( pLatchNew, Abc_ObjFanin0(pLatch)->pCopy );
+            Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
             Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
             Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
             Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
         }
     }
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pNext = NULL;
+
+    // remove dangling nodes
+    Abc_AigCleanup( pNtkFrames->pManFunc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkFrames ) )
     {
@@ -586,7 +592,9 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_
     }
     // transfer the implementation of the latch drivers to the latches
     Abc_NtkForEachLatch( pNtk, pLatch, i )
-        pLatch->pCopy = Abc_ObjChild0Copy(pLatch);
+        pLatch->pNext = Abc_ObjChild0Copy(pLatch);
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pCopy = pLatch->pNext;
 }
 
 
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 3d9534c8..421e3059 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -144,6 +144,8 @@ pManRef->timeTotal = clock() - clkStart;
     Abc_NtkManRefStop( pManRef );
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
+    Abc_AigRehash( pNtk->pManFunc );
+//    Abc_AigCheckFaninOrder( pNtk->pManFunc );
     // fix the levels
     if ( fUpdateLevel )
         Abc_NtkStopReverseLevels( pNtk );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 91a99a57..b70d30e6 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -115,6 +115,8 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     pNtk->pManCut = NULL;
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
+    Abc_AigRehash( pNtk->pManFunc );
+//    Abc_AigCheckFaninOrder( pNtk->pManFunc );
     // fix the levels
     if ( fUpdateLevel )
         Abc_NtkStopReverseLevels( pNtk );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index b335086f..e5bc2547 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -52,7 +52,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
     if ( Abc_NtkPoNum(pNtk) > 1 )
-        fprintf( stdout, "Warning: The miter has more than 1 output. SAT will try to prove all of them.\n" );
+        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
 
     // load clauses into the solver
     clk = clock();
@@ -65,11 +65,11 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
     status = solver_simplify(pSat);
 //    printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
-    if ( status == l_False )
+    if ( status == 0 )
     {
         solver_delete( pSat );
-        printf( "The problem is UNSATISFIABLE after simplification.\n" );
-        return 0;
+//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+        return -1;
     }
 
     // solve the miter
@@ -146,8 +146,10 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
         Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
     }
     // add clauses for each PO
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        Abc_NodeAddClausesTop( pSat, pNode, vVars );
+//    Abc_NtkForEachPo( pNtk, pNode, i )
+//        Abc_NodeAddClausesTop( pSat, pNode, vVars );
+
+    Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars );
 
     // delete
     Vec_StrFree( vCube );