aboutsummaryrefslogtreecommitdiffstats
path: root/os/kernel/include/chsem.h
blob: 17c6a03e315017f2f37ef53dc36e1e3cf2bb7791 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
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
106
107
108
109
110
111
/*
    ChibiOS/RT - Copyright (C) 2006,2007,2008,2009,2010 Giovanni Di Sirio.

    This file is part of ChibiOS/RT.

    ChibiOS/RT is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 3 of the License, or
    (at your option) any later version.

    ChibiOS/RT is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
*/

/**
 * @file    chsem.h
 * @brief   Semaphores macros and structures.
 *
 * @addtogroup semaphores
 * @{
 */

#ifndef _CHSEM_H_
#define _CHSEM_H_

#if CH_USE_SEMAPHORES || defined(__DOXYGEN__)

/**
 * @brief   Semaphore structure.
 */
typedef struct Semaphore {
  ThreadsQueue          s_queue;    /**< @brief Queue of the threads sleeping
                                                on this semaphore.          */
  cnt_t                 s_cnt;      /**< @brief The semaphore counter.      */
} Semaphore;

#ifdef __cplusplus
extern "C" {
#endif
  void chSemInit(Semaphore *sp, cnt_t n);
  void chSemReset(Semaphore *sp, cnt_t n);
  void chSemResetI(Semaphore *sp, cnt_t n);
  msg_t chSemWait(Semaphore *sp);
  msg_t chSemWaitS(Semaphore *sp);
  msg_t chSemWaitTimeout(Semaphore *sp, systime_t time);
  msg_t chSemWaitTimeoutS(Semaphore *sp, systime_t time);
  void chSemSignal(Semaphore *sp);
  void chSemSignalI(Semaphore *sp);
#if CH_USE_SEMSW
  msg_t chSemSignalWait(Semaphore *sps, Semaphore *spw);
#endif
#ifdef __cplusplus
}
#endif

/**
 * @brief   Data part of a static semaphore initializer.
 * @details This macro should be used when statically initializing a semaphore
 *          that is part of a bigger structure.
 *
 * @param[in] name      the name of the semaphore variable
 * @param[in] n         the counter initial value, this value must be
 *                      non-negative
 */
#define _SEMAPHORE_DATA(name, n) {_THREADSQUEUE_DATA(name.s_queue), n}

/**
 * @brief   Static semaphore initializer.
 * @details Statically initialized semaphores require no explicit
 *          initialization using @p chSemInit().
 *
 * @param[in] name      the name of the semaphore variable
 * @param[in] n         the counter initial value, this value must be
 *                      non-negative
 */
#define SEMAPHORE_DECL(name, n) Semaphore name = _SEMAPHORE_DATA(name, n)

/**
 * @brief   Decreases the semaphore counter.
 * @details This macro can be used when the counter is known to be positive.
 *
 * @iclass
 */
#define chSemFastWaitI(sp)      ((sp)->s_cnt--)

/**
 * @brief   Increases the semaphore counter.
 * @details This macro can be used when the counter is known to be not
 *          negative.
 *
 * @iclass
 */
#define chSemFastSignalI(sp)    ((sp)->s_cnt++)

/**
 * @brief   Returns the semaphore counter current value.
 *
 * @iclass
 */
#define chSemGetCounterI(sp)    ((sp)->s_cnt)

#endif /* CH_USE_SEMAPHORES */

#endif /* _CHSEM_H_ */

