Unsuccessful attempt to improve PDR and a few minor changes.

5 files changed, 366 insertions, 30 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index f667d4e3..aa55f2fc 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -254,10 +254,17 @@ static inline int          Aig_WordFindFirstBit( unsigned uWord )
     return -1;
 }
 
-static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
-static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^  01); }
-static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
-static inline int          Aig_IsComplement( Aig_Obj_t * p )      { return (int)((ABC_PTRUINT_T)(p) & 01);          }
+static inline int          Aig_Var2Lit( int Var, int fCompl )     { return Var + Var + fCompl;                       }
+static inline int          Aig_Lit2Var( int Lit )                 { return Lit >> 1;                                 }
+static inline int          Aig_LitIsCompl( int Lit )              { return Lit & 1;                                  }
+static inline int          Aig_LitNot( int Lit )                  { return Lit ^ 1;                                  }
+static inline int          Aig_LitNotCond( int Lit, int c )       { return Lit ^ (int)(c > 0);                       }
+static inline int          Aig_LitRegular( int Lit )              { return Lit & ~01;                                }
+
+static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);  }
+static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);  }
+static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));  }
+static inline int          Aig_IsComplement( Aig_Obj_t * p )      { return (int)((ABC_PTRUINT_T)(p) & 01);           }
 
 static inline int          Aig_ManPiNum( Aig_Man_t * p )          { return p->nObjs[AIG_OBJ_PI];                     }
 static inline int          Aig_ManPoNum( Aig_Man_t * p )          { return p->nObjs[AIG_OBJ_PO];                     }
diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c
new file mode 100644
index 00000000..c6b3a8c0
--- /dev/null
+++ b/src/aig/aig/aigJust.c
@@ -0,0 +1,299 @@
+/**CFile****************************************************************
+ 
+  FileName    [aigJust.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Justification of node values.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigJust.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define AIG_VAL0  1
+#define AIG_VAL1  2
+#define AIG_VALX  3
+
+// storing ternary values
+static inline int Aig_ObjSetTerValue( Aig_Obj_t * pNode, int Value )
+{
+    assert( Value );
+    pNode->fMarkA = (Value & 1);
+    pNode->fMarkB = ((Value >> 1) & 1);
+    return Value;
+}
+static inline int Aig_ObjGetTerValue( Aig_Obj_t * pNode )
+{
+    return (pNode->fMarkB << 1) | pNode->fMarkA;
+}
+
+// working with ternary values
+static inline int Aig_ObjNotTerValue( int Value )
+{
+    if ( Value == AIG_VAL1 )
+        return AIG_VAL0;
+    if ( Value == AIG_VAL0 )
+        return AIG_VAL1;
+    return AIG_VALX;
+}
+static inline int Aig_ObjAndTerValue( int Value0, int Value1 )
+{
+    if ( Value0 == AIG_VAL0 || Value1 == AIG_VAL0 )
+        return AIG_VAL0;
+    if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 )
+        return AIG_VAL1;
+    return AIG_VALX;
+}
+static inline int Aig_ObjNotCondTerValue( int Value, int Cond )
+{
+    return Cond ? Aig_ObjNotTerValue( Value ) : Value;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns value (0 or 1) or X if unassigned.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_ObjSatValue( Aig_Man_t * pAig, Aig_Obj_t * pNode, int fCompl )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
+        return (pNode->fMarkA ^ fCompl) ? AIG_VAL1 : AIG_VAL0;
+    return AIG_VALX;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively searched for a satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Vec_Int_t * vSuppLits, int Heur )
+{
+    int Value0, Value1;
+//    ++Heur;
+    if ( Aig_ObjIsConst1(pNode) )
+        return 1;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
+        return ((int)pNode->fMarkA == Value);
+    Aig_ObjSetTravIdCurrent(pAig, pNode);
+    pNode->fMarkA = Value;
+    if ( Aig_ObjIsPi(pNode) )
+    {
+//        if ( Aig_ObjId(pNode) % 1000 == 0 )
+//            Value ^= 1;
+        if ( vSuppLits )
+            Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
+        return 1;
+    }
+    assert( Aig_ObjIsNode(pNode) );
+    // propagation
+    if ( Value ) 
+    {
+        if ( !Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), !Aig_ObjFaninC0(pNode), vSuppLits, Heur) )
+            return 0;
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), !Aig_ObjFaninC1(pNode), vSuppLits, Heur);
+    }
+    // justification
+    Value0 = Aig_ObjSatValue( pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode) );
+    if ( Value0 == AIG_VAL0 )
+        return 1;
+    Value1 = Aig_ObjSatValue( pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode) );
+    if ( Value1 == AIG_VAL0 )
+        return 1;
+    if ( Value0 == AIG_VAL1 && Value1 == AIG_VAL1 )
+        return 0;
+    if ( Value0 == AIG_VAL1 )
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur);
+    if ( Value1 == AIG_VAL1 )
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur);
+    assert( Value0 == AIG_VALX && Value1 == AIG_VALX );
+    // decision making
+//    if ( rand() % 10 == Heur )
+//    if ( Aig_ObjId(pNode) % 8 == Heur )
+    if ( ++Heur % 8 == 0 )
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin1(pNode), Aig_ObjFaninC1(pNode), vSuppLits, Heur);
+    else
+        return Aig_NtkFindSatAssign_rec(pAig, Aig_ObjFanin0(pNode), Aig_ObjFaninC0(pNode), vSuppLits, Heur);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if SAT assignment is found; 0 otherwise.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjFindSatAssign( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Vec_Int_t * vSuppLits )
+{
+    int i;
+    if ( Aig_ObjIsPo(pNode) )
+        return Aig_ObjFindSatAssign( pAig, Aig_ObjFanin0(pNode), Value ^ Aig_ObjFaninC0(pNode), vSuppLits );
+    for ( i = 0; i < 8; i++ )
+    {
+        Vec_IntClear( vSuppLits );
+        Aig_ManIncrementTravId( pAig );
+        if ( Aig_NtkFindSatAssign_rec( pAig, pNode, Value, vSuppLits, i ) )
+            return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjTerSimulate_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode )
+{
+    int Value0, Value1;
+    if ( Aig_ObjIsConst1(pNode) )
+        return AIG_VAL1;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pNode) )
+        return Aig_ObjGetTerValue( pNode );
+    Aig_ObjSetTravIdCurrent( pAig, pNode );
+    if ( Aig_ObjIsPi(pNode) )
+        return Aig_ObjSetTerValue( pNode, AIG_VALX );
+    Value0 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin0(pNode)), Aig_ObjFaninC0(pNode) );
+    if ( Aig_ObjIsPo(pNode) || Value0 == AIG_VAL0 )
+        return Aig_ObjSetTerValue( pNode, Value0 );
+    assert( Aig_ObjIsNode(pNode) );
+    Value1 = Aig_ObjNotCondTerValue( Aig_ObjTerSimulate_rec(pAig, Aig_ObjFanin1(pNode)), Aig_ObjFaninC1(pNode) );
+    return Aig_ObjSetTerValue( pNode, Aig_ObjAndTerValue(Value0, Value1) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns value of the object under input assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLits )
+{
+    Aig_Obj_t * pObj;
+    int i, Entry;
+    Aig_ManIncrementTravId( pAig );
+    Vec_IntForEachEntry( vSuppLits, Entry, i )
+    {
+        pObj = Aig_ManPi( pAig, Aig_Lit2Var(Entry) );
+        Aig_ObjSetTerValue( pObj, Aig_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 );
+        Aig_ObjSetTravIdCurrent( pAig, pObj );
+//printf( "%d ", Entry );
+    }
+//printf( "\n" );
+    return Aig_ObjTerSimulate_rec( pAig, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing of the framework.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManTerSimulate( Aig_Man_t * pAig )
+{
+    Vec_Int_t * vSuppLits;
+    Aig_Obj_t * pObj;
+    int i, clk = clock(), Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
+    int nTotalLits = 0;
+    vSuppLits = Vec_IntAlloc( 100 );
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        if ( pObj->fPhase ) // const 1
+        {
+            if ( Aig_ObjFindSatAssign(pAig, pObj, 0, vSuppLits) )
+            {
+//                assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL0 );
+                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 )
+                    printf( "Justification error!\n" );
+                Count0++;
+                nTotalLits += Vec_IntSize(vSuppLits);
+            }
+            else
+                Count0f++;
+        }
+        else
+        {
+            if ( Aig_ObjFindSatAssign(pAig, pObj, 1, vSuppLits) )
+            {
+//                assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL1 );
+                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 )
+                    printf( "Justification error!\n" );
+                Count1++;
+                nTotalLits += Vec_IntSize(vSuppLits);
+            }
+            else
+                Count1f++;
+        }
+    }
+    Vec_IntFree( vSuppLits );
+    printf( "PO =%6d. C0 =%6d. C0f =%6d. C1 =%6d. C1f =%6d. (%6.2f %%) Ave =%4.1f ", 
+        Aig_ManPoNum(pAig), Count0, Count0f, Count1, Count1f, 100.0*(Count0+Count1)/Aig_ManPoNum(pAig), 1.0*nTotalLits/(Count0+Count1) );
+    Abc_PrintTime( 1, "T", clock() - clk );
+    Aig_ManCleanMarkAB( pAig );
+}
+
+
+
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigPack.c b/src/aig/aig/aigPack.c
new file mode 100644
index 00000000..8d7b54df
--- /dev/null
+++ b/src/aig/aig/aigPack.c
@@ -0,0 +1,54 @@
+/**CFile****************************************************************
+ 
+  FileName    [aigPack.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Bit-packing code.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigPack.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 03504138..c291433f 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -6,12 +6,14 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigFrames.c \
     src/aig/aig/aigInter.c \
+    src/aig/aig/aigJust.c \
     src/aig/aig/aigMan.c \
     src/aig/aig/aigMem.c \
     src/aig/aig/aigMffc.c \
     src/aig/aig/aigObj.c \
     src/aig/aig/aigOper.c \
     src/aig/aig/aigOrder.c \
+    src/aig/aig/aigPack.c \
     src/aig/aig/aigPart.c \
     src/aig/aig/aigPartReg.c \
     src/aig/aig/aigPartSat.c \
diff --git a/src/aig/ivy/ivyFastMap.c b/src/aig/ivy/ivyFastMap.c
index 05db377d..1d9efca1 100644
--- a/src/aig/ivy/ivyFastMap.c
+++ b/src/aig/ivy/ivyFastMap.c
@@ -344,32 +344,6 @@ static inline int Ivy_ObjIsNodeInt2( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_IntSelectSort( int * pArray, int nSize )
-{
-    int temp, i, j, best_i;
-    for ( i = 0; i < nSize-1; i++ )
-    {
-        best_i = i;
-        for ( j = i+1; j < nSize; j++ )
-            if ( pArray[j] < pArray[best_i] )
-                best_i = j;
-        temp = pArray[i]; 
-        pArray[i] = pArray[best_i]; 
-        pArray[best_i] = temp;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fast mapping for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static inline int Vec_IntRemoveDup( int * pArray, int nSize )
 {
     int i, k;