Version abc90413

10 files changed, 86 insertions, 20 deletions

diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 5a52e913..cd3ce7b9 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -711,6 +711,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
         pRes  = Cec_ManSimSimRef( p, i );
         pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
         pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
+
         if ( Gia_ObjFaninC0(pObj) )
         {
             if ( Gia_ObjFaninC1(pObj) )
@@ -729,6 +730,7 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
                 for ( w = 1; w <= p->nWords; w++ )
                     pRes[w] = pRes0[w] & pRes1[w];
         }
+
 references:
         // if this node is candidate constant, collect it
         if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index eb582e4c..de71ecc9 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -70,7 +70,8 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 ***********************************************************************/
 void Cec_ManSatPrintStats( Cec_ManSat_t * p )
 {
-    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
+    printf( "CO = %8d  ", Gia_ManCoNum(p->pAig) );
+    printf( "AND = %8d  ", Gia_ManAndNum(p->pAig) );
     printf( "Conf = %5d  ", p->pPars->nBTLimit );
     printf( "MinVar = %5d  ", p->pPars->nSatVarMax );
     printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 832eff26..f53a3d33 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -885,6 +885,8 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
         pDecVar = Gia_Not(Gia_ObjChild0(pVar));
     else
         pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+//    pDecVar = Gia_NotCond( Gia_Regular(pDecVar), Gia_Regular(pDecVar)->fPhase );
+//    pDecVar = Gia_Not(pDecVar);
     // decide on first fanin
     Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
     if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
@@ -955,8 +957,9 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
 ***********************************************************************/
 void Cbs_ManSatPrintStats( Cbs_Man_t * p )
 {
-    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
-    printf( "Conf = %5d  ", p->Pars.nBTLimit );
+    printf( "CO = %8d  ", Gia_ManCoNum(p->pAig) );
+    printf( "AND = %8d  ", Gia_ManAndNum(p->pAig) );
+    printf( "Conf = %6d  ", p->Pars.nBTLimit );
     printf( "JustMax = %5d  ", p->Pars.nJustLimit );
     printf( "\n" );
     printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
@@ -984,6 +987,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
 ***********************************************************************/
 Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
 {
+    extern void Gia_ManCollectTest( Gia_Man_t * pAig );
     extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
     Cbs_Man_t * p; 
     Vec_Int_t * vCex, * vVisit, * vCexStore;
@@ -991,11 +995,13 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
     Gia_Obj_t * pRoot; 
     int i, status, clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) == 0 );
+//    Gia_ManCollectTest( pAig );
     // prepare AIG
     Gia_ManCreateRefs( pAig );
     Gia_ManCleanMark0( pAig );
     Gia_ManCleanMark1( pAig );
     Gia_ManFillValue( pAig ); // maps nodes into trail ids
+    Gia_ManSetPhase( pAig ); // maps nodes into trail ids
     // create logic network
     p = Cbs_ManAlloc();
     p->Pars.nBTLimit = nConfs;
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
index 409af56c..a0d97693 100644
--- a/src/aig/gia/giaCSatOld.c
+++ b/src/aig/gia/giaCSatOld.c
@@ -674,8 +674,9 @@ int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
 ***********************************************************************/
 void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
 {
-    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
-    printf( "Conf = %5d  ", p->Pars.nBTLimit );
+    printf( "CO = %8d  ", Gia_ManCoNum(p->pAig) );
+    printf( "AND = %8d  ", Gia_ManAndNum(p->pAig) );
+    printf( "Conf = %6d  ", p->Pars.nBTLimit );
     printf( "JustMax = %5d  ", p->Pars.nJustLimit );
     printf( "\n" );
     printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index a978dcc3..8a3aef92 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -122,7 +122,7 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN
     Gia_Obj_t * pObj;
     int i; 
     Vec_IntClear( vNodes );
-    Gia_ManIncrementTravId( p );
+//    Gia_ManIncrementTravId( p );
     Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
     for ( i = 0; i < nNodes; i++ )
     {
@@ -145,6 +145,34 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManCollectTest( Gia_Man_t * p )
+{
+    Vec_Int_t * vNodes;
+    Gia_Obj_t * pObj;
+    int i, iNode, clk = clock();
+    vNodes = Vec_IntAlloc( 100 );
+    Gia_ManResetTravId( p );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        iNode = Gia_ObjId(p, pObj);
+        Gia_ManCollectAnds( p, &iNode, 1, vNodes );
+    }
+    Vec_IntFree( vNodes );
+    ABC_PRT( "DFS from each output", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects support nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Gia_ManSuppSize_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     if ( Gia_ObjIsTravIdCurrent(p, pObj) )
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index cdee73d0..041be0f5 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1135,6 +1135,8 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
             assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
             return;
         }
+        if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
+            return;
         assert( pRepr->Value < pObj->Value );
         pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
         pObjNew  = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8ac8b241..6beaf144 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2575,7 +2575,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     if ( fComplOuts )
-    Abc_NtkForEachCo( pNtkRes, pObj, c )
+    Abc_NtkForEachPo( pNtkRes, pObj, c )
         Abc_ObjXorFaninC( pObj, 0 );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -14914,8 +14914,9 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int nFrames;
+    int fUseXval;
     int fVerbose;
-    extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+    extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVerbose );
     extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -14924,9 +14925,10 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nFrames    = 100;
+    fUseXval   =   0;
     fVerbose   =   0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fxvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14941,6 +14943,9 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames < 0 ) 
                 goto usage;
             break;
+        case 'x':
+            fUseXval ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -14966,18 +14971,25 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "The network is combinational.\n" );
         return 0;
     }
