dchCore.c 5.02 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
/**CFile****************************************************************

  FileName    [dchCore.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Choice computation for tech-mapping.]

  Synopsis    [The core procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 29, 2008.]

  Revision    [$Id: dchCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]

***********************************************************************/

#include "dchInt.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [This procedure sets default parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dch_ManSetDefaultParams( Dch_Pars_t * p )
{
    memset( p, 0, sizeof(Dch_Pars_t) );
Alan Mishchenko committed
48 49 50 51 52 53
    p->nWords         =     8;  // the number of simulation words
    p->nBTLimit       =  1000;  // conflict limit at a node
    p->nSatVarMax     =  5000;  // the max number of SAT variables
    p->fSynthesis     =     1;  // derives three snapshots
    p->fPolarFlip     =     1;  // uses polarity adjustment
    p->fSimulateTfo   =     1;  // simulate TFO
Alan Mishchenko committed
54
    p->fPower         =     0;  // power-aware rewriting
Alan Mishchenko committed
55
    p->fLightSynth    =     0;  // uses lighter version of synthesis
56
    p->fSkipRedSupp   =     0;  // skips choices with redundant structural support
Alan Mishchenko committed
57 58 59
    p->fVerbose       =     0;  // verbose stats
    p->nNodesAhead    =  1000;  // the lookahead in terms of nodes
    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
Alan Mishchenko committed
60 61 62 63
}

/**Function*************************************************************

64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
  Synopsis    [Returns verbose parameter.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Dch_ManReadVerbose( Dch_Pars_t * p )
{
    return p->fVerbose;
}

/**Function*************************************************************

Alan Mishchenko committed
80 81 82 83 84 85 86 87 88
  Synopsis    [Performs computation of AIGs with choices.]

  Description [Takes several AIGs and performs choicing.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
89
Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
Alan Mishchenko committed
90 91 92
{
    Dch_Man_t * p;
    Aig_Man_t * pResult;
93
    clock_t clk, clkTotal = clock();
Alan Mishchenko committed
94 95
    // reset random numbers
    Aig_ManRandom(1);
Alan Mishchenko committed
96
    // start the choicing manager
Alan Mishchenko committed
97
    p = Dch_ManCreate( pAig, pPars );
Alan Mishchenko committed
98
    // compute candidate equivalence classes
Alan Mishchenko committed
99
clk = clock(); 
Alan Mishchenko committed
100
    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
Alan Mishchenko committed
101 102 103 104 105
p->timeSimInit = clock() - clk;
//    Dch_ClassesPrint( p->ppClasses, 0 );
    p->nLits = Dch_ClassesLitNum( p->ppClasses );
    // perform SAT sweeping
    Dch_ManSweep( p );
Alan Mishchenko committed
106
    // free memory ahead of time
Alan Mishchenko committed
107
p->timeTotal = clock() - clkTotal;
Alan Mishchenko committed
108
    Dch_ManStop( p );
Alan Mishchenko committed
109 110
    // create choices
    ABC_FREE( pAig->pTable );
111
    pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
Alan Mishchenko committed
112
    // count the number of representatives
Alan Mishchenko committed
113
    if ( pPars->fVerbose ) 
114
        Abc_Print( 1, "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
Alan Mishchenko committed
115 116 117
               Dch_DeriveChoiceCountReprs( pAig ),
               Dch_DeriveChoiceCountEquivs( pResult ),
               Aig_ManChoiceNum( pResult ) );
Alan Mishchenko committed
118 119 120
    return pResult;
}

Alan Mishchenko committed
121 122 123 124 125 126 127 128 129 130 131 132 133 134
/**Function*************************************************************

  Synopsis    [Performs computation of AIGs with choices.]

  Description [Takes several AIGs and performs choicing.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
    Dch_Man_t * p;
135
    clock_t clk, clkTotal = clock();
Alan Mishchenko committed
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
    // reset random numbers
    Aig_ManRandom(1);
    // start the choicing manager
    p = Dch_ManCreate( pAig, pPars );
    // compute candidate equivalence classes
clk = clock(); 
    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
p->timeSimInit = clock() - clk;
//    Dch_ClassesPrint( p->ppClasses, 0 );
    p->nLits = Dch_ClassesLitNum( p->ppClasses );
    // perform SAT sweeping
    Dch_ManSweep( p );
    // free memory ahead of time
p->timeTotal = clock() - clkTotal;
    Dch_ManStop( p );
}

Alan Mishchenko committed
153 154 155 156 157
////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


158 159
ABC_NAMESPACE_IMPL_END