Version abc80915

2 files changed, 52 insertions, 10 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0db761c7..a0d26e3b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7684,7 +7684,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
-//    Abc_Ntk_t * pNtkRes;
+    Abc_Ntk_t * pNtkRes = NULL;
     int c;
     int fBmc;
     int nFrames;
@@ -7712,6 +7712,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
     extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
 //    extern void Aig_ProcedureTest();
+    extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -7912,14 +7914,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*//*
-
-    if ( argc != globalUtilOptind + 1 )
-        goto usage;
-    pFileName = argv[globalUtilOptind];
-    Nwk_ManLutMergeGraphTest( pFileName );
 */
-//    Aig_ProcedureTest();
+
+    pNtkRes = Abc_NtkDarTestNtk( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 
     return 0;
 usage:
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index f1e5efb0..388fc5df 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2351,20 +2351,58 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
 ***********************************************************************/
 void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
 {
-    Aig_Man_t * pMan;
+    extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
+
+    Aig_Man_t * pMan, * pTemp;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
-
+/*
 Aig_ManSetRegNum( pMan, pMan->nRegs );
 Aig_ManPrintStats( pMan );
 Saig_ManDumpBlif( pMan, "_temp_.blif" );
 Aig_ManStop( pMan );
 pMan = Saig_ManReadBlif( "_temp_.blif" );
 Aig_ManPrintStats( pMan );
+*/
+    Aig_ManSetRegNum( pMan, pMan->nRegs );
+    pTemp = Ssw_SignalCorrespondeceTestPairs( pMan );
+    Aig_ManStop( pTemp );
+    Aig_ManStop( pMan );
+}
 
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
+{
+    extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
+
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+
+    Aig_ManSetRegNum( pMan, pMan->nRegs );
+    pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan );
+    Aig_ManStop( pTemp );
+
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
     Aig_ManStop( pMan );
+    return pNtkAig;
 }
 
 ////////////////////////////////////////////////////////////////////////