/** @} */
#n498'>498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598
/**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"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        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*************************************************************

  Synopsis    [Establishes relationship between nodes using pairing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
{
    Aig_Obj_t * pObj0, * pObj1;
    int i;
    // create matching
    Aig_ManCleanData( p0 );
    Aig_ManCleanData( p1 );
    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
    Saig_ManForEachPi( p0, pObj0, i )
    {
        pObj1 = Aig_ManPi( p1, i );
        assert( pObj0->pData == pObj1 );
        assert( pObj1->pData == pObj0 );
    }
    // make sure the POs are not matched
    Aig_ManForEachPo( p0, pObj0, i )
    {
        pObj1 = Aig_ManPo( p1, i );
        assert( pObj0->pData == NULL );
        assert( pObj1->pData == NULL );
    }

    // check that LIs/LOs are matched in sync
    Saig_ManForEachLo( p0, pObj0, i )
    {
        if ( pObj0->pData == NULL )
            continue;
        pObj1 = (Aig_Obj_t *)pObj0->pData;
        if ( !Saig_ObjIsLo(p1, pObj1) )
            printf( "Mismatch between LO pairs.\n" );
    }
    Saig_ManForEachLo( p1, pObj1, i )
    {
        if ( pObj1->pData == NULL )
            continue;
        pObj0 = (Aig_Obj_t *)pObj1->pData;
        if ( !Saig_ObjIsLo(p0, pObj0) )
            printf( "Mismatch between LO pairs.\n" );
    }
}

/**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;
    int i, k, iFan;
    Vec_PtrClear( vNodes );
    Aig_ManIncrementTravId( p );
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
            continue;
        if ( pObj->pData != NULL )
            continue;
        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 );
            }
        }
        Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )  
        {
            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 );
            }
        }
    }
}

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

  Synopsis    [Establishes relationship between nodes using pairing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_MatchingCountUnmached( Aig_Man_t * p )
{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
            continue;
        if ( pObj->pData != NULL )
            continue;
        Counter++;
    }
    return Counter;
}

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

  Synopsis    [Establishes relationship between nodes using pairing.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose )
{
    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 )
    {
        int nUnmached = Ssw_MatchingCountUnmached(p0);
        printf( "Extending islands by %d steps:\n", nDist );
        printf( "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
            0, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0), 
            nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
    }
    for ( d = 0; d < nDist; d++ )
    {
        Ssw_MatchingExtendOne( p0, vNodes0 );
        Ssw_MatchingExtendOne( p1, vNodes1 );
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pNext0, k )
        {
            pNext1 = (Aig_Obj_t *)pNext0->pData;
            if ( pNext1 == NULL )
                continue;
            assert( pNext1->pData == pNext0 );
            if ( Saig_ObjIsPi(p0, pNext1) )
                continue;
            pNext0->pData = NULL;
            pNext1->pData = NULL;
        }
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pNext0, k )
        {
            pNext1 = (Aig_Obj_t *)pNext0->pData;
            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);
            printf( "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
                d+1, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0), 
                nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
        }
    }
    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 )
            continue;
        pObj1 = Aig_ObjCreatePi( p1 );
        pObj0->pData = pObj1;
        pObj1->pData = pObj0;
        Vec_PtrPush( vNewLis, pObj0Li );
    }
    // add missing nodes in the topological order
    Aig_ManForEachNode( p0, pObj0, i )
    {
        if ( pObj0->pData != NULL )
            continue;
        pObj1 = Aig_And( p1, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
        pObj0->pData = pObj1;
        pObj1->pData = pObj0;
    }
    // create register outputs in p0 that are absent in p1
    Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i )
        Aig_ObjCreatePo( p1, Aig_ObjChild0Copy(pObj0Li) );
    // increment the number of registers
    Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
    Vec_PtrFree( vNewLis );
}


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

  Synopsis    [Derives matching for all pairs.]

  Description [Modifies both AIGs.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
{
    Vec_Int_t * vPairsNew;
    Aig_Obj_t * pObj0, * pObj1;
    int i;
    // check correctness
    assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) );
    assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) );
    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 )
    {
        if ( Aig_ObjIsPo(pObj0) )
            continue;
        pObj1 = (Aig_Obj_t *)pObj0->pData;
        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.]
               
  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;
        if ( Aig_ObjIsNone((Aig_Obj_t *)pObj0->pData) || Aig_ObjIsNone((Aig_Obj_t *)pObj1->pData) )
            continue;
        // get the miter nodes
        pObj0 = (Aig_Obj_t *)pObj0->pData;
        pObj1 = (Aig_Obj_t *)pObj1->pData;
        assert( !Aig_IsComplement(pObj0) );
        assert( !Aig_IsComplement(pObj1) );
        assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
        if ( Aig_ObjIsPo(pObj0) )
            continue;
        assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) );
        assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) );
        assert( pObj0->Id < pObj1->Id );
        Vec_IntPush( vPairsMiter, pObj0->Id );
        Vec_IntPush( vPairsMiter, pObj1->Id );
    }
    return vPairsMiter;
}





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

  Synopsis    [Solves SEC using structural similarity.]

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

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
{
    Ssw_Man_t * p; 
    Vec_Int_t * vPairsAll, * vPairsMiter;
    Aig_Man_t * pMiter, * pAigNew;
    // 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 );
    // start the induction manager
    p = Ssw_ManCreate( pMiter, pPars );
    // create equivalence classes using these IDs
    if ( p->pPars->fPartSigCorr )
        p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
    else
        p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
    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 );
            printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
        }
        else
            printf( "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
    }
    p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
    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 );
    // perform refinement of classes
    pAigNew = Ssw_SignalCorrespondenceRefine( p );
    // cleanup
    Ssw_ManStop( p );
    Aig_ManStop( pMiter );
    Vec_IntFree( vPairsMiter );
    return pAigNew;
}

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

  Synopsis    [Solves SEC with structural similarity.]

  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.]
               
  SideEffects [The managers will be updated by adding "islands of difference".]

  SeeAlso     []

***********************************************************************/
int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars )
{
    Ssw_Pars_t Pars;
    Aig_Man_t * pAigRes;
    int RetValue, clk = clock();
    // 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
    RetValue = Ssw_MiterStatus( pAigRes, 1 );
    if ( RetValue == 1 )
        printf( "Verification successful.  " );
    else if ( RetValue == 0 )
        printf( "Verification failed with a counter-example.  " );
    else
        printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
    ABC_PRT( "Time", clock() - clk );
    Aig_ManStop( pAigRes );
    return RetValue;
}

/**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 )
    {
        if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
            continue;
        Vec_IntPush( vPairs, i );
        Vec_IntPush( vPairs, i );
    }
    return vPairs;
}

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

  Synopsis    [Solves SEC with structural similarity.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars )
{
    Vec_Int_t * vPairs;
    Aig_Man_t * pPart0, * pPart1;
    int RetValue;
    if ( pPars->fVerbose )
        printf( "Performing sequential verification using structural similarity.\n" );
    // consider the case when a miter is given
    if ( p1 == NULL )
    {
        if ( pPars->fVerbose )
        {
            Aig_ManPrintStats( p0 );
        }
        // demiter the miter
        if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
        {
            printf( "Demitering has failed.\n" );
            return -1;
        }
    }
    else
    {
        pPart0 = Aig_ManDupSimple( p0 );
        pPart1 = Aig_ManDupSimple( p1 );
    }
    if ( pPars->fVerbose )
    {
//        Aig_ManPrintStats( pPart0 );
//        Aig_ManPrintStats( pPart1 );
        if ( p1 == NULL )
        {
//        Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
//        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
//        printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
        }
    }
    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 );
    Aig_ManStop( pPart0 );
    Aig_ManStop( pPart1 );
    Vec_IntFree( vPairs );
    return RetValue;
}

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


ABC_NAMESPACE_IMPL_END