sswIslands.c

Go to the documentation of this file.

 
#include "sswInt.h"
 
ABC_NAMESPACE_IMPL_START
 



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 );
}

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_ManCi( p1, i );
        assert( pObj0->pData == pObj1 );
        assert( pObj1->pData == pObj0 );
    }
    // make sure the POs are not matched
    Aig_ManForEachCo( p0, pObj0, i )
    {
        pObj1 = Aig_ManCo( 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) )
            Abc_Print( 1, "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) )
            Abc_Print( 1, "Mismatch between LO pairs.\n" );
    }
}

void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
{
    Aig_Obj_t * pNext, * pObj;
    int i, k, iFan = -1;
    Vec_PtrClear( vNodes );
    Aig_ManIncrementTravId( p );
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(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 );
            }
        }
    }
}

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_ObjIsCi(pObj) )
            continue;
        if ( pObj->pData != NULL )
            continue;
        Counter++;
    }
    return Counter;
}

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);
        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),
            nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(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);
            Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
                d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
                nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
        }
    }
    Vec_PtrFree( vNodes0 );
    Vec_PtrFree( vNodes1 );
    Aig_ManFanoutStop(p0);
    Aig_ManFanoutStop(p1);
}

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_ObjCreateCi( 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_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) );
    // increment the number of registers
    Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
    Vec_PtrFree( vNewLis );
}
 

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_ManCiNum(p0) == Aig_ManCiNum(p1) );
    assert( Aig_ManCoNum(p0) == Aig_ManCoNum(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_ObjIsCo(pObj0) )
            continue;
        pObj1 = (Aig_Obj_t *)pObj0->pData;
        Vec_IntPush( vPairsNew, pObj0->Id );
        Vec_IntPush( vPairsNew, pObj1->Id );
    }
    return vPairsNew;
}
 
 
 
 

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_ObjIsCo(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;
}
 
 
 
 

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->fConstCorr, 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 );
            Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
        }
        else
            Abc_Print( 1, "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;
}

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;
    abctime clk = Abc_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 )
        Abc_Print( 1, "Verification successful.  " );
    else if ( RetValue == 0 )
        Abc_Print( 1, "Verification failed with a counter-example.  " );
    else
        Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ",
            Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
    ABC_PRT( "Time", Abc_Clock() - clk );
    Aig_ManStop( pAigRes );
    return RetValue;
}

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_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
            continue;
        Vec_IntPush( vPairs, i );
        Vec_IntPush( vPairs, i );
    }
    return vPairs;
}

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 )
        Abc_Print( 1, "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 ) )
        {
            Abc_Print( 1, "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 );
//        Abc_Print( 1, "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;
}

 
 
ABC_NAMESPACE_IMPL_END