cecChoice.c 14.5 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6
/**CFile****************************************************************

  FileName    [cecChoice.c]

  SystemName  [ABC: Logic synthesis and verification system.]

Alan Mishchenko committed
7
  PackageName [Combinational equivalence checking.]
Alan Mishchenko committed
8 9 10 11 12 13 14 15 16 17 18 19 20 21

  Synopsis    [Computation of structural choices.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: cecChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

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

#include "cecInt.h"
22 23
#include "aig/gia/giaAig.h"
#include "proof/dch/dch.h"
Alan Mishchenko committed
24

25 26 27
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
28 29 30 31
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

Alan Mishchenko committed
32 33 34 35 36
static void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj );

extern int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore );
extern int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings );

Alan Mishchenko committed
37 38 39 40 41 42
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

Alan Mishchenko committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
  Synopsis    [Computes the real value of the literal w/o spec reduction.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cec_ManCombSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
    assert( Gia_ObjIsAnd(pObj) );
    Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
    Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
    return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}

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

  Synopsis    [Recursively performs speculative reduction for the object.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
    Gia_Obj_t * pRepr;
    if ( ~pObj->Value )
        return;
    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
    {
        Cec_ManCombSpecReduce_rec( pNew, p, pRepr );
79
        pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
Alan Mishchenko committed
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
        return;
    }
    pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj );
}

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

  Synopsis    [Derives SRM for signal correspondence.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fRings )
{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj, * pRepr;
    Vec_Int_t * vXorLits;
    int i, iPrev, iObj, iPrevNew, iObjNew;
    assert( p->pReprs != NULL );
    Gia_ManSetPhase( p );
    Gia_ManFillValue( p );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
106
    pNew->pName = Abc_UtilStrsav( p->pName );
107
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Alan Mishchenko committed
108 109 110 111 112 113 114 115 116 117 118 119 120
    Gia_ManHashAlloc( pNew );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachCi( p, pObj, i )
        pObj->Value = Gia_ManAppendCi(pNew);
    *pvOutputs = Vec_IntAlloc( 1000 );
    vXorLits = Vec_IntAlloc( 1000 );
    if ( fRings )
    {
        Gia_ManForEachObj1( p, pObj, i )
        {
            if ( Gia_ObjIsConst( p, i ) )
            {
                iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
121
                iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
Alan Mishchenko committed
122 123 124 125 126 127 128 129 130 131 132 133 134 135
                if ( iObjNew != 0 )
                {
                    Vec_IntPush( *pvOutputs, 0 );
                    Vec_IntPush( *pvOutputs, i );
                    Vec_IntPush( vXorLits, iObjNew );
                }
            }
            else if ( Gia_ObjIsHead( p, i ) )
            {
                iPrev = i;
                Gia_ClassForEachObj1( p, i, iObj )
                {
                    iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
                    iObjNew  = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
136 137
                    iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
                    iObjNew  = Abc_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
Alan Mishchenko committed
138 139 140 141
                    if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
                    {
                        Vec_IntPush( *pvOutputs, iPrev );
                        Vec_IntPush( *pvOutputs, iObj );
142
                        Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
Alan Mishchenko committed
143 144 145 146 147 148
                    }
                    iPrev = iObj;
                }
                iObj = i;
                iPrevNew = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
                iObjNew  = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
149 150
                iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
                iObjNew  = Abc_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
Alan Mishchenko committed
151 152 153 154
                if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
                {
                    Vec_IntPush( *pvOutputs, iPrev );
                    Vec_IntPush( *pvOutputs, iObj );
155
                    Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
Alan Mishchenko committed
156 157 158 159 160 161 162 163 164 165 166 167 168
                }
            }
        }
    }
    else
    {
        Gia_ManForEachObj1( p, pObj, i )
        {
            pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
            if ( pRepr == NULL )
                continue;
            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Cec_ManCombSpecReal( pNew, p, pRepr );
            iObjNew  = Cec_ManCombSpecReal( pNew, p, pObj );
169
            iObjNew  = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
Alan Mishchenko committed
170 171 172 173 174 175 176 177 178 179 180 181
            if ( iPrevNew != iObjNew )
            {
                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
                Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
            }
        }
    }
    Vec_IntForEachEntry( vXorLits, iObjNew, i )
        Gia_ManAppendCo( pNew, iObjNew );
    Vec_IntFree( vXorLits );
    Gia_ManHashStop( pNew );
182
//Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
Alan Mishchenko committed
183
    pNew = Gia_ManCleanup( pTemp = pNew );
184
//Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
Alan Mishchenko committed
185 186 187 188 189 190 191
    Gia_ManStop( pTemp );
    return pNew;
}


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

Alan Mishchenko committed
192 193 194 195 196 197 198 199 200
  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
201 202 203 204 205 206 207 208 209 210 211
int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
{
    int nItersMax = 1000;
    Vec_Str_t * vStatus;
    Vec_Int_t * vOutputs;
    Vec_Int_t * vCexStore;
    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
    Cec_ManSim_t * pSim;
    Gia_Man_t * pSrm;
    int r, RetValue;
212 213
    abctime clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = Abc_Clock();
    abctime clk2, clk = Abc_Clock();
Alan Mishchenko committed
214 215 216 217 218 219
    ABC_FREE( pAig->pReprs );
    ABC_FREE( pAig->pNexts );
    Gia_ManRandom( 1 );
    // prepare simulation manager
    Cec_ManSimSetDefaultParams( pParsSim );
    pParsSim->nWords     = pPars->nWords;
Alan Mishchenko committed
220
    pParsSim->nFrames    = pPars->nRounds;
Alan Mishchenko committed
221 222 223 224 225
    pParsSim->fVerbose   = pPars->fVerbose;
    pParsSim->fLatchCorr   = 0;
    pParsSim->fSeqSimulate = 0;
    // create equivalence classes of registers
    pSim = Cec_ManSimStart( pAig, pParsSim );
226
    Cec_ManSimClassesPrepare( pSim, -1 );
Alan Mishchenko committed
227 228 229 230 231 232 233
    Cec_ManSimClassesRefine( pSim );
    // prepare SAT solving
    Cec_ManSatSetDefaultParams( pParsSat );
    pParsSat->nBTLimit = pPars->nBTLimit;
    pParsSat->fVerbose = pPars->fVerbose;
    if ( pPars->fVerbose )
    {
234
        Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Ring = %d. CSat = %d.\n",
Alan Mishchenko committed
235
            Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
236
        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
Alan Mishchenko committed
237 238 239 240
    }
    // perform refinement of equivalence classes
    for ( r = 0; r < nItersMax; r++ )
    { 
241
        clk = Abc_Clock();
Alan Mishchenko committed
242
        // perform speculative reduction
243
        clk2 = Abc_Clock();
Alan Mishchenko committed
244 245
        pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );
        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );
246
        clkSrm += Abc_Clock() - clk2;
Alan Mishchenko committed
247 248 249
        if ( Gia_ManCoNum(pSrm) == 0 )
        {
            if ( pPars->fVerbose )
250
                Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );
Alan Mishchenko committed
251 252 253 254 255 256
            Vec_IntFree( vOutputs );
            Gia_ManStop( pSrm );            
            break;
        }
//Gia_DumpAiger( pSrm, "choicesrm", r, 2 );
        // found counter-examples to speculation
257
        clk2 = Abc_Clock();
Alan Mishchenko committed
258 259 260 261 262
        if ( pPars->fUseCSat )
            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
        else
            vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
        Gia_ManStop( pSrm );
263
        clkSat += Abc_Clock() - clk2;
Alan Mishchenko committed
264 265 266
        if ( Vec_IntSize(vCexStore) == 0 )
        {
            if ( pPars->fVerbose )
267
                Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
Alan Mishchenko committed
268 269 270 271 272 273
            Vec_IntFree( vCexStore );
            Vec_StrFree( vStatus );
            Vec_IntFree( vOutputs );
            break;
        }
        // refine classes with these counter-examples
274
        clk2 = Abc_Clock();
Alan Mishchenko committed
275 276
        RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );
        Vec_IntFree( vCexStore );
277
        clkSim += Abc_Clock() - clk2;
Alan Mishchenko committed
278 279
        Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
        if ( pPars->fVerbose )
280
            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
Alan Mishchenko committed
281 282 283 284 285 286
        Vec_StrFree( vStatus );
        Vec_IntFree( vOutputs );
//Gia_ManEquivPrintClasses( pAig, 1, 0 );
    }
    // check the overflow
    if ( r == nItersMax )
287
        Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
Alan Mishchenko committed
288
    Cec_ManSimStop( pSim );
289
    clkTotal = Abc_Clock() - clkTotal;
Alan Mishchenko committed
290 291 292
    // report the results
    if ( pPars->fVerbose )
    {
293 294 295 296 297
        Abc_PrintTimeP( 1, "Srm  ", clkSrm,                        clkTotal );
        Abc_PrintTimeP( 1, "Sat  ", clkSat,                        clkTotal );
        Abc_PrintTimeP( 1, "Sim  ", clkSim,                        clkTotal );
        Abc_PrintTimeP( 1, "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
        Abc_PrintTime( 1, "TOTAL",  clkTotal );
Alan Mishchenko committed
298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
    }
    return 0;
}

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

  Synopsis    [Computes choices for the vector of AIGs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
313
Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars )
Alan Mishchenko committed
314
{
Alan Mishchenko committed
315
    Gia_Man_t * pNew;
Alan Mishchenko committed
316 317
    int RetValue;
    // compute equivalences of the miter
Alan Mishchenko committed
318
//    pMiter = Gia_ManChoiceMiter( vGias );
319
//    Gia_ManSetRegNum( pMiter, 0 );
Alan Mishchenko committed
320
    RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
Alan Mishchenko committed
321
    // derive AIG with choices
Alan Mishchenko committed
322
    pNew = Gia_ManEquivToChoices( pGia, nGias );
323
//    Gia_ManHasChoices_very_old( pNew );
Alan Mishchenko committed
324
//    Gia_ManStop( pMiter );
Alan Mishchenko committed
325 326 327
    // report the results
    if ( pPars->fVerbose )
    {
328
//        Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
Alan Mishchenko committed
329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349
//            Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), 
//            100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), 
//            Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 
//            100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
    }
    return pNew;
}

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

  Synopsis    [Computes choices for one AIGs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc )
{
350
//    extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
Alan Mishchenko committed
351 352 353 354 355
    Dch_Pars_t Pars, * pPars = &Pars;
    Aig_Man_t * pMan, * pManNew;
    Gia_Man_t * pGia;
    if ( 0 ) 
    {
Alan Mishchenko committed
356
        pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc );
Alan Mishchenko committed
357 358 359 360 361 362 363 364 365 366 367 368
    }
    else
    {
        pMan = Gia_ManToAig( pAig, 0 );
        Dch_ManSetDefaultParams( pPars );
        pPars->fUseGia  = 1;
        pPars->nBTLimit = pParsChc->nBTLimit;
        pPars->fUseCSat = pParsChc->fUseCSat;
        pPars->fVerbose = pParsChc->fVerbose;
        pManNew = Dar_ManChoiceNew( pMan, pPars );
        pGia = Gia_ManFromAig( pManNew );
        Aig_ManStop( pManNew );
Alan Mishchenko committed
369
//        Aig_ManStop( pMan );
Alan Mishchenko committed
370 371 372 373 374 375 376 377 378 379 380 381 382 383 384
    }
    return pGia;
}

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

  Synopsis    [Performs computation of AIGs with choices.]

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

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
385
Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
Alan Mishchenko committed
386
{
Alan Mishchenko committed
387 388 389
    Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
    Aig_Man_t * pAig;
    if ( pPars->fVerbose )
390
        Abc_PrintTime( 1, "Synthesis time", pPars->timeSynth );
Alan Mishchenko committed
391 392 393 394 395 396
    Cec_ManChcSetDefaultParams( pParsChc );
    pParsChc->nBTLimit = pPars->nBTLimit;
    pParsChc->fUseCSat = pPars->fUseCSat;
    if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
        pParsChc->nBTLimit = 100;
    pParsChc->fVerbose = pPars->fVerbose;
Alan Mishchenko committed
397 398
    pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc );
    Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
Alan Mishchenko committed
399 400 401
    pAig = Gia_ManToAig( pGia, 1 );
    Gia_ManStop( pGia );
    return pAig;
Alan Mishchenko committed
402 403 404 405 406 407 408
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


409 410
ABC_NAMESPACE_IMPL_END