Version abc80927

1 files changed, 311 insertions, 0 deletions

diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
new file mode 100644
index 00000000..48a26a3c
--- /dev/null
+++ b/src/aig/saig/saigAbs.c
@@ -0,0 +1,311 @@
+/**CFile****************************************************************
+
+  FileName    [saigAbs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Proof-based abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+#include "cnf.h"
+#include "satSolver.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Saig_ObjFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i )                       { return ppMap[nFrames*pObj->Id + i];  }
+static inline void        Saig_ObjSetFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + i] = pNode; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for BMC.]
+
+  Description [The resulting manager is combinational. The only PO is
+  the output of the last frame.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** pppMap )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t ** ppMap;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    // start the mapping
+    ppMap = *pppMap = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) * nFrames );
+    // start the manager
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+    {
+        pObj->pData = Aig_ManConst0( pFrames );
+        Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData );
+    }
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // map the constant node
+        Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+        Saig_ObjSetFrame( ppMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pAig)->pData );
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+        }
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+        }
+        // create POs for this frame
+        if ( f == nFrames - 1 )
+        {
+            Saig_ManForEachPo( pAig, pObj, i )
+            {
+                pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+                Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+            }
+            break;
+        }
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+        {
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+        }
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+        {
+            pObjLo->pData = pObjLi->pData;
+            Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData );
+        }
+    }
+    Aig_ManCleanup( pFrames );
+    // remove mapping for the nodes that are no longer there
+    for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ )
+        if ( ppMap[i] && Aig_ObjIsNone( Aig_Regular(ppMap[i]) ) )
+            ppMap[i] = NULL;
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the set of variables involved in the UNSAT core.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nConfMax, int fVerbose )
+{
+    void * pSatCnf; 
+    Intp_Man_t * pManProof;
+    sat_solver * pSat;
+    Vec_Int_t * vCore;
+    int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars;
+    int i, RetValue;
+    // create the SAT solver
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat ); 
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+        {
+            printf( "The BMC problem is trivially UNSAT.\n" );
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    sat_solver_store_mark_roots( pSat ); 
+    // solve the problem
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
+    if ( RetValue == l_Undef )
+    {
+        printf( "Conflict limit is reached.\n" );
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+    if ( RetValue == l_True )
+    {
+        printf( "The BMC problem is SAT.\n" );
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+    printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
+    assert( RetValue == l_False );
+    pSatCnf = sat_solver_store_release( pSat ); 
+    sat_solver_delete( pSat );
+    // derive the UNSAT core
+    pManProof = Intp_ManAlloc();
+    vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose );
+    Intp_ManFree( pManProof );
+    Sto_ManFree( pSatCnf );
+    // derive the set of variables on which the core depends
+    // collect the variable numbers
+    nVars = 0;
+    pVars = ALLOC( int, pCnf->nVars );
+    memset( pVars, 0, sizeof(int) * pCnf->nVars );
+    Vec_IntForEachEntry( vCore, iClause, i )
+    {
+        pClause1 = pCnf->pClauses[iClause];
+        pClause2 = pCnf->pClauses[iClause+1];
+        for ( pLit = pClause1; pLit < pClause2; pLit++ )
+        {
+            if ( pVars[ (*pLit) >> 1 ] == 0 )
+                nVars++;
+            pVars[ (*pLit) >> 1 ] = 1;
+            if ( fVerbose )
+            printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
+        }
+        if ( fVerbose )
+        printf( "\n" );
+    }
+    Vec_IntFree( vCore );
+    return pVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels nodes with the given CNF variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iVar )
+{
+    int iVarThis = pCnf->pVarNums[pObj->Id];
+    if ( iVarThis >= 0 && iVarThis != iVar )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin0(pObj), pCnf, iVar );
+    Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin1(pObj), pCnf, iVar );
+    pCnf->pVarNums[pObj->Id] = iVar;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose )
+{
+    Cnf_Dat_t * pCnf;
+    Vec_Int_t * vFlops;
+    Aig_Man_t * pFrames, * pResult;
+    Aig_Obj_t ** ppAigToFrames;
+    Aig_Obj_t * pObj, * pObjFrame;
+    int f, i, * pUnsatCoreVars, clk = clock();
+    assert( Saig_ManPoNum(p) == 1 );
+    Aig_ManSetPioNumbers( p );
+    if ( fVerbose )
+        printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
+    // create the timeframes
+    pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames );
+    // convert them into CNF
+//    pCnf = Cnf_Derive( pFrames, 0 );
+    pCnf = Cnf_DeriveSimple( pFrames, 0 );
+    // collect CNF variables involved in UNSAT core
+    pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, nConfMax, 0 );
+    if ( pUnsatCoreVars == NULL )
+    {
+        Aig_ManStop( pFrames );
+        Cnf_DataFree( pCnf );
+        return NULL;
+    }
+    if ( fVerbose )
+    {
+        int Counter = 0;
+        for ( i = 0; i < pCnf->nVars; i++ )
+            Counter += pUnsatCoreVars[i];
+        printf( "The number of variables in the UNSAT core is %d (out of %d).\n", Counter, pCnf->nVars );
+    }
+    // map other nodes into existing CNF variables
+    Aig_ManForEachNode( pFrames, pObj, i )
+        if ( pCnf->pVarNums[pObj->Id] >= 0 )
+            Saig_ManMarkIntoPresentVars_rec( pObj, pCnf, pCnf->pVarNums[pObj->Id] );
+    // collect relevant registers
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Saig_ManForEachLo( p, pObj, i )
+        {
+            pObjFrame = Saig_ObjFrame( ppAigToFrames, nFrames, pObj, f );
+            if ( pObjFrame == NULL )
+                continue;
+            pObjFrame = Aig_Regular(pObjFrame);
+            if ( Aig_ObjIsConst1( pObjFrame ) )
+                continue;
+            assert( pCnf->pVarNums[pObjFrame->Id] >= 0 );
+            if ( pUnsatCoreVars[ pCnf->pVarNums[pObjFrame->Id] ] )
+                pObj->fMarkA = 1;
+        }
+    }
+    // collect the flops
+    vFlops = Vec_IntAlloc( 1000 );
+    Saig_ManForEachLo( p, pObj, i )
+        if ( pObj->fMarkA )
+        {
+            pObj->fMarkA = 0;
+            Vec_IntPush( vFlops, i );
+        }
+    if ( fVerbose )
+    {
+        printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
+        PRT( "Time", clock() - clk );
+    }
+    // create the resulting AIG
+    pResult = Saig_ManAbstraction( p, vFlops );
+    // cleanup
+    Aig_ManStop( pFrames );
+    Cnf_DataFree( pCnf );
+    free( ppAigToFrames );
+    free( pUnsatCoreVars );
+    Vec_IntFree( vFlops );
+    return pResult;
+
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+