Major restructuring of the code.

1 files changed, 0 insertions, 380 deletions

diff --git a/src/aig/cec/cecSynth.c b/src/aig/cec/cecSynth.c
deleted file mode 100644
index 52b50a43..00000000
--- a/src/aig/cec/cecSynth.c
+++ /dev/null
@@ -1,380 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cecSynth.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Combinational equivalence checking.]
-
-  Synopsis    [Partitioned sequential synthesis.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cecSynth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-#include "giaAig.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Populate sequential synthesis parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_SeqSynthesisSetDefaultParams( Cec_ParSeq_t * p )
-{
-    memset( p, 0, sizeof(Cec_ParSeq_t) );
-    p->fUseLcorr    =    0;  // enables latch correspondence
-    p->fUseScorr    =    0;  // enables signal correspondence
-    p->nBTLimit     = 1000;  // (scorr/lcorr) conflict limit at a node
-    p->nFrames      =    1;  // (scorr only) the number of timeframes
-    p->nLevelMax    =   -1;  // (scorr only) the max number of levels
-    p->fConsts      =    1;  // (scl only) merging constants
-    p->fEquivs      =    1;  // (scl only) merging equivalences
-    p->fUseMiniSat  =    0;  // enables MiniSat in lcorr/scorr
-    p->nMinDomSize  =  100;  // the size of minimum clock domain
-    p->fVeryVerbose =    0;  // verbose stats
-    p->fVerbose     =    0;  // verbose stats
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_SeqReadMinDomSize( Cec_ParSeq_t * p )
-{
-    return p->nMinDomSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_SeqReadVerbose( Cec_ParSeq_t * p )
-{
-    return p->fVerbose;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes partitioning of registers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManRegCreatePart( Gia_Man_t * p, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack )
-{
-    Gia_Man_t * pNew;
-    Gia_Obj_t * pObj;
-    Vec_Int_t * vNodes, * vRoots;
-    int i, iOut, nCountPis, nCountRegs;
-    int * pMapBack;
-    // collect/mark nodes/PIs in the DFS order from the roots
-    Gia_ManIncrementTravId( p );
-    vRoots  = Vec_IntAlloc( Vec_IntSize(vPart) );
-    Vec_IntForEachEntry( vPart, iOut, i )
-        Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManCo(p, Gia_ManPoNum(p)+iOut)) );
-    vNodes = Gia_ManCollectNodesCis( p, Vec_IntArray(vRoots), Vec_IntSize(vRoots) );
-    Vec_IntFree( vRoots );
-    // unmark register outputs
-    Vec_IntForEachEntry( vPart, iOut, i )
-        Gia_ObjSetTravIdPrevious( p, Gia_ManCi(p, Gia_ManPiNum(p)+iOut) );
-    // count pure PIs
-    nCountPis = nCountRegs = 0;
-    Gia_ManForEachPi( p, pObj, i )
-        nCountPis += Gia_ObjIsTravIdCurrent(p, pObj);
-    // count outputs of other registers
-    Gia_ManForEachRo( p, pObj, i )
-        nCountRegs += Gia_ObjIsTravIdCurrent(p, pObj); // should be !Gia_... ???
-    if ( pnCountPis )
-        *pnCountPis = nCountPis;
-    if ( pnCountRegs )
-        *pnCountRegs = nCountRegs;
-    // clean old manager
-    Gia_ManFillValue(p);
-    Gia_ManConst0(p)->Value = 0;
-    // create the new manager
-    pNew = Gia_ManStart( Vec_IntSize(vNodes) );
-    // create the PIs
-    Gia_ManForEachCi( p, pObj, i )
-        if ( Gia_ObjIsTravIdCurrent(p, pObj) )
-            pObj->Value = Gia_ManAppendCi(pNew);
-    // add variables for the register outputs
-    // create fake POs to hold the register outputs
-    Vec_IntForEachEntry( vPart, iOut, i )
-    {
-        pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut);
-        pObj->Value = Gia_ManAppendCi(pNew);
-        Gia_ManAppendCo( pNew, pObj->Value );
-        Gia_ObjSetTravIdCurrent( p, pObj ); // added
-    }
-    // create the nodes
-    Gia_ManForEachObjVec( vNodes, p, pObj, i )
-        if ( Gia_ObjIsAnd(pObj) )
-            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    // add real POs for the registers
-    Vec_IntForEachEntry( vPart, iOut, i )
-    {
-        pObj = Gia_ManCo( p, Gia_ManPoNum(p)+iOut );
-        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    }
-    Gia_ManSetRegNum( pNew, Vec_IntSize(vPart) );
-    // create map
-    if ( ppMapBack )
-    {
-        pMapBack = ABC_FALLOC( int, Gia_ManObjNum(pNew) );
-        // map constant nodes
-        pMapBack[0] = 0;
-        // logic cones of register outputs
-        Gia_ManForEachObjVec( vNodes, p, pObj, i )
-        {
-//            pObjNew = Aig_Regular(pObj->pData);
-//            pMapBack[pObjNew->Id] = pObj->Id;
-            assert( Gia_Lit2Var(Gia_ObjValue(pObj)) >= 0 );
-            assert( Gia_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) );
-            pMapBack[ Gia_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj);
-        }
-        // map register outputs
-        Vec_IntForEachEntry( vPart, iOut, i )
-        {
-            pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut);
-//            pObjNew = pObj->pData;
-//            pMapBack[pObjNew->Id] = pObj->Id;
-            assert( Gia_Lit2Var(Gia_ObjValue(pObj)) >= 0 );
-            assert( Gia_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) );
-            pMapBack[ Gia_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj);
-        }
-        *ppMapBack = pMapBack;
-    }
-    Vec_IntFree( vNodes );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_TransferMappedClasses( Gia_Man_t * pPart, int * pMapBack, int * pReprs )
-{
-    Gia_Obj_t * pObj;
-    int i, Id1, Id2, nClasses;
-    if ( pPart->pReprs == NULL ) 
-        return 0;
-    nClasses = 0;
-    Gia_ManForEachObj( pPart, pObj, i )
-    {
-        if ( Gia_ObjRepr(pPart, i) == GIA_VOID )
-            continue;
-        assert( i                     < Gia_ManObjNum(pPart) );
-        assert( Gia_ObjRepr(pPart, i) < Gia_ManObjNum(pPart) );
-        Id1 = pMapBack[ i ];
-        Id2 = pMapBack[ Gia_ObjRepr(pPart, i) ];
-        if ( Id1 == Id2 )
-            continue;
-        if ( Id1 < Id2 )
-            pReprs[Id2] = Id1;
-        else
-            pReprs[Id1] = Id2;
-        nClasses++;
-    }
-    return nClasses;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManFindRepr_rec( int * pReprs, int Id )
-{
-    if ( pReprs[Id] == 0 )
-        return 0;
-    if ( pReprs[Id] == ~0 )
-        return Id;
-    return Gia_ManFindRepr_rec( pReprs, pReprs[Id] );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Normalizes equivalences.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManNormalizeEquivalences( Gia_Man_t * p, int * pReprs )
-{
-    int i, iRepr;
-    assert( p->pReprs == NULL );
-    assert( p->pNexts == NULL );
-    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
-    for ( i = 0; i < Gia_ManObjNum(p); i++ )
-        Gia_ObjSetRepr( p, i, GIA_VOID );
-    for ( i = 0; i < Gia_ManObjNum(p); i++ )
-    {
-        if ( pReprs[i] == ~0 )
-            continue;
-        iRepr = Gia_ManFindRepr_rec( pReprs, i );
-        Gia_ObjSetRepr( p, i, iRepr );
-    }
-    p->pNexts = Gia_ManDeriveNexts( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Partitioned sequential synthesis.]
-
-  Description [Returns AIG annotated with equivalence classes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
-{
-    int fPrintParts = 0;
-    char Buffer[100];
-    Gia_Man_t * pTemp;
-    Vec_Ptr_t * vParts = (Vec_Ptr_t *)p->vClockDoms;
-    Vec_Int_t * vPart;
-    int * pMapBack, * pReprs;
-    int i, nCountPis, nCountRegs;
-    int nClasses, clk = clock();
-
-    // save parameters
-    if ( fPrintParts )
-    {
-        // print partitions
-        Abc_Print( 1, "The following clock domains are used:\n" );
-        Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
-        {
-            pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
-            sprintf( Buffer, "part%03d.aig", i );
-            Gia_WriteAiger( pTemp, Buffer, 0, 0 );
-            Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
-                i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) );
-            Gia_ManStop( pTemp );
-        }
-    }
-
-    // perform sequential synthesis for clock domains
-    pReprs = ABC_FALLOC( int, Gia_ManObjNum(p) );
-    Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
-    {
-        pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, &pMapBack );
-        if ( nCountPis > 0 ) 
-        {
-            if ( pPars->fUseScorr )
-            {
-                Cec_ParCor_t CorPars, * pCorPars = &CorPars;
-                Cec_ManCorSetDefaultParams( pCorPars );
-                pCorPars->nBTLimit   = pPars->nBTLimit;
-                pCorPars->nLevelMax  = pPars->nLevelMax;
-                pCorPars->fVerbose   = pPars->fVeryVerbose;
-                pCorPars->fUseCSat   = 1;
-                Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
-            }
-            else if ( pPars->fUseLcorr )
-            {
-                Cec_ParCor_t CorPars, * pCorPars = &CorPars;
-                Cec_ManCorSetDefaultParams( pCorPars );
-                pCorPars->fLatchCorr = 1;
-                pCorPars->nBTLimit   = pPars->nBTLimit;
-                pCorPars->fVerbose   = pPars->fVeryVerbose;
-                pCorPars->fUseCSat   = 1;
-                Cec_ManLSCorrespondenceClasses( pTemp, pCorPars );
-            }
-            else
-            {
-//                pNew = Gia_ManSeqStructSweep( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
-//                Gia_ManStop( pNew );
-                Gia_ManSeqCleanupClasses( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose );
-            }
-//Abc_Print( 1, "Part equivalences = %d.\n", Gia_ManEquivCountLitsAll(pTemp) );
-            nClasses = Gia_TransferMappedClasses( pTemp, pMapBack, pReprs );
-            if ( pPars->fVerbose )
-            {
-                Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. Cl = %5d.\n", 
-                    i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp), nClasses );
-            }
-        }
-        Gia_ManStop( pTemp );
-        ABC_FREE( pMapBack );
-    }
-
-    // generate resulting equivalences
-    Gia_ManNormalizeEquivalences( p, pReprs );
-//Abc_Print( 1, "Total equivalences = %d.\n", Gia_ManEquivCountLitsAll(p) );
-    ABC_FREE( pReprs );
-    if ( pPars->fVerbose )
-    {
-        Abc_PrintTime( 1, "Total time", clock() - clk );
-    }
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-