-
-    if ( Abc_NtkIsStrash(pNtk) )
-        Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
+    if ( fUseXval && !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "X-valued simulation only works for AIGs. Run \"strash\".\n" );
+        return 0;
+    }
+    if ( fUseXval )
+        Abc_NtkCycleInitState( pNtk, nFrames, 1, fVerbose );
+    else if ( Abc_NtkIsStrash(pNtk) )
+        Abc_NtkCycleInitState( pNtk, nFrames, 0, fVerbose );
     else
         Abc_NtkCycleInitStateSop( pNtk, nFrames, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cycle [-F num] [-vh]\n" );
-    fprintf( pErr, "\t         cycles sequiential circuit for the given number of timeframes\n" );
+    fprintf( pErr, "usage: cycle [-F num] [-xvh]\n" );
+    fprintf( pErr, "\t         cycles sequential circuit for the given number of timeframes\n" );
     fprintf( pErr, "\t         to derive a new initial state (which may be on the envelope)\n" );
     fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-x     : use x-valued primary inputs [default = %s]\n", fUseXval? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -16090,6 +16102,14 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
     }
 
+    if ( Abc_NtkLatchNum(pNtk1) || Abc_NtkLatchNum(pNtk2) )
+    {
+        if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+        if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+        printf( "Currently this command only works for networks without latches. Run \"comb\".\n" );
+        return 1;
+    }
+
     // perform equivalence checking
     if ( fSat && fMiter )
         Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
@@ -21934,6 +21954,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         pMan = Gia_ManToAig( pAbc->pAig, 0 );
         pNtk = Abc_NtkFromAigPhase( pMan );
+        pNtk->pName = Extra_UtilStrsav(pMan->pName);
         Aig_ManStop( pMan );
     }
     else
@@ -23059,7 +23080,7 @@ usage:
     fprintf( stdout, "usage: &frames [-FL <num>] [-ivh]\n" );
     fprintf( stdout, "\t         unrolls the design for several timeframes\n" );
     fprintf( stdout, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
-    fprintf( stdout, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" );
+    fprintf( stdout, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit );
     fprintf( stdout, "\t-i     : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index e63b296a..76a82b51 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -181,15 +181,15 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXS
 
   Synopsis    [Cycles the circuit to create a new initial state.]
 
-  Description [Simulates the circuit with random input for the given 
-  number of timeframes to get a better initial state.]
+  Description [Simulates the circuit with random (or ternary) input 
+  for the given number of timeframes to get a better initial state.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
+void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVerbose )
 { 
     Abc_Obj_t * pObj;
     int i, f;
@@ -198,13 +198,12 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
     // initialize the values
     Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
     Abc_NtkForEachLatch( pNtk, pObj, i )
-//        Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchIsInit1(pObj)? XVS1 : XVS0 );
         Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
     // simulate for the given number of timeframes
     for ( f = 0; f < nFrames; f++ )
     {
         Abc_NtkForEachPi( pNtk, pObj, i )
-            Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+            Abc_ObjSetXsim( pObj, fUseXval? ABC_INIT_DC : Abc_XsimRand2() );
         Abc_AigForEachAnd( pNtk, pObj, i )
             Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
         Abc_NtkForEachCo( pNtk, pObj, i )
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index eea601a8..95e7cd1d 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -941,6 +941,9 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
             Abc_LatchSetInit0( pObj );
         else
         {
+            if ( Vec_PtrSize(vTokens) > 6 )
+                printf( "Warning: Line %d has .latch directive with unrecognized entries (the total of %d entries).\n", 
+                    Io_MvGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) ); 
             if ( Vec_PtrSize(vTokens) > 3 )
                 Init = atoi( Vec_PtrEntryLast(vTokens) );
             else
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 8fc30056..9cacd021 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -332,6 +332,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     Hop_Obj_t * pFunc;
     int nFanins, status;
     int c, i, * pGloVars;
+//    int clk = clock();
 
 //    p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
 
@@ -345,6 +346,8 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
         p->nTimeOuts++;
         return NULL;
     }
+//printf( "%d\n", pSat->stats.conflicts );
+//    ABC_PRT( "S", clock() - clk );
     // get the learned clauses
     pCnf = sat_solver_store_release( pSat );
     sat_solver_delete( pSat );