Version abc70624

3 files changed, 91 insertions, 11 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d5321e6d..36311596 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26,6 +26,7 @@
 #include "fpga.h"
 #include "if.h"
 #include "res.h"
+//#include "dar.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -330,7 +331,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Kit_TruthCountMintermsPrecomp();
 //    Kit_DsdPrecompute4Vars();
 
-//    Dar_LibStart();
+    Dar_LibStart();
 } 
 
 /**Function*************************************************************
@@ -346,7 +347,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
-//    Dar_LibStop();
+    Dar_LibStop();
 
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
@@ -6048,7 +6049,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 //    Abc_Ntk4VarTable( pNtk );
-//    Dat_NtkGenerateArrays( pNtk );
+//    Dar_NtkGenerateArrays( pNtk );
+//    Dar_ManDeriveCnfTest2();
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
@@ -7301,6 +7303,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fExdc;
     int c;
     int fPartition = 0;
+    extern void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10535,6 +10538,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     char ** pArgvNew;
     int nArgcNew;
     int c;
+    int fRetime;
     int fSat;
     int fVerbose;
     int nFrames;
@@ -10544,6 +10548,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames );
     extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
+    extern void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -10551,6 +10556,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fRetime  =  0; // verification after retiming
     fSat     =  0;
     fVerbose =  0;
     nFrames  =  5;
@@ -10558,7 +10564,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     nConfLimit = 10000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10606,6 +10612,9 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nInsLimit < 0 ) 
                 goto usage;
             break;
+        case 'r':
+            fRetime ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -10629,7 +10638,9 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // perform equivalence checking
-    if ( fSat )
+    if ( fRetime )
+        Abc_NtkSecRetime( pNtk1, pNtk2 );
+    else if ( fSat )
         Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nInsLimit, nFrames );
     else
         Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
@@ -10639,9 +10650,10 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-svh] <file1> <file2>\n" );
+    fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-srvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs bounded sequential equivalence checking\n" );
     fprintf( pErr, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
+    fprintf( pErr, "\t-r     : toggles retiming verification [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 81278515..a936f9bf 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -53,7 +53,10 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
         pObj->pCopy = (Abc_Obj_t *)Dar_ObjCreatePi(pMan);
     // perform the conversion of the internal nodes (assumes DFS ordering)
     Abc_NtkForEachNode( pNtk, pObj, i )
+    {
         pObj->pCopy = (Abc_Obj_t *)Dar_And( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj), (Dar_Obj_t *)Abc_ObjChild1Copy(pObj) );
+//        printf( "%d->%d ", pObj->Id, ((Dar_Obj_t *)pObj->pCopy)->Id );
+    }
     // create the POs
     Abc_NtkForEachCo( pNtk, pObj, i )
         Dar_ObjCreatePo( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj) );
@@ -87,7 +90,10 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
     // rebuild the AIG
     vNodes = Dar_ManDfs( pMan );
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) );
+        if ( Dar_ObjIsBuf(pObj) )
+            pObj->pData = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj);
+        else
+            pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) );
     Vec_PtrFree( vNodes );
     // connect the PO nodes
     Dar_ManForEachPo( pMan, pObj, i )
@@ -195,6 +201,52 @@ int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs verification after retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+    int fRemove1, fRemove2;
+    Dar_Man_t * pMan1, * pMan2;
+    int * pArray;
+
+    fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
+    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
+
+
+    pMan1 = Abc_NtkToDar( pNtk1 );
+    pMan2 = Abc_NtkToDar( pNtk2 );
+
+    Dar_ManPrintStats( pMan1 );
+    Dar_ManPrintStats( pMan2 );
+
+    pArray = Abc_NtkGetLatchValues(pNtk1);
+    Dar_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray );
+    free( pArray );
+
+    pArray = Abc_NtkGetLatchValues(pNtk2);
+    Dar_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray );
+    free( pArray );
+
+    Dar_ManPrintStats( pMan1 );
+    Dar_ManPrintStats( pMan2 );
+
+    Dar_ManStop( pMan1 );
+    Dar_ManStop( pMan2 );
+
+
+    if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
+    if ( fRemove2 )  Abc_NtkDelete( pNtk2 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -208,7 +260,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkAig;
     Dar_Man_t * pMan;//, * pTemp;
-    int * pArray;
+//    int * pArray;
 
     assert( Abc_NtkIsStrash(pNtk) );
     // convert to the AIG manager
@@ -223,15 +275,29 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
     }
     // perform balance
     Dar_ManPrintStats( pMan );
-
+/*
     pArray = Abc_NtkGetLatchValues(pNtk);
     Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray );
     free( pArray );
+*/
 
 //    Dar_ManDumpBlif( pMan, "aig_temp.blif" );
 //    pMan->pPars = Dar_ManDefaultParams();
-//    Dar_ManRewrite( pMan );
+    Dar_ManRewrite( pMan );
     Dar_ManPrintStats( pMan );
+    Dar_ManPrintRuntime( pMan );
+//    Dar_ManComputeCuts( pMan );
+
+/*
+{
+extern Dar_Cnf_t * Dar_ManDeriveCnf( Dar_Man_t * p );
+extern void Dar_CnfFree( Dar_Cnf_t * pCnf );
+Dar_Cnf_t * pCnf;
+pCnf = Dar_ManDeriveCnf( pMan );
+Dar_CnfFree( pCnf );
+}
+*/
+
     // convert from the AIG manager
     if ( Dar_ManLatchNum(pMan) )
         pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan );
@@ -250,6 +316,8 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
     return pNtkAig;
 }
 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index 0413dc8f..fdfdb4f6 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -131,7 +131,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
             for ( i = 1; i < vTokens->nSize; i++ )
                 Io_ReadCreatePo( pNtk, vTokens->pArray[i] );
         }
-        else
+        else 
         {
             // check if the input/output names are given
             if ( Abc_NtkPiNum(pNtk) == 0 )