Version abc70727

5 files changed, 63 insertions, 30 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1dd9b65e..1df13db8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -326,7 +326,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
-//    Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "scleanup",      Abc_CommandSeqCleanup,       1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
@@ -10736,8 +10736,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fExdc;
     int fImp;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10801,14 +10800,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-//    if ( fImp )
-//        pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose );
-//    else
-//        pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose );
-    pNtkRes = NULL;
+    pNtkRes = Abc_NtkSeqSweep( pNtk, nFrames, fVerbose );
     if ( pNtkRes == NULL )
     {
-        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        fprintf( pErr, "Sequential sweeping has failed.\n" );
         return 1;
     }
     // replace the current network
@@ -10819,8 +10814,8 @@ usage:
     fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using van Eijk's method\n" );
     fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames );
-    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
-    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
+//    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
+//    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index f04f3d97..64043717 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -129,7 +129,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Abc_Ntk_t * pNtkNew;
     Aig_Obj_t * pObj, * pTemp;
     int i;
-    assert( pMan->pReprs != NULL );
+    assert( pMan->pEquivs != NULL );
     assert( Aig_ManBufNum(pMan) == 0 );
     // perform strashing
     pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
@@ -142,7 +142,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
-        if ( pTemp = pMan->pReprs[pObj->Id] )
+        if ( pTemp = pMan->pEquivs[pObj->Id] )
         {
             Abc_Obj_t * pAbcRepr, * pAbcObj;
             assert( pTemp->pData != NULL );
@@ -261,14 +261,15 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
+Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
 {
+    Vec_Int_t * vInits;
     Abc_Obj_t * pLatch;
-    int i, * pArray;
-    pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+    int i;
+    vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
-        pArray[i] = Abc_LatchIsInit1(pLatch);
-    return pArray;
+        Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) );
+    return vInits;
 }
 
 /**Function*************************************************************
@@ -298,11 +299,13 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     Aig_ManPrintStats( pMan1 );
     Aig_ManPrintStats( pMan2 );
 
-    pArray = Abc_NtkGetLatchValues(pNtk1);
+//    pArray = Abc_NtkGetLatchValues(pNtk1);
+    pArray = NULL;
     Aig_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray );
     free( pArray );
 
-    pArray = Abc_NtkGetLatchValues(pNtk2);
+//    pArray = Abc_NtkGetLatchValues(pNtk2);
+    pArray = NULL;
     Aig_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray );
     free( pArray );
 
@@ -414,7 +417,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
     pPars->fDoSparse    = fDoSparse;
     pPars->fSpeculate   = fSpeculate;
     pPars->fChoicing    = fChoicing;
-    pMan = Fra_Perform( pTemp = pMan, pPars );
+    pMan = Fra_FraigPerform( pTemp = pMan, pPars );
     if ( fChoicing )
         pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
     else
@@ -471,14 +474,14 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
-
+/*
 //    Aig_ManSupports( pMan );
     {
         Vec_Vec_t * vParts;
         vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL );
         Vec_VecFree( vParts );
     }
-
+*/
     Dar_ManRewrite( pMan, pPars );
 //    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
 //    Aig_ManStop( pTemp );
@@ -703,7 +706,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
     Aig_ManPrintStats( pMan );
 
     // derive CNF
-    pCnf = Cnf_Derive( pMan );
+    pCnf = Cnf_Derive( pMan, 0 );
     pManCnf = Cnf_ManRead();
 
     // write the network for verification
@@ -747,7 +750,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     // conver to the manager
     pMan = Abc_NtkToDar( pNtk );
     // derive CNF
-    pCnf = Cnf_Derive( pMan );
+    pCnf = Cnf_Derive( pMan, 0 );
     // convert into the SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf );
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
@@ -763,7 +766,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
 
 
 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-    PRT( "Time", clock() - clk );
+//    PRT( "Time", clock() - clk );
 
     // simplify the problem
     clk = clock();
@@ -818,6 +821,35 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+    pMan->vInits = Abc_NtkGetLatchValues( pNtk );
+
+    pMan = Fra_Induction( pTemp = pMan, nFrames, fVerbose );
+    Aig_ManStop( pTemp );
+
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 2376b72c..89b79e5a 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -69,13 +69,13 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
     assert( Abc_NtkIsStrash(pNtk) );
     // cleanup the AIG
     Abc_AigCleanup(pNtk->pManFunc);
-
+/*
     {
         Vec_Vec_t * vParts;
         vParts = Abc_NtkPartitionSmart( pNtk, 50, 1 );
         Vec_VecFree( vParts );
     }
-
+*/
 
     // start placement package
     if ( fPlaceEnable )
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index aafa6530..58614584 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -70,7 +70,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
 //return 1;
 
 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-    PRT( "Time", clock() - clk );
+//    PRT( "Time", clock() - clk );
 
     // simplify the problem
     clk = clock();
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 1c6cbcb0..8f43c605 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -237,7 +237,13 @@ usage:
 
   Synopsis    [Initialization procedure for the library project.]
 
-  Description []
+  Description [Note that when Abc_Start() is run in a static library
+  project, it does not load the resource file by default. As a result, 
+  ABC is not set up the same way, as when it is run on a command line. 
+  For example, some error messages while parsing files will not be 
+  produced, and intermediate networks will not be checked for consistancy. 
+  One possibility is to load the resource file after Abc_Start() as follows:
+  Abc_UtilsSource(  Abc_FrameGetGlobalFrame() );]
                
   SideEffects []