Experiments with resubstitution.

2 files changed, 366 insertions, 2 deletions

diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index cb10507e..564be76c 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -1361,6 +1361,7 @@ Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCex
         iPat += Gia_ManSimBitPackOne( nWordsMax, vSimsIn, vSimsCare, iPat, Vec_IntEntryP(vCexStore, iCur), Size );
         iCur += Size;
         assert( iPat <= nCexes );
+        Out = 0;
     }
     printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat );
     assert( iCur == Vec_IntSize(vCexStore) );
@@ -1550,7 +1551,7 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
         assert( Status >= -1 && Status <= 1 );
         Counts[Status+1]++;
     }
-    printf( "Total = %d : SAT = %d.  UNSAT = %d.  UNDEC = %d.\n", Gia_ManCoNum(p), Counts[1], Counts[2], Counts[0] );
+    printf( "Total = %d : SAT = %d.  UNSAT = %d.  UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] );
     if ( Counts[1] == 0 )
         printf( "There are no counter-examples.  No need for more simulation.\n" );
     else
@@ -1562,6 +1563,300 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
     }
     Vec_StrFree( vStatus );
     Vec_IntFree( vCexStore );
+    Vec_WrdFree( vSims );
+}
+
+
+
+
+
+typedef struct Gia_SimRsbMan_t_ Gia_SimRsbMan_t;
+struct Gia_SimRsbMan_t_
+{
+    Gia_Man_t *    pGia;
+    Vec_Int_t *    vTfo;
+    Vec_Int_t *    vCands;
+    Vec_Int_t *    vFanins;
+    Vec_Int_t *    vFanins2;
+    Vec_Wrd_t *    vSimsObj;
+    Vec_Wrd_t *    vSimsObj2;
+    int            nWords;
+    word *         pFunc[3];
+};
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_SimRsbMan_t * Gia_SimRsbAlloc( Gia_Man_t * pGia )
+{
+    Gia_SimRsbMan_t * p = ABC_CALLOC( Gia_SimRsbMan_t, 1 );
+    p->pGia      = pGia;
+    p->nWords    = Vec_WrdSize(pGia->vSimsPi) / Gia_ManCiNum(pGia); assert( Vec_WrdSize(pGia->vSimsPi) % Gia_ManCiNum(pGia) == 0 );
+    p->pFunc[0]  = ABC_CALLOC( word, p->nWords );
+    p->pFunc[1]  = ABC_CALLOC( word, p->nWords );
+    p->pFunc[2]  = ABC_CALLOC( word, p->nWords );
+    p->vTfo      = Vec_IntAlloc( 1000 );
+    p->vCands    = Vec_IntAlloc( 1000 );
+    p->vFanins   = Vec_IntAlloc( 10 );
+    p->vFanins2  = Vec_IntAlloc( 10 );
+    p->vSimsObj  = Gia_ManSimPatSim( pGia );
+    p->vSimsObj2 = Vec_WrdStart( Vec_WrdSize(p->vSimsObj) );
+    assert( p->nWords == Vec_WrdSize(p->vSimsObj) / Gia_ManObjNum(pGia) );
+    Gia_ManStaticFanoutStart( pGia );
+    return p;
+}
+void Gia_SimRsbFree( Gia_SimRsbMan_t * p )
+{
+    Gia_ManStaticFanoutStop( p->pGia );
+    Vec_IntFree( p->vTfo );
+    Vec_IntFree( p->vCands );
+    Vec_IntFree( p->vFanins );
+    Vec_IntFree( p->vFanins2 );
+    Vec_WrdFree( p->vSimsObj );
+    Vec_WrdFree( p->vSimsObj2 );
+    ABC_FREE( p->pFunc[0] );
+    ABC_FREE( p->pFunc[1] );
+    ABC_FREE( p->pFunc[2] );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SimRsbTfo_rec( Gia_Man_t * p, int iObj, int iFanout, Vec_Int_t * vTfo )
+{
+    int i, iFan;
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i )
+        if ( iFanout == -1 || iFan == iFanout )
+            Gia_SimRsbTfo_rec( p, iFan, -1, vTfo );
+    Vec_IntPush( vTfo, iObj );
+}
+Vec_Int_t * Gia_SimRsbTfo( Gia_SimRsbMan_t * p, int iObj, int iFanout )
+{
+    assert( iObj > 0 );
+    Vec_IntClear( p->vTfo );
+    Gia_ManIncrementTravId( p->pGia );
+    Gia_SimRsbTfo_rec( p->pGia, iObj, iFanout, p->vTfo );
+    assert( Vec_IntEntryLast(p->vTfo) == iObj );
+    Vec_IntPop( p->vTfo );
+    Vec_IntReverseOrder( p->vTfo );
+    Vec_IntSort( p->vTfo, 0 );
+    return p->vTfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+word * Gia_SimRsbFunc( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins, int fOnSet )
+{
+    int nTruthWords = Abc_Truth6WordNum( Vec_IntSize(vFanins) );
+    word * pTruth   = ABC_CALLOC( word, nTruthWords ); 
+    word * pFunc    = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj );
+    word * pFanins[16] = {NULL};  int s, b, iMint, i, iFanin;
+    assert( Vec_IntSize(vFanins) <= 16 );
+    Vec_IntForEachEntry( vFanins, iFanin, i )
+        pFanins[i] = Vec_WrdEntryP( p->vSimsObj, p->nWords*iFanin );
+    for ( s = 0; s < 64*p->nWords; s++ )
+    {
+        if ( !Abc_TtGetBit(p->pFunc[2], s) || !Abc_TtGetBit(pFunc, s) == fOnSet )
+            continue;
+        iMint = 0;
+        for ( b = 0; b < Vec_IntSize(vFanins); b++ )
+            if ( Abc_TtGetBit(pFanins[b], s) )
+                iMint |= 1 << b;
+        Abc_TtSetBit( pTruth, iMint );
+    }
+    return pTruth;
+}
+int Gia_SimRsbResubVerify( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vFanins )
+{
+    word * pTruth0 = Gia_SimRsbFunc( p, iObj, p->vFanins, 0 );
+    word * pTruth1 = Gia_SimRsbFunc( p, iObj, p->vFanins, 1 );
+    int Res = !Abc_TtIntersect( pTruth0, pTruth1, p->nWords, 0 );
+    ABC_FREE( pTruth0 );
+    ABC_FREE( pTruth1 );
+    return Res;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_SimRsbSimAndCareSet( Gia_Man_t * p, int i, Gia_Obj_t * pObj, int nWords, Vec_Wrd_t * vSims, Vec_Wrd_t * vSims2 )
+{
+    word pComps[2] = { 0, ~(word)0 };
+    word Diff0 = pComps[Gia_ObjFaninC0(pObj)];
+    word Diff1 = pComps[Gia_ObjFaninC1(pObj)];
+    Vec_Wrd_t * vSims0 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) ? vSims2 : vSims;
+    Vec_Wrd_t * vSims1 = Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ? vSims2 : vSims;
+    word * pSims0 = Vec_WrdEntryP( vSims0, nWords*Gia_ObjFaninId0(pObj, i) );
+    word * pSims1 = Vec_WrdEntryP( vSims1, nWords*Gia_ObjFaninId1(pObj, i) );
+    word * pSims2 = Vec_WrdEntryP( vSims2, nWords*i ); int w;
+    for ( w = 0; w < nWords; w++ )
+        pSims2[w] = (pSims0[w] ^ Diff0) & (pSims1[w] ^ Diff1);
+}
+word * Gia_SimRsbCareSet( Gia_SimRsbMan_t * p, int iObj, Vec_Int_t * vTfo )
+{
+    word * pSims  = Vec_WrdEntryP( p->vSimsObj,  p->nWords*iObj );
+    word * pSims2 = Vec_WrdEntryP( p->vSimsObj2, p->nWords*iObj );  int iNode, i;
+    Abc_TtCopy( pSims2, pSims, p->nWords, 1 );
+    Abc_TtClear( p->pFunc[2], p->nWords );
+    Vec_IntForEachEntry( vTfo, iNode, i )
+    {
+        Gia_Obj_t * pNode = Gia_ManObj(p->pGia, iNode);
+        if ( Gia_ObjIsAnd(pNode) )
+            Gia_SimRsbSimAndCareSet( p->pGia, iNode, pNode, p->nWords, p->vSimsObj, p->vSimsObj2 );
+        else if ( Gia_ObjIsCo(pNode) )
+        {
+            word * pSimsA = Vec_WrdEntryP( p->vSimsObj,  p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) );
+            word * pSimsB = Vec_WrdEntryP( p->vSimsObj2, p->nWords*Gia_ObjFaninId0p(p->pGia, pNode) );
+            Abc_TtOrXor( p->pFunc[2], pSimsA, pSimsB, p->nWords );
+        }
+        else assert( 0 );
+    }
+    return p->pFunc[2];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ObjSimCollect( Gia_SimRsbMan_t * p )
+{
+    int i, k, iTemp, iFanout;
+    Vec_IntClear( p->vFanins2 );
+    assert( Vec_IntSize(p->vFanins) > 0 );
+    Vec_IntForEachEntry( p->vFanins, iTemp, i )
+    {
+        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iTemp );
+        if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId0(pObj, iTemp) ) )
+            Vec_IntPush( p->vFanins2, Gia_ObjFaninId0(pObj, iTemp) );
+        if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsTravIdCurrentId( p->pGia, Gia_ObjFaninId1(pObj, iTemp) ) )
+            Vec_IntPush( p->vFanins2, Gia_ObjFaninId1(pObj, iTemp) );
+        Gia_ObjForEachFanoutStaticId( p->pGia, iTemp, iFanout, k )
+            if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanout)) && !Gia_ObjIsTravIdCurrentId( p->pGia, iFanout ) )
+                Vec_IntPush( p->vFanins2, iFanout );
+    }
+}
+Vec_Int_t * Gia_ObjSimCands( Gia_SimRsbMan_t * p, int iObj, int nCands )
+{
+    assert( iObj > 0 );
+    assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) );
+    Vec_IntClear( p->vCands );
+    Vec_IntFill( p->vFanins, 1, iObj );
+    while ( Vec_IntSize(p->vFanins) > 0 && Vec_IntSize(p->vCands) < nCands )
+    {
+        int i, iTemp;
+        Vec_IntForEachEntry( p->vFanins, iTemp, i )
+            Gia_ObjSetTravIdCurrentId( p->pGia, iTemp );
+        Gia_ObjSimCollect( p ); // p->vFanins -> p->vFanins2
+        Vec_IntAppend( p->vCands, p->vFanins2 );
+        ABC_SWAP( Vec_Int_t *, p->vFanins, p->vFanins2 );
+    }
+    assert( Vec_IntSize(p->vFanins) == 0 || Vec_IntSize(p->vCands) >= nCands );
+    if ( Vec_IntSize(p->vCands) > nCands )
+        Vec_IntShrink( p->vCands, nCands );
+    return p->vCands;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjSimRsb( Gia_SimRsbMan_t * p, int iObj, int nCands, int fVerbose, int * pnBufs, int * pnInvs )
+{
+    int i, iCand, RetValue = 0;
+    Vec_Int_t * vTfo   = Gia_SimRsbTfo( p, iObj, -1 );
+    word * pCareSet    = Gia_SimRsbCareSet( p, iObj, vTfo );
+    word * pFunc       = Vec_WrdEntryP( p->vSimsObj, p->nWords*iObj );
+    Vec_Int_t * vCands = Gia_ObjSimCands( p, iObj, nCands );
+    Abc_TtAndSharp( p->pFunc[0], pCareSet, pFunc, p->nWords, 1 );
+    Abc_TtAndSharp( p->pFunc[1], pCareSet, pFunc, p->nWords, 0 );
+
+/*
+printf( "Considering node %d with %d candidates:\n", iObj, Vec_IntSize(vCands) );
+Vec_IntPrint( vTfo );
+Vec_IntPrint( vCands );
+Extra_PrintBinary( stdout, (unsigned *)pCareSet,    64 );  printf( "\n" );
+Extra_PrintBinary( stdout, (unsigned *)pFunc,       64 );  printf( "\n" );
+Extra_PrintBinary( stdout, (unsigned *)p->pFunc[0], 64 );  printf( "\n" );
+Extra_PrintBinary( stdout, (unsigned *)p->pFunc[1], 64 );  printf( "\n" );
+*/
+    Vec_IntForEachEntry( vCands, iCand, i )
+    {
+        word * pDiv = Vec_WrdEntryP( p->vSimsObj, p->nWords*iCand );
+        if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 0) &&
+             !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 1) )
+            { (*pnBufs)++; if ( fVerbose ) printf( "Level %3d : %d = buf(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; }
+        if ( !Abc_TtIntersect(pDiv, p->pFunc[0], p->nWords, 1) &&
+             !Abc_TtIntersect(pDiv, p->pFunc[1], p->nWords, 0) )
+            { (*pnInvs)++; if ( fVerbose ) printf( "Level %3d : %d = inv(%d)\n", Gia_ObjLevelId(p->pGia, iObj), iObj, iCand ); RetValue = 1; }
+    }
+    return RetValue;
+}
+
+int Gia_ManSimRsb( Gia_Man_t * pGia, int nCands, int fVerbose )
+{
+    Gia_Obj_t * pObj; int iObj, nCount = 0, nBufs = 0, nInvs = 0;
+    Gia_SimRsbMan_t * p = Gia_SimRsbAlloc( pGia );
+    assert( pGia->vSimsPi != NULL );
+    Gia_ManLevelNum( pGia );
+    Gia_ManForEachAnd( pGia, pObj, iObj )
+        //if ( iObj == 6 )
+        nCount += Gia_ObjSimRsb( p, iObj, nCands, fVerbose, &nBufs, &nInvs );
+    printf( "Resubstitution is possible for %d nodes (%.2f %% out of %d) (Bufs = %d Invs = %d)\n", 
+        nCount, 100.0*nCount/Gia_ManAndNum(pGia), Gia_ManAndNum(pGia), nBufs, nInvs );
+    Gia_SimRsbFree( p );
+    return nCount;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f6fc7ea6..6a852bf7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -414,6 +414,7 @@ static int Abc_CommandAbc9Sim3               ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9ReadSim            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9WriteSim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SimPat             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SimRsb             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Resim              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SpecI              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Equiv              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1126,6 +1127,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_sim",     Abc_CommandAbc9ReadSim,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&write_sim",    Abc_CommandAbc9WriteSim,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&simpat",       Abc_CommandAbc9SimPat,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&simrsb",       Abc_CommandAbc9SimRsb,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&resim",        Abc_CommandAbc9Resim,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&speci",        Abc_CommandAbc9SpecI,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&equiv",        Abc_CommandAbc9Equiv,        0 );
@@ -32687,7 +32689,7 @@ int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia->vSimsPi == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9WriteSim(): Does not have simulation information available.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9SimPat(): Does not have simulation information available.\n" );
         return 0;
     }
     Gia_ManSimPat( pAbc->pGia, nWords, fVerbose );
@@ -32713,6 +32715,73 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9SimRsb( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManSimRsb( Gia_Man_t * p, int nCands, int fVerbose );
+    int c, nCands = 32, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCands = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCands < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SimRsb(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SimRsb(): This command works only for combinational AIGs.\n" );
+        return 0;
+    }
+    if ( pAbc->pGia->vSimsPi == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SimRsb(): Does not have simulation information available.\n" );
+        return 0;
+    }
+    Gia_ManSimRsb( pAbc->pGia, nCands, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &simrsb [-N num] [-vh]\n" );
+    Abc_Print( -2, "\t         performs resubstitution\n" );
+    Abc_Print( -2, "\t-C num : the number of candidates to try [default = %d]\n", nCands );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Resim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cec_ParSim_t Pars, * pPars = &Pars;