Experimental implementation of BMC-related procedures.

4 files changed, 430 insertions, 0 deletions

diff --git a/abclib.dsp b/abclib.dsp
index ba457573..5559b243 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1479,6 +1479,10 @@ SOURCE=.\src\sat\bmc\bmcCexTools.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcChain.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcEco.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 37d96dcc..7bd2b617 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -428,6 +428,7 @@ static int Abc_CommandAbc9GroupProve         ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SplitProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9ChainBmc           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9BCore              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ICheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatTest            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1028,6 +1029,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&splitprove",   Abc_CommandAbc9SplitProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&chainbmc",     Abc_CommandAbc9ChainBmc,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bcore",        Abc_CommandAbc9BCore,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&icheck",       Abc_CommandAbc9ICheck,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sattest",      Abc_CommandAbc9SatTest,      0 );
@@ -35458,6 +35460,90 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9ChainBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Bmc_ChainTest( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose );
+    int nFrameMax    =  200;
+    int nConfMax     =    0;
+    int fVerbose     =    0;
+    int fVeryVerbose =    0;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrameMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrameMax < 0 )
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfMax < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ChainBmc(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( !Gia_ManRegNum(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ChainBmc(): The AIG is combinational.\n" );
+        return 0;
+    }
+    Bmc_ChainTest( pAbc->pGia, nFrameMax, nConfMax, fVerbose, fVeryVerbose );
+    //pAbc->Status  = ...;
+    //pAbc->nFrames = pPars->iFrame;
+    //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: &chainbmc [-FC <num>] [-vwh]\n" );
+    Abc_Print( -2, "\t           runs a specialized flavor of BMC\n" );
+    Abc_Print( -2, "\t-F <num> : the max number of timeframes (0 = unused) [default = %d]\n", nFrameMax );
+    Abc_Print( -2, "\t-C <num> : the max number of conflicts (0 = unused) [default = %d]\n", nConfMax );
+    Abc_Print( -2, "\t-v       : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggle printing even more information [default = %s]\n", fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9BCore( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
diff --git a/src/sat/bmc/bmcChain.c b/src/sat/bmc/bmcChain.c
new file mode 100644
index 00000000..d2a57d12
--- /dev/null
+++ b/src/sat/bmc/bmcChain.c
@@ -0,0 +1,339 @@
+/**CFile****************************************************************
+
+  FileName    [bmcChain.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Implementation of chain BMC.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcChain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "aig/gia/giaAig.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satSolver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Find the first failure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Bmc_ChainFailOneOutput( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose )
+{
+    int RetValue;
+    Abc_Cex_t * pCex = NULL;
+    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+    Saig_ParBmc_t Pars, * pPars = &Pars;
+    Saig_ParBmcSetDefaultParams( pPars );
+    pPars->nFramesMax = nFrameMax;
+    pPars->nConfLimit = nConfMax;
+    pPars->fVerbose   = fVeryVerbose;
+    RetValue = Saig_ManBmcScalable( pAig, pPars );
+    if ( RetValue == 0 ) // SAT
+    {
+        pCex = pAig->pSeqModel, pAig->pSeqModel = NULL;
+        if ( fVeryVerbose )
+            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, p->pName, pCex->iFrame );
+    }
+    else if ( fVeryVerbose )
+        Abc_Print( 1, "No output asserted in %d frames. Resource limit reached.\n", pPars->iFrame+2 );
+    Aig_ManStop( pAig );
+    return pCex;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Move GIA into the failing state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupWithInit( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+        {
+            pObj->Value = Gia_ManAppendCi( pNew );
+            pObj->Value = Abc_LitNotCond( pObj->Value, pObj->fMark0 );
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+            pObj->Value = Abc_LitNotCond( pObj->Value, pObj->fMark0 );
+            pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
+        }
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+Gia_Man_t * Gia_ManVerifyCexAndMove( Gia_Man_t * pGia, Abc_Cex_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Gia_ManCleanMark0(pGia);
+    Gia_ManForEachRo( pGia, pObj, i )
+        pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Gia_ManForEachPi( pGia, pObj, k )
+            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pGia, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pGia, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( iBit == p->nBits );
+    RetValue = Gia_ManPo(pGia, p->iPo)->fMark0;
+    assert( RetValue );
+    // set PI/PO values to zero and transfer RO values to RI
+    Gia_ManForEachPi( pGia, pObj, k )
+        pObj->fMark0 = 0;
+    Gia_ManForEachPo( pGia, pObj, k )
+        pObj->fMark0 = 0;
+    Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k )
+        pObjRi->fMark0 = pObjRo->fMark0;
+    // duplicate assuming CI/CO marks are set correctly
+    pNew = Gia_ManDupWithInit( pGia );
+    Gia_ManCleanMark0(pGia);
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find what outputs fail in this state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupPosAndPropagateInit( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;  int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsPi(p, pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = 0;
+        else if ( Gia_ObjIsPo(p, pObj) )
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManHashStop( pNew );
+    assert( Gia_ManPiNum(p) == Gia_ManPiNum(pNew) );
+    assert( Gia_ManPoNum(p) == Gia_ManPoNum(pNew) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+sat_solver * Gia_ManDeriveSatSolver( Gia_Man_t * p )
+{
+//    return Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    sat_solver * pSat;
+    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+    Cnf_Dat_t * pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
+    Aig_ManStop( pAig );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    Cnf_DataFree( pCnf );
+    assert( p->nRegs == 0 );
+    return pSat;
+}
+Vec_Int_t * Bmc_ChainFindFailedOutputs( Gia_Man_t * p )
+{
+    Vec_Int_t * vOutputs;
+    Gia_Man_t * pInit;
+    Gia_Obj_t * pObj;
+    sat_solver * pSat;
+    int i, Lit, status = 0;
+    // derive output logic cones
+    pInit = Gia_ManDupPosAndPropagateInit( p );
+    // derive SAT solver and test
+    pSat = Gia_ManDeriveSatSolver( pInit );
+    vOutputs = Vec_IntAlloc( 100 );
+    Gia_ManForEachPo( pInit, pObj, i )
+    {
+        if ( Gia_ObjFaninLit0p(pInit, pObj) == 0 )
+            continue;
+        Lit = Abc_Var2Lit( i+1, 0 );
+        status = sat_solver_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 );
+        if ( status == l_True )
+            Vec_IntPush( vOutputs, i );
+    }
+    Gia_ManStop( pInit );
+    sat_solver_delete( pSat );
+    return vOutputs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleanup AIG by removing COs replacing failed out by const0.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_ObjMakePoConst0( Gia_Man_t * p, Gia_Obj_t * pObj )
+{ 
+    assert( Gia_ObjIsCo(pObj) );
+    pObj->iDiff0 = Gia_ObjId( p, pObj );
+    pObj->fCompl0 = 0;
+}
+int Gia_ManCountNonConst0( Gia_Man_t * p )
+{ 
+    Gia_Obj_t * pObj;
+    int i, Count = 0;
+    Gia_ManForEachPo( p, pObj, i )
+        Count += (Gia_ObjFaninLit0p(p, pObj) != 0);
+    return Count;
+}
+Gia_Man_t * Bmc_ChainCleanup( Gia_Man_t * p, Vec_Int_t * vOutputs )
+{
+    int i, iOut;
+    Vec_IntForEachEntry( vOutputs, iOut, i )
+    {
+        Gia_Obj_t * pObj = Gia_ManPo( p, iOut );
+        assert( Gia_ObjFaninLit0p(p, pObj) != 0 );
+        Gia_ObjMakePoConst0( p, pObj );
+        assert( Gia_ObjFaninLit0p(p, pObj) == 0 );
+    }
+    return Gia_ManCleanup( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bmc_ChainTest( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int fVeryVerbose )
+{
+    int Iter, IterMax = 10000;
+    Gia_Man_t * pTemp, * pNew = Gia_ManDup(p);
+    Abc_Cex_t * pCex = NULL;
+    Vec_Int_t * vOutputs;
+    abctime clk = Abc_Clock(); 
+    int DepthTotal = 0;
+    for ( Iter = 0; Iter < IterMax; Iter++ )
+    {
+        if ( Gia_ManPoNum(pNew) == 0 )
+        {
+            if ( fVerbose )
+                printf( "Finished all POs.\n" );
+            break;
+        }
+        // run BMC till the first failure
+        pCex = Bmc_ChainFailOneOutput( pNew, nFrameMax, nConfMax, fVerbose, fVeryVerbose );
+        if ( pCex == NULL )
+        {
+            if ( fVerbose )
+                printf( "BMC could not detect a failed output in %d frames with %d conflicts.\n", nFrameMax, nConfMax );
+            break;
+        }
+        assert( !Iter || pCex->iFrame > 0 );
+        // move the AIG to the failure state
+        pNew = Gia_ManVerifyCexAndMove( pTemp = pNew, pCex );
+        Gia_ManStop( pTemp );
+        DepthTotal += pCex->iFrame;
+        // find outputs that fail in this state
+        vOutputs = Bmc_ChainFindFailedOutputs( pNew );
+        assert( Vec_IntFind(vOutputs, pCex->iPo) >= 0 );
+        Abc_CexFree( pCex );
+        // remove them from the AIG 
+        pNew = Bmc_ChainCleanup( pTemp = pNew, vOutputs );
+        Gia_ManStop( pTemp );
+        // perform sequential cleanup
+//        pNew = Gia_ManSeqStructSweep( pTemp = pNew, 0, 1, 0 );
+//        Gia_ManStop( pTemp );
+        // printout
+        if ( fVerbose )
+        {
+            int nNonConst = Gia_ManCountNonConst0(pNew);
+            printf( "Iter %4d : ",    Iter+1 );
+            printf( "Depth =%6d ",    DepthTotal );
+            printf( "FailPo =%6d ",   Vec_IntSize(vOutputs) );
+            printf( "UndefPo =%6d ",  nNonConst );
+            printf( "(%6.2f %%) ",    100.0 * nNonConst / Gia_ManPoNum(pNew) );
+            printf( "AIG = %8d  ",    Gia_ManAndNum(pNew) );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        }
+        Vec_IntFree( vOutputs );
+    }
+    printf( "Completed a CEX chain with %d segments, %d frames, and %d failed POs (out of %d). ", 
+        Iter, DepthTotal, Gia_ManPoNum(pNew) - Gia_ManCountNonConst0(pNew), Gia_ManPoNum(pNew) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Gia_ManStop( pNew );
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 72af4dc1..3de71902 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -10,6 +10,7 @@ SRC +=    src/sat/bmc/bmcBCore.c \
     src/sat/bmc/bmcCexMin1.c \
     src/sat/bmc/bmcCexMin2.c \
     src/sat/bmc/bmcCexTools.c \
+    src/sat/bmc/bmcChain.c \
     src/sat/bmc/bmcEco.c \
     src/sat/bmc/bmcFault.c \
     src/sat/bmc/bmcICheck.c \