diff options
Diffstat (limited to 'src/aig/ssw/sswPairs.c')
| -rw-r--r-- | src/aig/ssw/sswPairs.c | 477 |
1 files changed, 0 insertions, 477 deletions
diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c deleted file mode 100644 index 0aba942f..00000000 --- a/src/aig/ssw/sswPairs.c +++ /dev/null @@ -1,477 +0,0 @@ -/**CFile**************************************************************** - - FileName [sswPairs.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Inductive prover with constraints.] - - Synopsis [Calls to the SAT solver.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - September 1, 2008.] - - Revision [$Id: sswPairs.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "sswInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Reports the status of the miter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose ) -{ - Aig_Obj_t * pObj, * pChild; - int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; -// if ( p->pData ) -// return 0; - Saig_ManForEachPo( p, pObj, i ) - { - pChild = Aig_ObjChild0(pObj); - // check if the output is constant 0 - if ( pChild == Aig_ManConst0(p) ) - { - CountConst0++; - continue; - } - // check if the output is constant 1 - if ( pChild == Aig_ManConst1(p) ) - { - CountNonConst0++; - continue; - } - // check if the output is a primary input - if ( p->nRegs == 0 && Aig_ObjIsPi(Aig_Regular(pChild)) ) - { - CountNonConst0++; - continue; - } - // check if the output can be not constant 0 - if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) ) - { - CountNonConst0++; - continue; - } - CountUndecided++; - } - - if ( fVerbose ) - { - printf( "Miter has %d outputs. ", Saig_ManPoNum(p) ); - printf( "Const0 = %d. ", CountConst0 ); - printf( "NonConst0 = %d. ", CountNonConst0 ); - printf( "Undecided = %d. ", CountUndecided ); - printf( "\n" ); - } - - if ( CountNonConst0 ) - return 0; - if ( CountUndecided ) - return -1; - return 1; -} - -/**Function************************************************************* - - Synopsis [Transfer equivalent pairs to the miter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Ssw_TransferSignalPairs( Aig_Man_t * pMiter, Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2 ) -{ - Vec_Int_t * vIds; - Aig_Obj_t * pObj1, * pObj2; - Aig_Obj_t * pObj1m, * pObj2m; - int i; - vIds = Vec_IntAlloc( 2 * Vec_IntSize(vIds1) ); - for ( i = 0; i < Vec_IntSize(vIds1); i++ ) - { - pObj1 = Aig_ManObj( pAig1, Vec_IntEntry(vIds1, i) ); - pObj2 = Aig_ManObj( pAig2, Vec_IntEntry(vIds2, i) ); - pObj1m = Aig_Regular((Aig_Obj_t *)pObj1->pData); - pObj2m = Aig_Regular((Aig_Obj_t *)pObj2->pData); - assert( pObj1m && pObj2m ); - if ( pObj1m == pObj2m ) - continue; - if ( pObj1m->Id < pObj2m->Id ) - { - Vec_IntPush( vIds, pObj1m->Id ); - Vec_IntPush( vIds, pObj2m->Id ); - } - else - { - Vec_IntPush( vIds, pObj2m->Id ); - Vec_IntPush( vIds, pObj1m->Id ); - } - } - return vIds; -} - -/**Function************************************************************* - - Synopsis [Transform pairs into class representation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t ** Ssw_TransformPairsIntoTempClasses( Vec_Int_t * vPairs, int nObjNumMax ) -{ - Vec_Int_t ** pvClasses; // vector of classes - int * pReprs; // mapping nodes into their representatives - int Entry, idObj, idRepr, idReprObj, idReprRepr, i; - // allocate data-structures - pvClasses = ABC_CALLOC( Vec_Int_t *, nObjNumMax ); - pReprs = ABC_ALLOC( int, nObjNumMax ); - for ( i = 0; i < nObjNumMax; i++ ) - pReprs[i] = -1; - // consider pairs - for ( i = 0; i < Vec_IntSize(vPairs); i += 2 ) - { - // get both objects - idRepr = Vec_IntEntry( vPairs, i ); - idObj = Vec_IntEntry( vPairs, i+1 ); - assert( idObj > 0 ); - assert( (pReprs[idRepr] == -1) || (pvClasses[pReprs[idRepr]] != NULL) ); - assert( (pReprs[idObj] == -1) || (pvClasses[pReprs[idObj] ] != NULL) ); - // get representatives of both objects - idReprRepr = pReprs[idRepr]; - idReprObj = pReprs[idObj]; - // check different situations - if ( idReprRepr == -1 && idReprObj == -1 ) - { // they do not have classes - // create a class - pvClasses[idRepr] = Vec_IntAlloc( 4 ); - Vec_IntPush( pvClasses[idRepr], idRepr ); - Vec_IntPush( pvClasses[idRepr], idObj ); - pReprs[ idRepr ] = idRepr; - pReprs[ idObj ] = idRepr; - } - else if ( idReprRepr >= 0 && idReprObj == -1 ) - { // representative has a class - // add iObj to the same class - Vec_IntPushUniqueOrder( pvClasses[idReprRepr], idObj ); - pReprs[ idObj ] = idReprRepr; - } - else if ( idReprRepr == -1 && idReprObj >= 0 ) - { // object has a class - assert( idReprObj != idRepr ); - if ( idReprObj < idRepr ) - { // add idRepr to the same class - Vec_IntPushUniqueOrder( pvClasses[idReprObj], idRepr ); - pReprs[ idRepr ] = idReprObj; - } - else // if ( idReprObj > idRepr ) - { // make idRepr new representative - Vec_IntPushFirst( pvClasses[idReprObj], idRepr ); - pvClasses[idRepr] = pvClasses[idReprObj]; - pvClasses[idReprObj] = NULL; - // set correct representatives of each node - Vec_IntForEachEntry( pvClasses[idRepr], Entry, i ) - pReprs[ Entry ] = idRepr; - } - } - else // if ( idReprRepr >= 0 && idReprObj >= 0 ) - { // both have classes - if ( idReprRepr == idReprObj ) - { // the classes are the same - // nothing to do - } - else - { // the classes are different - // find the repr of the new class - if ( idReprRepr < idReprObj ) - { - Vec_IntForEachEntry( pvClasses[idReprObj], Entry, i ) - { - Vec_IntPushUniqueOrder( pvClasses[idReprRepr], Entry ); - pReprs[ Entry ] = idReprRepr; - } - Vec_IntFree( pvClasses[idReprObj] ); - pvClasses[idReprObj] = NULL; - } - else // if ( idReprRepr > idReprObj ) - { - Vec_IntForEachEntry( pvClasses[idReprRepr], Entry, i ) - { - Vec_IntPushUniqueOrder( pvClasses[idReprObj], Entry ); - pReprs[ Entry ] = idReprObj; - } - Vec_IntFree( pvClasses[idReprRepr] ); - pvClasses[idReprRepr] = NULL; - } - } - } - } - ABC_FREE( pReprs ); - return pvClasses; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ssw_FreeTempClasses( Vec_Int_t ** pvClasses, int nObjNumMax ) -{ - int i; - for ( i = 0; i < nObjNumMax; i++ ) - if ( pvClasses[i] ) - Vec_IntFree( pvClasses[i] ); - ABC_FREE( pvClasses ); -} - -/**Function************************************************************* - - Synopsis [Performs signal correspondence for the miter of two AIGs with node pairs defined.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ) -{ - Ssw_Man_t * p; - Aig_Man_t * pAigNew, * pMiter; - Ssw_Pars_t Pars; - Vec_Int_t * vPairs; - Vec_Int_t ** pvClasses; - assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) ); - // create sequential miter - pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 ); - Aig_ManCleanup( pMiter ); - // transfer information to the miter - vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 ); - // create representation of the classes - pvClasses = Ssw_TransformPairsIntoTempClasses( vPairs, Aig_ManObjNumMax(pMiter) ); - Vec_IntFree( vPairs ); - // if parameters are not given, create them - if ( pPars == NULL ) - Ssw_ManSetDefaultParams( pPars = &Pars ); - // start the induction manager - p = Ssw_ManCreate( pMiter, pPars ); - // create equivalence classes using these IDs - p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses ); - p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + 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_FreeTempClasses( pvClasses, Aig_ManObjNumMax(pMiter) ); - Ssw_ManStop( p ); - Aig_ManStop( pMiter ); - return pAigNew; -} - -/**Function************************************************************* - - Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ) -{ - Aig_Man_t * pAigNew, * pAigRes; - Ssw_Pars_t Pars, * pPars = &Pars; - Vec_Int_t * vIds1, * vIds2; - Aig_Obj_t * pObj, * pRepr; - int RetValue, i, clk = clock(); - Ssw_ManSetDefaultParams( pPars ); - pPars->fVerbose = 1; - pAigNew = Ssw_SignalCorrespondence( pAig, pPars ); - // record pairs of equivalent nodes - vIds1 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) ); - vIds2 = Vec_IntAlloc( Aig_ManObjNumMax(pAig) ); - Aig_ManForEachObj( pAig, pObj, i ) - { - pRepr = Aig_Regular((Aig_Obj_t *)pObj->pData); - if ( pRepr == NULL ) - continue; - if ( Aig_ManObj(pAigNew, pRepr->Id) == NULL ) - continue; -/* - if ( Aig_ObjIsNode(pObj) ) - printf( "n " ); - else if ( Saig_ObjIsPi(pAig, pObj) ) - printf( "pi " ); - else if ( Saig_ObjIsLo(pAig, pObj) ) - printf( "lo " ); -*/ - Vec_IntPush( vIds1, Aig_ObjId(pObj) ); - Vec_IntPush( vIds2, Aig_ObjId(pRepr) ); - } - printf( "Recorded %d pairs (before: %d after: %d).\n", Vec_IntSize(vIds1), Aig_ManObjNumMax(pAig), Aig_ManObjNumMax(pAigNew) ); - // try the new AIGs - pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig, pAigNew, vIds1, vIds2, pPars ); - Vec_IntFree( vIds1 ); - Vec_IntFree( vIds2 ); - // report the results - RetValue = Ssw_MiterStatus( pAigRes, 1 ); - if ( RetValue == 1 ) - printf( "Verification successful. " ); - else if ( RetValue == 0 ) - printf( "Verification failed with the counter-example. " ); - else - printf( "Verification UNDECIDED. Remaining registers %d (total %d). ", - Aig_ManRegNum(pAigRes), Aig_ManRegNum(pAig) + Aig_ManRegNum(pAigNew) ); - ABC_PRT( "Time", clock() - clk ); - // cleanup - Aig_ManStop( pAigNew ); - return pAigRes; -} - -/**Function************************************************************* - - Synopsis [Runs inductive SEC for the miter of two AIGs with node pairs defined.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ) -{ - Aig_Man_t * pAigRes; - int RetValue, clk = clock(); - assert( vIds1 != NULL && vIds2 != NULL ); - // try the new AIGs - printf( "Performing specialized verification with node pairs.\n" ); - pAigRes = Ssw_SignalCorrespondenceWithPairs( pAig1, pAig2, vIds1, vIds2, pPars ); - // report the results - 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(pAig1) + Aig_ManRegNum(pAig2) ); - ABC_PRT( "Time", clock() - clk ); - // cleanup - Aig_ManStop( pAigRes ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Runs inductive SEC for the miter of two AIGs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) -{ - Aig_Man_t * pAigRes, * pMiter; - int RetValue, clk = clock(); - // try the new AIGs - printf( "Performing general verification without node pairs.\n" ); - pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 ); - Aig_ManCleanup( pMiter ); - pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); - Aig_ManStop( pMiter ); - // report the results - 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(pAig1) + Aig_ManRegNum(pAig2) ); - ABC_PRT( "Time", clock() - clk ); - // cleanup - Aig_ManStop( pAigRes ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Runs inductive SEC for the miter of two AIGs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ) -{ - Aig_Man_t * pAigRes; - int RetValue, clk = clock(); - // try the new AIGs -// printf( "Performing general verification without node pairs.\n" ); - pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); - // report the results - 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(pMiter) ); - ABC_PRT( "Time", clock() - clk ); - // cleanup - Aig_ManStop( pAigRes ); - return RetValue; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |