sswIslands.c 18.8 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    [sswIslands.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [Detection of islands of difference.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

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

#include "sswInt.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 48 49 50 51 52 53 54
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

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

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

  Synopsis    [Creates pair of structurally equivalent nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
    pObj0->pData = pObj1;
    pObj1->pData = pObj0;
    Vec_IntPush( vPairs, pObj0->Id );
    Vec_IntPush( vPairs, pObj1->Id );
}

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

Alan Mishchenko committed
55
  Synopsis    [Establishes relationship between nodes using pairing.]
Alan Mishchenko committed
56 57 58 59 60 61 62 63

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
64
void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
Alan Mishchenko committed
65
{
Alan Mishchenko committed
66
    Aig_Obj_t * pObj0, * pObj1;
Alan Mishchenko committed
67
    int i;
Alan Mishchenko committed
68
    // create matching
Alan Mishchenko committed
69 70
    Aig_ManCleanData( p0 );
    Aig_ManCleanData( p1 );
Alan Mishchenko committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
    {
        pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
        pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
        assert( pObj0->pData == NULL );
        assert( pObj1->pData == NULL );
        pObj0->pData = pObj1;
        pObj1->pData = pObj0;
    }
    // make sure constants are matched
    pObj0 = Aig_ManConst1( p0 );
    pObj1 = Aig_ManConst1( p1 );
    assert( pObj0->pData == pObj1 );
    assert( pObj1->pData == pObj0 );
    // make sure PIs are matched
Alan Mishchenko committed
86
    Saig_ManForEachPi( p0, pObj0, i )
Alan Mishchenko committed
87
    {
88
        pObj1 = Aig_ManCi( p1, i );
Alan Mishchenko committed
89 90 91 92
        assert( pObj0->pData == pObj1 );
        assert( pObj1->pData == pObj0 );
    }
    // make sure the POs are not matched
93
    Aig_ManForEachCo( p0, pObj0, i )
Alan Mishchenko committed
94
    {
95
        pObj1 = Aig_ManCo( p1, i );
Alan Mishchenko committed
96 97 98 99 100
        assert( pObj0->pData == NULL );
        assert( pObj1->pData == NULL );
    }

    // check that LIs/LOs are matched in sync
Alan Mishchenko committed
101 102
    Saig_ManForEachLo( p0, pObj0, i )
    {
Alan Mishchenko committed
103 104
        if ( pObj0->pData == NULL )
            continue;
105
        pObj1 = (Aig_Obj_t *)pObj0->pData;
Alan Mishchenko committed
106
        if ( !Saig_ObjIsLo(p1, pObj1) )
107
            Abc_Print( 1, "Mismatch between LO pairs.\n" );
Alan Mishchenko committed
108
    }
Alan Mishchenko committed
109 110 111 112
    Saig_ManForEachLo( p1, pObj1, i )
    {
        if ( pObj1->pData == NULL )
            continue;
113
        pObj0 = (Aig_Obj_t *)pObj1->pData;
Alan Mishchenko committed
114
        if ( !Saig_ObjIsLo(p0, pObj0) )
115
            Abc_Print( 1, "Mismatch between LO pairs.\n" );
Alan Mishchenko committed
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
    }
}

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

  Synopsis    [Establishes relationship between nodes using pairing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
{
    Aig_Obj_t * pNext, * pObj;
133
    int i, k, iFan = -1;
Alan Mishchenko committed
134 135 136
    Vec_PtrClear( vNodes );
    Aig_ManIncrementTravId( p );
    Aig_ManForEachObj( p, pObj, i )
Alan Mishchenko committed
137
    {
138
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
139
            continue;
Alan Mishchenko committed
140
        if ( pObj->pData != NULL )
Alan Mishchenko committed
141
            continue;
Alan Mishchenko committed
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
        if ( Saig_ObjIsLo(p, pObj) )
        {
            pNext = Saig_ObjLoToLi(p, pObj);
            pNext = Aig_ObjFanin0(pNext);
            if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) && !Aig_ObjIsConst1(pNext) )
            {
                Aig_ObjSetTravIdCurrent(p, pNext);
                Vec_PtrPush( vNodes, pNext );
            }
        }
        if ( Aig_ObjIsNode(pObj) )
        {
            pNext = Aig_ObjFanin0(pObj);
            if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
            {
                Aig_ObjSetTravIdCurrent(p, pNext);
                Vec_PtrPush( vNodes, pNext );
            }
            pNext = Aig_ObjFanin1(pObj);
            if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
            {
                Aig_ObjSetTravIdCurrent(p, pNext);
                Vec_PtrPush( vNodes, pNext );
            }
        }
167
        Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
Alan Mishchenko committed
168 169 170 171 172 173 174 175 176 177 178
        {
            if ( Saig_ObjIsPo(p, pNext) )
                continue;
            if ( Saig_ObjIsLi(p, pNext) )
                pNext = Saig_ObjLiToLo(p, pNext);
            if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
            {
                Aig_ObjSetTravIdCurrent(p, pNext);
                Vec_PtrPush( vNodes, pNext );
            }
        }
Alan Mishchenko committed
179 180 181 182 183
    }
}

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

Alan Mishchenko committed
184
  Synopsis    [Establishes relationship between nodes using pairing.]
Alan Mishchenko committed
185 186

  Description []
187

Alan Mishchenko committed
188 189 190 191 192
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
193
int Ssw_MatchingCountUnmached( Aig_Man_t * p )
Alan Mishchenko committed
194
{
Alan Mishchenko committed
195 196 197
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Aig_ManForEachObj( p, pObj, i )
Alan Mishchenko committed
198
    {
199
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
Alan Mishchenko committed
200 201
            continue;
        if ( pObj->pData != NULL )
Alan Mishchenko committed
202
            continue;
Alan Mishchenko committed
203
        Counter++;
Alan Mishchenko committed
204
    }
Alan Mishchenko committed
205
    return Counter;
Alan Mishchenko committed
206 207 208 209
}

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

Alan Mishchenko committed
210
  Synopsis    [Establishes relationship between nodes using pairing.]
Alan Mishchenko committed
211 212 213 214 215 216 217 218

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
219
void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose )
Alan Mishchenko committed
220
{
Alan Mishchenko committed
221 222 223 224 225 226 227 228
    Vec_Ptr_t * vNodes0, * vNodes1;
    Aig_Obj_t * pNext0, * pNext1;
    int d, k;
    Aig_ManFanoutStart(p0);
    Aig_ManFanoutStart(p1);
    vNodes0 = Vec_PtrAlloc( 1000 );
    vNodes1 = Vec_PtrAlloc( 1000 );
    if ( fVerbose )
Alan Mishchenko committed
229
    {
Alan Mishchenko committed
230
        int nUnmached = Ssw_MatchingCountUnmached(p0);
231 232 233
        Abc_Print( 1, "Extending islands by %d steps:\n", nDist );
        Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
            0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
234
            nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
Alan Mishchenko committed
235
    }
Alan Mishchenko committed
236
    for ( d = 0; d < nDist; d++ )
Alan Mishchenko committed
237
    {
Alan Mishchenko committed
238 239
        Ssw_MatchingExtendOne( p0, vNodes0 );
        Ssw_MatchingExtendOne( p1, vNodes1 );
240
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pNext0, k )
Alan Mishchenko committed
241
        {
242
            pNext1 = (Aig_Obj_t *)pNext0->pData;
Alan Mishchenko committed
243 244 245 246 247 248 249 250
            if ( pNext1 == NULL )
                continue;
            assert( pNext1->pData == pNext0 );
            if ( Saig_ObjIsPi(p0, pNext1) )
                continue;
            pNext0->pData = NULL;
            pNext1->pData = NULL;
        }
251
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pNext0, k )
Alan Mishchenko committed
252
        {
253
            pNext1 = (Aig_Obj_t *)pNext0->pData;
Alan Mishchenko committed
254 255 256 257 258 259 260 261 262 263 264
            if ( pNext1 == NULL )
                continue;
            assert( pNext1->pData == pNext0 );
            if ( Saig_ObjIsPi(p1, pNext1) )
                continue;
            pNext0->pData = NULL;
            pNext1->pData = NULL;
        }
        if ( fVerbose )
        {
            int nUnmached = Ssw_MatchingCountUnmached(p0);
265 266
            Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
                d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
267
                nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
Alan Mishchenko committed
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296
        }
    }
    Vec_PtrFree( vNodes0 );
    Vec_PtrFree( vNodes1 );
    Aig_ManFanoutStop(p0);
    Aig_ManFanoutStop(p1);
}

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

  Synopsis    [Used differences in p0 to complete p1.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
{
    Vec_Ptr_t * vNewLis;
    Aig_Obj_t * pObj0, * pObj0Li, * pObj1;
    int i;
    // create register outputs in p0 that are absent in p1
    vNewLis = Vec_PtrAlloc( 100 );
    Saig_ManForEachLiLo( p0, pObj0Li, pObj0, i )
    {
        if ( pObj0->pData != NULL )
Alan Mishchenko committed
297
            continue;
298
        pObj1 = Aig_ObjCreateCi( p1 );
Alan Mishchenko committed
299 300 301
        pObj0->pData = pObj1;
        pObj1->pData = pObj0;
        Vec_PtrPush( vNewLis, pObj0Li );
Alan Mishchenko committed
302
    }
Alan Mishchenko committed
303 304
    // add missing nodes in the topological order
    Aig_ManForEachNode( p0, pObj0, i )
Alan Mishchenko committed
305
    {
Alan Mishchenko committed
306 307 308 309 310
        if ( pObj0->pData != NULL )
            continue;
        pObj1 = Aig_And( p1, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
        pObj0->pData = pObj1;
        pObj1->pData = pObj0;
Alan Mishchenko committed
311
    }
Alan Mishchenko committed
312
    // create register outputs in p0 that are absent in p1
313
    Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i )
314
        Aig_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) );
Alan Mishchenko committed
315 316 317
    // increment the number of registers
    Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
    Vec_PtrFree( vNewLis );
Alan Mishchenko committed
318 319
}

Alan Mishchenko committed
320

Alan Mishchenko committed
321 322
/**Function*************************************************************

Alan Mishchenko committed
323
  Synopsis    [Derives matching for all pairs.]
Alan Mishchenko committed
324

Alan Mishchenko committed
325
  Description [Modifies both AIGs.]
326

Alan Mishchenko committed
327 328 329 330 331
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
332
Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
Alan Mishchenko committed
333 334 335 336
{
    Vec_Int_t * vPairsNew;
    Aig_Obj_t * pObj0, * pObj1;
    int i;
Alan Mishchenko committed
337
    // check correctness
338 339
    assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
    assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
Alan Mishchenko committed
340 341 342 343 344
    assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) );
    assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) );
    // create complete pairs
    vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
    Aig_ManForEachObj( p0, pObj0, i )
Alan Mishchenko committed
345
    {
346
        if ( Aig_ObjIsCo(pObj0) )
Alan Mishchenko committed
347
            continue;
348
        pObj1 = (Aig_Obj_t *)pObj0->pData;
Alan Mishchenko committed
349 350 351 352 353 354 355 356 357 358 359 360 361 362 363
        Vec_IntPush( vPairsNew, pObj0->Id );
        Vec_IntPush( vPairsNew, pObj1->Id );
    }
    return vPairsNew;
}





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

  Synopsis    [Transfers the result of matching to miter.]

  Description [The array of pairs should be complete.]
364

Alan Mishchenko committed
365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairsAll )
{
    Vec_Int_t * vPairsMiter;
    Aig_Obj_t * pObj0, * pObj1;
    int i;
    // create matching of nodes in the miter
    vPairsMiter = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
    for ( i = 0; i < Vec_IntSize(vPairsAll); i += 2 )
    {
        pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairsAll, i) );
        pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairsAll, i+1) );
        assert( pObj0->pData != NULL );
        assert( pObj1->pData != NULL );
        if ( pObj0->pData == pObj1->pData )
            continue;
385
        if ( Aig_ObjIsNone((Aig_Obj_t *)pObj0->pData) || Aig_ObjIsNone((Aig_Obj_t *)pObj1->pData) )
Alan Mishchenko committed
386 387
            continue;
        // get the miter nodes
388 389
        pObj0 = (Aig_Obj_t *)pObj0->pData;
        pObj1 = (Aig_Obj_t *)pObj1->pData;
Alan Mishchenko committed
390 391
        assert( !Aig_IsComplement(pObj0) );
        assert( !Aig_IsComplement(pObj1) );
Alan Mishchenko committed
392
        assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
393
        if ( Aig_ObjIsCo(pObj0) )
Alan Mishchenko committed
394
            continue;
Alan Mishchenko committed
395 396
        assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) );
        assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) );
Alan Mishchenko committed
397
        assert( pObj0->Id < pObj1->Id );
Alan Mishchenko committed
398 399
        Vec_IntPush( vPairsMiter, pObj0->Id );
        Vec_IntPush( vPairsMiter, pObj1->Id );
Alan Mishchenko committed
400
    }
Alan Mishchenko committed
401
    return vPairsMiter;
Alan Mishchenko committed
402 403
}

Alan Mishchenko committed
404 405 406 407




Alan Mishchenko committed
408 409 410 411 412
/**Function*************************************************************

  Synopsis    [Solves SEC using structural similarity.]

  Description [Modifies both p0 and p1 by adding extra logic.]
413

Alan Mishchenko committed
414 415 416 417 418
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
419
Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
Alan Mishchenko committed
420
{
421
    Ssw_Man_t * p;
Alan Mishchenko committed
422
    Vec_Int_t * vPairsAll, * vPairsMiter;
Alan Mishchenko committed
423
    Aig_Man_t * pMiter, * pAigNew;
Alan Mishchenko committed
424 425 426 427 428 429 430 431 432 433 434
    // derive full matching
    Ssw_MatchingStart( p0, p1, vPairs );
    if ( pPars->nIsleDist )
        Ssw_MatchingExtend( p0, p1, pPars->nIsleDist, pPars->fVerbose );
    Ssw_MatchingComplete( p0, p1 );
    Ssw_MatchingComplete( p1, p0 );
    vPairsAll = Ssw_MatchingPairs( p0, p1 );
    // create miter and transfer matching
    pMiter = Saig_ManCreateMiter( p0, p1, 0 );
    vPairsMiter = Ssw_MatchingMiter( pMiter, p0, p1, vPairsAll );
    Vec_IntFree( vPairsAll );
Alan Mishchenko committed
435 436 437
    // start the induction manager
    p = Ssw_ManCreate( pMiter, pPars );
    // create equivalence classes using these IDs
Alan Mishchenko committed
438 439 440
    if ( p->pPars->fPartSigCorr )
        p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
    else
441
        p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
Alan Mishchenko committed
442 443 444 445 446 447 448
    if ( p->pPars->fDumpSRInit )
    {
        if ( p->pPars->fPartSigCorr )
        {
            Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
            Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL );
            Aig_ManStop( pSRed );
449
            Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
Alan Mishchenko committed
450 451
        }
        else
452
            Abc_Print( 1, "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
Alan Mishchenko committed
453
    }
Alan Mishchenko committed
454
    p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
455
    Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
Alan Mishchenko committed
456 457 458 459 460 461 462 463 464 465 466
    // perform refinement of classes
    pAigNew = Ssw_SignalCorrespondenceRefine( p );
    // cleanup
    Ssw_ManStop( p );
    Aig_ManStop( pMiter );
    Vec_IntFree( vPairsMiter );
    return pAigNew;
}

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

Alan Mishchenko committed
467
  Synopsis    [Solves SEC with structural similarity.]
Alan Mishchenko committed
468

Alan Mishchenko committed
469 470 471
  Description [The first two arguments are pointers to the AIG managers.
  The third argument is the array of pairs of IDs of structurally equivalent
  nodes from the first and second managers, respectively.]
Alan Mishchenko committed
472
               
Alan Mishchenko committed
473
  SideEffects [The managers will be updated by adding "islands of difference".]
Alan Mishchenko committed
474 475 476 477

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
478
int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
Alan Mishchenko committed
479
{
Alan Mishchenko committed
480
    Ssw_Pars_t Pars;
Alan Mishchenko committed
481
    Aig_Man_t * pAigRes;
482
    int RetValue;
483
    abctime clk = Abc_Clock();
Alan Mishchenko committed
484 485 486 487 488 489
    // derive parameters if not given
    if ( pPars == NULL )
        Ssw_ManSetDefaultParams( pPars = &Pars );
    // reduce the AIG with pairs
    pAigRes = Ssw_SecWithSimilaritySweep( p0, p1, vPairs, pPars );
    // report the result of verification
Alan Mishchenko committed
490 491
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
492
        Abc_Print( 1, "Verification successful.  " );
Alan Mishchenko committed
493
    else if ( RetValue == 0 )
494
        Abc_Print( 1, "Verification failed with a counter-example.  " );
Alan Mishchenko committed
495
    else
496
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
Alan Mishchenko committed
497
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
498
    ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
499 500 501 502
    Aig_ManStop( pAigRes );
    return RetValue;
}

Alan Mishchenko committed
503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522
/**Function*************************************************************

  Synopsis    [Dummy procedure to detect structural similarity.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_StrSimPerformMatching_hack( Aig_Man_t * p0, Aig_Man_t * p1 )
{
    Vec_Int_t * vPairs;
    Aig_Obj_t * pObj;
    int i;
    // create array of pairs
    vPairs = Vec_IntAlloc( 100 );
    Aig_ManForEachObj( p0, pObj, i )
    {
523
        if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
Alan Mishchenko committed
524 525 526 527 528 529
            continue;
        Vec_IntPush( vPairs, i );
        Vec_IntPush( vPairs, i );
    }
    return vPairs;
}
Alan Mishchenko committed
530 531 532

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

Alan Mishchenko committed
533
  Synopsis    [Solves SEC with structural similarity.]
Alan Mishchenko committed
534 535 536 537 538 539 540 541

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Alan Mishchenko committed
542
int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
Alan Mishchenko committed
543
{
Alan Mishchenko committed
544
    Vec_Int_t * vPairs;
Alan Mishchenko committed
545 546
    Aig_Man_t * pPart0, * pPart1;
    int RetValue;
Alan Mishchenko committed
547
    if ( pPars->fVerbose )
548
        Abc_Print( 1, "Performing sequential verification using structural similarity.\n" );
Alan Mishchenko committed
549 550
    // consider the case when a miter is given
    if ( p1 == NULL )
Alan Mishchenko committed
551
    {
Alan Mishchenko committed
552 553 554 555 556 557 558
        if ( pPars->fVerbose )
        {
            Aig_ManPrintStats( p0 );
        }
        // demiter the miter
        if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
        {
559
            Abc_Print( 1, "Demitering has failed.\n" );
Alan Mishchenko committed
560 561
            return -1;
        }
Alan Mishchenko committed
562
    }
Alan Mishchenko committed
563 564 565 566 567 568
    else
    {
        pPart0 = Aig_ManDupSimple( p0 );
        pPart1 = Aig_ManDupSimple( p1 );
    }
    if ( pPars->fVerbose )
Alan Mishchenko committed
569 570 571
    {
//        Aig_ManPrintStats( pPart0 );
//        Aig_ManPrintStats( pPart1 );
Alan Mishchenko committed
572 573
        if ( p1 == NULL )
        {
Alan Mishchenko committed
574 575
//        Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
//        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
576
//        Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
Alan Mishchenko committed
577
        }
Alan Mishchenko committed
578
    }
Alan Mishchenko committed
579 580 581 582 583 584 585 586
    assert( Aig_ManRegNum(pPart0) > 0 );
    assert( Aig_ManRegNum(pPart1) > 0 );
    assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
    assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
    // derive pairs
//    vPairs = Saig_StrSimPerformMatching_hack( pPart0, pPart1 );
    vPairs = Saig_StrSimPerformMatching( pPart0, pPart1, 0, pPars->fVerbose, NULL );
    RetValue = Ssw_SecWithSimilarityPairs( pPart0, pPart1, vPairs, pPars );
Alan Mishchenko committed
587 588
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
Alan Mishchenko committed
589
    Vec_IntFree( vPairs );
Alan Mishchenko committed
590 591 592 593 594 595 596 597
    return RetValue;
}

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


598
ABC_NAMESPACE_IMPL_END