diff options
Diffstat (limited to 'src/proof/ssw/sswIslands.c')
| -rw-r--r-- | src/proof/ssw/sswIslands.c | 598 |
1 files changed, 598 insertions, 0 deletions
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c new file mode 100644 index 00000000..0802aca5 --- /dev/null +++ b/src/proof/ssw/sswIslands.c @@ -0,0 +1,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->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 ); + 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 + |