Experiments with simulation.

abclib.dsp

@@ -5539,6 +5539,10 @@ SOURCE=.\src\proof\cec\cecSeq.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\cec\cecSim.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\cec\cecSolve.c
 # End Source File
 # Begin Source File

src/aig/gia/gia.h

@@ -479,6 +479,7 @@ static inline int          Gia_ObjValue( Gia_Obj_t * pObj )                    {
 static inline void         Gia_ObjSetValue( Gia_Obj_t * pObj, int i )          { pObj->Value = i;                                            }
 static inline int          Gia_ObjPhase( Gia_Obj_t * pObj )                    { return pObj->fPhase;                                        }
 static inline int          Gia_ObjPhaseReal( Gia_Obj_t * pObj )                { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj);  }
+static inline int          Gia_ObjPhaseDiff( Gia_Man_t * p, int i, int k )     { return Gia_ManObj(p, i)->fPhase ^ Gia_ManObj(p, k)->fPhase; }
 
 static inline int          Gia_ObjIsTerm( Gia_Obj_t * pObj )                   { return pObj->fTerm;                             } 
 static inline int          Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj )            { return!pObj->fTerm;                             } 

src/misc/util/utilTruth.h

@@ -216,6 +216,12 @@ static inline void Abc_TtMask( word * pTruth, int nWords, int nBits )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Abc_TtVec( word * pOut, int nWords, word Entry )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] = Entry;
+}
 static inline void Abc_TtConst( word * pOut, int nWords, int fConst1 )
 {
     int w;
@@ -316,6 +322,12 @@ static inline void Abc_TtOrXor( word * pOut, word * pIn1, word * pIn2, int nWord
     for ( w = 0; w < nWords; w++ )
         pOut[w] |= pIn1[w] ^ pIn2[w];
 }
+static inline void Abc_TtOrAnd( word * pOut, word * pIn1, word * pIn2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pOut[w] |= pIn1[w] & pIn2[w];
+}
 static inline void Abc_TtXor( word * pOut, word * pIn1, word * pIn2, int nWords, int fCompl )
 {
     int w;

src/proof/cec/cecSim.c

@@ -6,7 +6,7 @@
 
   PackageName [Combinational equivalence checking.]
 
-  Synopsis    [Simulation manager.]
+  Synopsis    [Simulation.]
 
   Author      [Alan Mishchenko]
   
@@ -19,14 +19,40 @@
 ***********************************************************************/
 
 #include "cecInt.h"
+#include "aig/gia/giaAig.h"
+#include "misc/util/utilTruth.h"
 
-ABC_NAMESPACE_IMPL_START
 
+ABC_NAMESPACE_IMPL_START
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define SIM_RANDS    113
+
+typedef struct Cec_ManS_t_ Cec_ManS_t;
+struct Cec_ManS_t_
+{
+    int              nWords;
+    int              nLevelMax;
+    int              nLevelMin;
+    int              iRand;
+    Gia_Man_t *      pAig;       
+    Vec_Int_t *      vInputs;
+    Vec_Wec_t *      vLevels;
+    Vec_Wrd_t *      vSims;
+    word *           pTemp[4];
+    word             Rands[SIM_RANDS];
+    int              nSkipped;
+    int              nVisited;
+    int              nCexes;
+    abctime          clkSat;
+    abctime          clkUnsat;
+};
+
+static inline word * Cec_ManSSim( Cec_ManS_t * p, int iNode, int Value ) { return Vec_WrdEntryP(p->vSims, p->nWords*(iNode+iNode+Value)); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -36,12 +62,343 @@ ABC_NAMESPACE_IMPL_START
   Synopsis    []
 
   Description []
-  
+               
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
+Cec_ManS_t * Cec_ManSStart( Gia_Man_t * pAig, int nWords )
+{
+    Cec_ManS_t * p; int i;
+    p = ABC_ALLOC( Cec_ManS_t, 1 );
+    memset( p, 0, sizeof(Cec_ManS_t) );
+    p->nWords    = nWords;
+    p->pAig      = pAig;
+    p->vInputs   = Vec_IntAlloc( 100 );
+    p->vLevels   = Vec_WecStart( Gia_ManLevelNum(pAig) + 1 );
+    p->vSims     = Vec_WrdStart( Gia_ManObjNum(pAig) * nWords * 2 );
+    p->pTemp[0]  = ABC_ALLOC( word, 4*nWords );
+    for ( i = 1; i < 4; i++ )
+        p->pTemp[i] = p->pTemp[i-1] + nWords;
+    for ( i = 0; i < SIM_RANDS; i++ )
+        p->Rands[i] = Gia_ManRandomW(0);
+    return p;
+}
+void Cec_ManSStop( Cec_ManS_t * p )
+{
+    Vec_IntFree( p->vInputs );
+    Vec_WecFree( p->vLevels );
+    Vec_WrdFree( p->vSims );
+    ABC_FREE( p->pTemp[0] );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verify counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSVerify_rec( Gia_Man_t * p, int iObj )
+{
+    int Value0, Value1;
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    if ( iObj == 0 ) return 0;
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return pObj->fMark1;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    if ( Gia_ObjIsCi(pObj) )
+        return pObj->fMark1;
+    assert( Gia_ObjIsAnd(pObj) );
+    Value0 = Cec_ManSVerify_rec( p, Gia_ObjFaninId0(pObj, iObj) ) ^ Gia_ObjFaninC0(pObj);
+    Value1 = Cec_ManSVerify_rec( p, Gia_ObjFaninId1(pObj, iObj) ) ^ Gia_ObjFaninC1(pObj);
+    return pObj->fMark1 = Gia_ObjIsXor(pObj) ? Value0 ^ Value1 : Value0 & Value1;
+}
+void Cec_ManSVerifyTwo( Gia_Man_t * p, int iObj0, int iObj1 )
+{
+    int Value0, Value1;
+    Gia_ManIncrementTravId( p );
+    Value0 = Cec_ManSVerify_rec( p, iObj0 );
+    Value1 = Cec_ManSVerify_rec( p, iObj1 );
+    if ( (Value0 ^ Value1) == Gia_ObjPhaseDiff(p, iObj0, iObj1) )
+        printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 );
+//    else
+//        printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );;
+}
+void Cec_ManSVerify( Cec_ManS_t * p, int iObj0, int iObj1 )
+{
+    int fDoVerify = 0;
+    int w, i, iObj, nCares;
+    word * pCare = Vec_WrdArray(p->vSims);
+    if ( Vec_IntSize(p->vInputs) == 0 )
+    {
+        printf( "No primary inputs.\n" );
+        return;
+    }
+    Vec_IntForEachEntry( p->vInputs, iObj, i )
+    {
+        word * pSim_0 = Cec_ManSSim( p, iObj, 0 );
+        word * pSim_1 = Cec_ManSSim( p, iObj, 1 );
+        if ( p->nWords == 1 )
+            pCare[0] |= pSim_0[0] & pSim_1[0];
+        else
+            Abc_TtOrAnd( pCare, pSim_0, pSim_1, p->nWords );
+    }
+    nCares = Abc_TtCountOnesVec( pCare, p->nWords );
+    if ( nCares == 64*p->nWords )
+    {
+        printf( "No CEXes.\n" );
+        return;
+    }
+    assert( Vec_IntSize(p->vInputs) > 0 );
+    for ( w = 0; w < 64*p->nWords; w++ )
+    {
+        if ( Abc_TtGetBit(pCare, w) )
+            continue;
+        if ( !fDoVerify )
+            continue;
+        Vec_IntForEachEntry( p->vInputs, iObj, i )
+            Gia_ManObj(p->pAig, iObj)->fMark1 = Abc_TtGetBit( Cec_ManSSim(p, iObj, 1), w );
+        Cec_ManSVerifyTwo( p->pAig, iObj0, iObj1 );
+    }
+    printf( "Considered %d CEXes of nodes %d and %d.\n", 64*p->nWords - nCares, iObj0, iObj1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSRunImply( Cec_ManS_t * p, int iNode )
+{
+    Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode );
+    if ( Gia_ObjIsAnd(pNode) )
+    {
+        int iFan0 = Gia_ObjFaninId0( pNode, iNode );
+        int iFan1 = Gia_ObjFaninId1( pNode, iNode );
+        word * pSim__ = Cec_ManSSim( p, 0, 0 );
+        word * pSim_0 = Cec_ManSSim( p, iNode, 0 );
+        word * pSim_1 = Cec_ManSSim( p, iNode, 1 );
+        word * pSim00 = Cec_ManSSim( p, iFan0,  Gia_ObjFaninC0(pNode) );
+        word * pSim01 = Cec_ManSSim( p, iFan0, !Gia_ObjFaninC0(pNode) );
+        word * pSim10 = Cec_ManSSim( p, iFan1,  Gia_ObjFaninC1(pNode) );
+        word * pSim11 = Cec_ManSSim( p, iFan1, !Gia_ObjFaninC1(pNode) );
+        if ( p->nWords == 1 )
+        {
+            pSim_0[0] |= pSim00[0] | pSim10[0];
+            pSim_1[0] |= pSim01[0] & pSim11[0];
+            pSim__[0] |= pSim_0[0] & pSim_1[0];
+            pSim_0[0] &= ~pSim__[0];
+            pSim_1[0] &= ~pSim__[0];
+        }
+        else
+        {
+            Abc_TtOr( pSim_0, pSim_0, pSim00, p->nWords );
+            Abc_TtOr( pSim_0, pSim_0, pSim10, p->nWords );
+            Abc_TtOrAnd( pSim_1, pSim01, pSim11, p->nWords );
+            Abc_TtOrAnd( pSim__, pSim_0, pSim_1, p->nWords );
+            Abc_TtAndSharp( pSim_0, pSim_0, pSim__, p->nWords, 1 );
+            Abc_TtAndSharp( pSim_1, pSim_1, pSim__, p->nWords, 1 );
+        }
+    }
+}
+int Cec_ManSRunPropagate( Cec_ManS_t * p, int iNode )
+{
+    Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode );
+    int iFan0 = Gia_ObjFaninId0( pNode, iNode );
+    int iFan1 = Gia_ObjFaninId1( pNode, iNode );
+    word * pSim_0 = Cec_ManSSim( p, iNode, 0 );
+    word * pSim_1 = Cec_ManSSim( p, iNode, 1 );
+    if ( Abc_TtIsConst0(pSim_0, p->nWords) && Abc_TtIsConst0(pSim_1, p->nWords) )
+    {
+        p->nSkipped++;
+        return 0;
+    }
+    p->nVisited++;
+    Cec_ManSRunImply( p, iFan0 );
+    Cec_ManSRunImply( p, iFan1 );
+    {
+        word * pSim__ = Cec_ManSSim( p, 0, 0 );
+        word * pSim00 = Cec_ManSSim( p, iFan0,  Gia_ObjFaninC0(pNode) );
+        word * pSim01 = Cec_ManSSim( p, iFan0, !Gia_ObjFaninC0(pNode) );
+        word * pSim10 = Cec_ManSSim( p, iFan1,  Gia_ObjFaninC1(pNode) );
+        word * pSim11 = Cec_ManSSim( p, iFan1, !Gia_ObjFaninC1(pNode) );
+        p->iRand = p->iRand == SIM_RANDS-1 ? 0 : p->iRand + 1;
+        if ( p->nWords == 1 )
+        {
+            pSim__[0] |= pSim_0[0] &  pSim01[0] & pSim11[0];
+            pSim__[0] |= pSim_1[0] & (pSim00[0] | pSim10[0]);
+
+            pSim00[0] |= pSim_0[0] & ~pSim__[0] & (pSim01[0] | ~p->Rands[p->iRand]);
+            pSim10[0] |= pSim_0[0] & ~pSim__[0] & (pSim11[0] |  p->Rands[p->iRand]);
+
+            pSim01[0] |= pSim_1[0] & ~pSim__[0];
+            pSim11[0] |= pSim_1[0] & ~pSim__[0];
+
+            pSim__[0] |= pSim00[0] & pSim01[0];
+            pSim__[0] |= pSim10[0] & pSim11[0];
+        }
+        else
+        {
+            int w;
+
+            Abc_TtAnd( p->pTemp[0], pSim01, pSim11, p->nWords, 0 );
+            Abc_TtOrAnd( pSim__, pSim_0, p->pTemp[0], p->nWords );
+
+            Abc_TtOr( p->pTemp[0], pSim00, pSim10, p->nWords );
+            Abc_TtOrAnd( pSim__, pSim_1, p->pTemp[0], p->nWords );
+
+            //Abc_TtVec( p->pTemp[0], p->nWords, p->Rands[p->iRand] );
+            for ( w = 0; w < p->nWords; w++ )
+                p->pTemp[0][w] = p->Rands[(p->iRand + w) % SIM_RANDS];
+
+            Abc_TtAndCompl( p->pTemp[1], pSim01, 1, p->pTemp[0], 0, p->nWords );
+            Abc_TtAndCompl( p->pTemp[2], pSim__, 1, p->pTemp[1], 1, p->nWords );
+            Abc_TtOrAnd( pSim00, pSim_0, p->pTemp[2], p->nWords );
+
+            Abc_TtAndCompl( p->pTemp[1], pSim11, 1, p->pTemp[0], 1, p->nWords );
+            Abc_TtAndCompl( p->pTemp[2], pSim__, 1, p->pTemp[1], 1, p->nWords );
+            Abc_TtOrAnd( pSim10, pSim_0, p->pTemp[2], p->nWords );
+
+            Abc_TtAndSharp( p->pTemp[0], pSim_1, pSim__, p->nWords, 1 );
+            Abc_TtOr( pSim01, pSim01, p->pTemp[0], p->nWords );
+            Abc_TtOr( pSim11, pSim11, p->pTemp[0], p->nWords );
+
+            Abc_TtOrAnd( pSim__, pSim00, pSim01, p->nWords );
+            Abc_TtOrAnd( pSim__, pSim10, pSim11, p->nWords );
+        }
+    }
+    return 1;
+}
+void Cec_ManSInsert( Cec_ManS_t * p, int iNode )
+{
+    Gia_Obj_t * pNode; int Level;
+    assert( iNode > 0 );
+    if ( Gia_ObjIsTravIdCurrentId(p->pAig, iNode) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p->pAig, iNode);
+    pNode = Gia_ManObj( p->pAig, iNode );
+    if ( Gia_ObjIsCi(pNode) )
+    {
+        Vec_IntPush( p->vInputs, iNode );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pNode) );
+    Level = Gia_ObjLevelId( p->pAig, iNode );
+    assert( Level > 0 );
+    Vec_WecPush( p->vLevels, Level, iNode );
+    p->nLevelMax = Abc_MaxInt( p->nLevelMax, Level );
+    p->nLevelMin = Abc_MinInt( p->nLevelMin, Level );
+    assert( p->nLevelMin <= p->nLevelMax );
+}
+int Cec_ManSRunSimInt( Cec_ManS_t * p )
+{
+    Vec_Int_t * vLevel; 
+    int i, k, iNode, fSolved = 0;
+    Vec_WecForEachLevelReverseStartStop( p->vLevels, vLevel, i, p->nLevelMax+1, p->nLevelMin )
+    {
+        Vec_IntForEachEntry( vLevel, iNode, k )
+        {
+            Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode );
+            if ( !fSolved && Cec_ManSRunPropagate( p, iNode ) )
+            {
+                Cec_ManSInsert( p, Gia_ObjFaninId0(pNode, iNode) );
+                Cec_ManSInsert( p, Gia_ObjFaninId1(pNode, iNode) );
+                if ( Abc_TtIsConst1(Vec_WrdArray(p->vSims), p->nWords) )
+                    fSolved = 1;
+            }
+            Abc_TtClear( Cec_ManSSim(p, iNode, 0), 2*p->nWords );
+        }
+        Vec_IntClear( vLevel );
+    }
+    //Vec_WecForEachLevel( p->vLevels, vLevel, i )
+    //    assert( Vec_IntSize(vLevel) == 0 );
+    return fSolved;
+}
+int Cec_ManSRunSim( Cec_ManS_t * p, int iNode0, int iNode1 )
+{
+    abctime clk = Abc_Clock();
+    //Vec_Int_t * vLevel; 
+    int pNodes[2] = { iNode0, iNode1 };
+    int i, iNode, Status, fDiff = Gia_ObjPhaseDiff( p->pAig, iNode0, iNode1 );
+    word * pSim00 = Cec_ManSSim( p, iNode0, 0 );
+    word * pSim01 = Cec_ManSSim( p, iNode0, 1 );
+    word * pSim10 = Cec_ManSSim( p, iNode1,  fDiff );
+    word * pSim11 = Cec_ManSSim( p, iNode1, !fDiff );
+    Abc_TtClear( Vec_WrdArray(p->vSims), p->nWords );
+    //for ( i = 0; i < Vec_WrdSize(p->vSims); i++ )
+    //    assert( p->vSims->pArray[i] == 0 );
+    assert( Vec_IntSize(p->vInputs) == 0 );
+    if ( iNode0 == 0 )
+        Abc_TtFill( pSim11, p->nWords );
+    else
+    {
+        if ( p->nWords == 1 )
+        {
+            pSim00[0] = (word)0xFFFFFFFF;
+            pSim11[0] = (word)0xFFFFFFFF;
+            pSim01[0] = pSim00[0] << 32;
+            pSim10[0] = pSim11[0] << 32;
+        }
+        else
+        {
+            assert( p->nWords % 2 == 0 );
+            Abc_TtFill( pSim00,               p->nWords/2 );
+            Abc_TtFill( pSim11,               p->nWords/2 );
+            Abc_TtFill( pSim01 + p->nWords/2, p->nWords/2 );
+            Abc_TtFill( pSim10 + p->nWords/2, p->nWords/2 );
+        }
+    }
+    p->nLevelMin = ABC_INFINITY;
+    p->nLevelMax = 0;
+    Gia_ManIncrementTravId( p->pAig );
+    if ( iNode0 )
+    Cec_ManSInsert( p, iNode0 );
+    Cec_ManSInsert( p, iNode1 );
+    p->nSkipped = p->nVisited = 0;
+    Status = Cec_ManSRunSimInt( p );
+    if ( Status == 0 )
+        p->clkSat += Abc_Clock() - clk;
+    else
+        p->clkUnsat += Abc_Clock() - clk;
+//    if ( Status == 0 )
+//        printf( "Solving %6d and %6d.  Skipped = %6d.  Visited = %6d.  Cone = %6d.  Min = %3d.  Max = %3d.\n", 
+//            iNode0, iNode1, p->nSkipped, p->nVisited, Gia_ManConeSize(p->pAig, pNodes, 2), p->nLevelMin, p->nLevelMax );
+    if ( Status == 0 )
+        Cec_ManSVerify( p, iNode0, iNode1 ), p->nCexes++;
+    Vec_IntForEachEntry( p->vInputs, iNode, i )
+        Abc_TtClear( Cec_ManSSim(p, iNode, 0), 2*p->nWords );
+    Vec_IntClear( p->vInputs );
+    return Status;
+}
+void Cec_ManSRunTest( Gia_Man_t * pAig )
+{
+    abctime clk = Abc_Clock();
+    Cec_ManS_t * p;
+    int i, k, nWords = 1;
+    Gia_ManRandomW( 1 );
+    p = Cec_ManSStart( pAig, nWords );
+    Gia_ManForEachClass0( p->pAig, i )
+        Gia_ClassForEachObj1( p->pAig, i, k )
+            Cec_ManSRunSim( p, i, k );
+    printf( "Detected %d CEXes.  ", p->nCexes );
+    Abc_PrintTime( 1, "Time ", Abc_Clock() - clk );
+    Abc_PrintTime( 1, "Sat  ", p->clkSat );
+    Abc_PrintTime( 1, "Unsat", p->clkUnsat );
+    Cec_ManSStop( p );
+}
 
 
 ////////////////////////////////////////////////////////////////////////

src/proof/cec/module.make

@@ -10,6 +10,7 @@ SRC +=    src/proof/cec/cecCec.c \
     src/proof/cec/cecSatG.c \
     src/proof/cec/cecSatG2.c \
     src/proof/cec/cecSeq.c \
+    src/proof/cec/cecSim.c \
     src/proof/cec/cecSolve.c \
     src/proof/cec/cecSolveG.c \
     src/proof/cec/cecSplit.c \