Added generation of values of internal nodes for GIA manager.

5 files changed, 259 insertions, 93 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2d7a0695..3a22f8f4 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -154,6 +154,7 @@ struct Gia_Man_t_
     void *         pLutLib;       // LUT library
     word           nHashHit;      // hash table hit
     word           nHashMiss;     // hash table miss
+    unsigned *     pData2;        // storage for object values
     int            fVerbose;      // verbose reports
     // truth table computation for small functions
     int            nTtVars;       // truth table variables
@@ -740,6 +741,12 @@ extern void                Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFile
 /*=== giaBidec.c ===========================================================*/
 extern unsigned *          Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
 extern Gia_Man_t *         Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
+/*=== giaCex.c ============================================================*/
+extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
+extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
+extern void                Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex );
+extern void                Gia_ManCounterExampleValueStop( Gia_Man_t * pGia );
+extern int                 Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame );
 /*=== giaCsatOld.c ============================================================*/
 extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCsat.c ============================================================*/
@@ -959,8 +966,6 @@ extern int                 Gia_ManHasDangling( Gia_Man_t * p );
 extern int                 Gia_ManMarkDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
-extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
-extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
 extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
 extern void                Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern unsigned *          Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c
new file mode 100644
index 00000000..bb3da946
--- /dev/null
+++ b/src/aig/gia/giaCex.c
@@ -0,0 +1,250 @@
+/**CFile****************************************************************
+
+  FileName    [giaAbs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Counter-example-guided abstraction refinement.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#include "gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Gia_ManCleanMark0(pAig);
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Gia_ManForEachPi( pAig, pObj, k )
+            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pAig, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pAig, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+        {
+            pObjRo->fMark0 = pObjRi->fMark0;
+        }
+    }
+    assert( iBit == p->nBits );
+    if ( fDualOut )
+        RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
+    else
+        RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
+    Gia_ManCleanMark0(pAig);
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    assert( Gia_ManPiNum(pAig) == p->nPis );
+    Gia_ManCleanMark0(pAig);
+//    Gia_ManForEachRo( pAig, pObj, i )
+//       pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+    iBit = p->nRegs;
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Gia_ManForEachPi( pAig, pObj, k )
+            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pAig, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pAig, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( iBit == p->nBits );
+    // figure out the number of failed output
+    RetValue = -1;
+//    for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
+    for ( i = nOutputs; i < Gia_ManPoNum(pAig); i++ )
+    {
+        if ( Gia_ManPo(pAig, i)->fMark0 )
+        {
+            RetValue = i;
+            break;
+        }
+    }
+    Gia_ManCleanMark0(pAig);
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the process of returning values for internal nodes.]
+
+  Description [Should be called when pCex is available, before probing 
+  any object for its value using Gia_ManCounterExampleValueLookup().]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int Val0, Val1, nObjs, i, k, iBit = 0;
+    assert( Gia_ManRegNum(pGia) > 0 ); // makes sense only for sequential AIGs
+    assert( pGia->pData2 == NULL );    // if this fail, there may be a memory leak
+    // allocate memory to store simulation bits for internal nodes
+    pGia->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Gia_ManObjNum(pGia) ) );
+    // the register values in the counter-example should be zero
+    Gia_ManForEachRo( pGia, pObj, k )
+        assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
+    // iterate through the timeframes
+    nObjs = Gia_ManObjNum(pGia);
+    for ( i = 0; i <= pCex->iFrame; i++ )
+    {
+        // no need to set constant-0 node
+        // set primary inputs according to the counter-example
+        Gia_ManForEachPi( pGia, pObj, k )
+            if ( Abc_InfoHasBit(pCex->pData, iBit++) )
+                Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
+        // compute values for each node
+        Gia_ManForEachAnd( pGia, pObj, k )
+        {
+            Val0 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId0p(pGia, pObj) );
+            Val1 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId1p(pGia, pObj) );
+            if ( (Val0 ^ Gia_ObjFaninC0(pObj)) & (Val1 ^ Gia_ObjFaninC1(pObj)) )
+                Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
+        }
+        // derive values for combinational outputs
+        Gia_ManForEachCo( pGia, pObj, k )
+        {
+            Val0 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId0p(pGia, pObj) );
+            if ( Val0 ^ Gia_ObjFaninC0(pObj) )
+                Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
+        }
+        if ( i == pCex->iFrame )
+            continue;
+        // transfer values to the register output of the next frame
+        Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k )
+            if ( Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObjRi) ) )
+                Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * (i+1) + Gia_ObjId(pGia, pObjRo) );
+    }
+    assert( iBit == pCex->nBits );
+    // check that the counter-example is correct, that is, the corresponding output is asserted
+    assert( Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * pCex->iFrame + Gia_ObjId(Gia_ManCo(pGia, pCex->iPo)) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the process of returning values for internal nodes.]
+
+  Description [Should be called when probing is no longer needed]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia )
+{
+    assert( pGia->pData2 != NULL );    // if this fail, we try to call this procedure more than once
+    ABC_FREE( pGia->pData2 );
+    pGia->pData2 = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the value of the given object in the given timeframe.]
+
+  Description [Should be called to probe the value of an object with 
+  the given ID (iFrame is a 0-based number of a time frame - should not 
+  exceed the number of timeframes in the original counter-example).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCounterExampleValueLookup(  Gia_Man_t * pGia, int Id, int iFrame )
+{
+    assert( Id >= 0 && Id < Gia_ManObjNum(pGia) );
+    return Abc_InfoHasBit( (unsigned *)pGia->pData2, Gia_ManObjNum(pGia) * iFrame + Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure to test the above code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCounterExampleValueTest( Gia_Man_t * pGia, Abc_Cex_t * pCex )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( pGia, Gia_ManObjNum(pGia)/2 );
+    int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 );
+    printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
+    Gia_ManCounterExampleValueStart( pGia, pCex );
+    printf( "Value of object %d in frame %d is %d.\n", Gia_ObjId(pGia, pObj), iFrame,
+        Gia_ManCounterExampleValueLookup(pGia, Gia_ObjId(pGia, pObj), iFrame) );
+    Gia_ManCounterExampleValueStop( pGia );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 5b5fe13a..152ea223 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -93,6 +93,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vMapping );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
+    ABC_FREE( p->pData2 );
     ABC_FREE( p->pTravIds );
     ABC_FREE( p->pPlacement );
     ABC_FREE( p->pSwitching );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 6f01e5cd..43ef3e08 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1183,97 +1183,6 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
-{
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
-    int RetValue, i, k, iBit = 0;
-    Gia_ManCleanMark0(pAig);
-    Gia_ManForEachRo( pAig, pObj, i )
-        pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-        Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
-        Gia_ManForEachAnd( pAig, pObj, k )
-            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
-                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
-        Gia_ManForEachCo( pAig, pObj, k )
-            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
-        if ( i == p->iFrame )
-            break;
-        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
-        {
-            pObjRo->fMark0 = pObjRi->fMark0;
-        }
-    }
-    assert( iBit == p->nBits );
-    if ( fDualOut )
-        RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
-    else
-        RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
-    Gia_ManCleanMark0(pAig);
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
-{
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
-    int RetValue, i, k, iBit = 0;
-    assert( Gia_ManPiNum(pAig) == p->nPis );
-    Gia_ManCleanMark0(pAig);
-//    Gia_ManForEachRo( pAig, pObj, i )
-//       pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
-    iBit = p->nRegs;
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-        Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
-        Gia_ManForEachAnd( pAig, pObj, k )
-            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
-                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
-        Gia_ManForEachCo( pAig, pObj, k )
-            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
-        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
-            pObjRo->fMark0 = pObjRi->fMark0;
-    }
-    assert( iBit == p->nBits );
-    // figure out the number of failed output
-    RetValue = -1;
-//    for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
-    for ( i = nOutputs; i < Gia_ManPoNum(pAig); i++ )
-    {
-        if ( Gia_ManPo(pAig, i)->fMark0 )
-        {
-            RetValue = i;
-            break;
-        }
-    }
-    Gia_ManCleanMark0(pAig);
-    return RetValue;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Complements the constraint outputs.]
 
   Description []
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index b9e7fde7..83399eb8 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -9,6 +9,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAiger.c \
     src/aig/gia/giaBidec.c \
     src/aig/gia/giaCCof.c \
+    src/aig/gia/giaCex.c \
     src/aig/gia/giaCof.c \
     src/aig/gia/giaCSatOld.c \
     src/aig/gia/giaCSat.c \