Version abc80130

1 files changed, 0 insertions, 115 deletions

diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
deleted file mode 100644
index af6d237b..00000000
--- a/src/base/abci/abcBmc.c
+++ /dev/null
@@ -1,115 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcBmc.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Performs bounded model check.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "ivy.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc );
-
-static void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose )
-{
-    Ivy_FraigParams_t Params, * pParams = &Params; 
-    Ivy_Man_t * pMan, * pFrames, * pFraig;
-    Vec_Ptr_t * vMapping;
-    // convert to IVY manager
-    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
-    // generate timeframes
-    pFrames = Ivy_ManFrames( pMan, Abc_NtkLatchNum(pNtk), nFrames, fInit, &vMapping );
-    // fraig the timeframes
-    Ivy_FraigParamsDefault( pParams );
-    pParams->nBTLimitNode = ABC_INFINITY;
-    pParams->fVerbose = 0;
-    pParams->fProve = 0;
-    pFraig = Ivy_FraigPerform( pFrames, pParams );
-printf( "Frames have %6d nodes.  ", Ivy_ManNodeNum(pFrames) );
-printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
-    // report the classes
-//    if ( fVerbose )
-//        Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
-    // free stuff
-    Vec_PtrFree( vMapping );
-    Ivy_ManStop( pFraig );
-    Ivy_ManStop( pFrames );
-    Ivy_ManStop( pMan );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames )
-{
-    Ivy_Obj_t * pFirst1, * pFirst2, * pFirst3;
-    int i, f, nIdMax, Prev2, Prev3;
-    nIdMax = Ivy_ManObjIdMax(pMan);
-    // check what is the number of nodes in each frame
-    Prev2 = Prev3 = 0;
-    for ( f = 0; f < nFrames; f++ )
-    {
-        Ivy_ManForEachNode( pMan, pFirst1, i )
-        {
-            pFirst2 = Ivy_Regular( Vec_PtrEntry(vMapping, f * nIdMax + pFirst1->Id) );
-            if ( Ivy_ObjIsConst1(pFirst2) || pFirst2->Type == 0 )
-                continue;
-            pFirst3 = Ivy_Regular( pFirst2->pEquiv );
-            if ( Ivy_ObjIsConst1(pFirst3) || pFirst3->Type == 0 )
-                continue;
-            break;
-        }
-        if ( f )
-            printf( "Frame %3d :  Strash = %5d  Fraig = %5d\n", f, pFirst2->Id - Prev2, pFirst3->Id - Prev3 );
-        Prev2 = pFirst2->Id;
-        Prev3 = pFirst3->Id;   
-    }
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-