| /**CFile**************************************************************** |
| |
| FileName [bm.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Boolean Matching package.] |
| |
| Synopsis [Check P-equivalence and PP-equivalence of two circuits.] |
| |
| Author [Hadi Katebi] |
| |
| Affiliation [University of Michigan] |
| |
| Date [Ver. 1.0. Started - January, 2009.] |
| |
| Revision [No revisions so far] |
| |
| Comments [This is the cleaned up version of the code I used for DATE 2010 publication.] |
| [If you have any question or if you find a bug, contact me at hadik@umich.edu.] |
| [I don't guarantee that I can fix all the bugs, but I can definitely point you to |
| the right direction so you can fix the bugs yourself]. |
| |
| Debugging [There are some part of the code that are commented out. Those parts mostly print |
| the contents of the data structures to the standard output. Un-comment them if you |
| find them useful for debugging.] |
| |
| ***********************************************************************/ |
| |
| #include "base/abc/abc.h" |
| #include "opt/sim/sim.h" |
| #include "sat/bsat/satSolver.h" |
| //#include "bdd/extrab/extraBdd.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| #define FALSE 0 |
| #define TRUE 1 |
| |
| int match1by1(Abc_Ntk_t * pNtk1, Vec_Ptr_t ** nodesInLevel1, Vec_Int_t ** iMatch1, Vec_Int_t ** iDep1, Vec_Int_t * matchedInputs1, int * iGroup1, Vec_Int_t ** oMatch1, int * oGroup1, |
| Abc_Ntk_t * pNtk2, Vec_Ptr_t ** nodesInLevel2, Vec_Int_t ** iMatch2, Vec_Int_t ** iDep2, Vec_Int_t * matchedInputs2, int * iGroup2, Vec_Int_t ** oMatch2, int * oGroup2, |
| Vec_Int_t * matchedOutputs1, Vec_Int_t * matchedOutputs2, Vec_Int_t * oMatchedGroups, Vec_Int_t * iNonSingleton, int ii, int idx); |
| |
| int Abc_NtkBmSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Vec_Ptr_t * iMatchPairs, Vec_Ptr_t * oMatchPairs, Vec_Int_t * mismatch, int mode); |
| |
| void getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep) |
| { |
| Vec_Ptr_t * vSuppFun; |
| int i, j; |
| |
| vSuppFun = Sim_ComputeFunSupp(pNtk, 0); |
| for(i = 0; i < Abc_NtkPoNum(pNtk); i++) { |
| char * seg = (char *)vSuppFun->pArray[i]; |
| |
| for(j = 0; j < Abc_NtkPiNum(pNtk); j+=8) { |
| if(((*seg) & 0x01) == 0x01) |
| Vec_IntPushOrder(oDep[i], j); |
| if(((*seg) & 0x02) == 0x02) |
| Vec_IntPushOrder(oDep[i], j+1); |
| if(((*seg) & 0x04) == 0x04) |
| Vec_IntPushOrder(oDep[i], j+2); |
| if(((*seg) & 0x08) == 0x08) |
| Vec_IntPushOrder(oDep[i], j+3); |
| if(((*seg) & 0x10) == 0x10) |
| Vec_IntPushOrder(oDep[i], j+4); |
| if(((*seg) & 0x20) == 0x20) |
| Vec_IntPushOrder(oDep[i], j+5); |
| if(((*seg) & 0x40) == 0x40) |
| Vec_IntPushOrder(oDep[i], j+6); |
| if(((*seg) & 0x80) == 0x80) |
| Vec_IntPushOrder(oDep[i], j+7); |
| |
| seg++; |
| } |
| } |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk); i++) |
| for(j = 0; j < Vec_IntSize(oDep[i]); j++) |
| Vec_IntPush(iDep[Vec_IntEntry(oDep[i], j)], i); |
| |
| |
| /*for(i = 0; i < Abc_NtkPoNum(pNtk); i++) |
| { |
| printf("Output %d: ", i); |
| for(j = 0; j < Vec_IntSize(oDep[i]); j++) |
| printf("%d ", Vec_IntEntry(oDep[i], j)); |
| printf("\n"); |
| } |
| |
| printf("\n"); |
| |
| for(i = 0; i < Abc_NtkPiNum(pNtk); i++) |
| { |
| printf("Input %d: ", i); |
| for(j = 0; j < Vec_IntSize(iDep[i]); j++) |
| printf("%d ", Vec_IntEntry(iDep[i], j)); |
| printf("\n"); |
| } |
| |
| printf("\n"); */ |
| } |
| |
| void initMatchList(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep, Vec_Int_t** iMatch, int* iLastItem, Vec_Int_t** oMatch, int* oLastItem, int* iGroup, int* oGroup, int p_equivalence) |
| { |
| int i, j, curr; |
| Vec_Int_t** temp; |
| |
| if(!p_equivalence) { |
| temp = ABC_ALLOC( Vec_Int_t*, Abc_NtkPiNum(pNtk)+1); |
| |
| for(i = 0; i < Abc_NtkPiNum(pNtk)+1; i++) |
| temp[i] = Vec_IntAlloc( 0 ); |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk); i++) |
| Vec_IntPush(temp[Vec_IntSize(oDep[i])], i); |
| |
| curr = 0; |
| for(i = 0; i < Abc_NtkPiNum(pNtk)+1; i++) |
| { |
| if(Vec_IntSize(temp[i]) == 0) |
| Vec_IntFree( temp[i] ); |
| |
| else |
| { |
| oMatch[curr] = temp[i]; |
| |
| for(j = 0; j < Vec_IntSize(temp[i]); j++) |
| oGroup[Vec_IntEntry(oMatch[curr], j)] = curr; |
| |
| curr++; |
| } |
| } |
| |
| *oLastItem = curr; |
| |
| ABC_FREE( temp ); |
| } |
| else { |
| // the else part fixes the outputs for P-equivalence checking |
| for(i = 0; i < Abc_NtkPoNum(pNtk); i++) |
| { |
| Vec_IntPush(oMatch[i], i); |
| oGroup[i] = i; |
| (*oLastItem) = Abc_NtkPoNum(pNtk); |
| } |
| } |
| |
| /*for(j = 0; j < *oLastItem; j++) |
| { |
| printf("oMatch %d: ", j); |
| for(i = 0; i < Vec_IntSize(oMatch[j]); i++) |
| printf("%d ", Vec_IntEntry(oMatch[j], i)); |
| printf("\n"); |
| } |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk); i++) |
| printf("%d: %d ", i, oGroup[i]);*/ |
| |
| ////////////////////////////////////////////////////////////////////////////// |
| |
| temp = ABC_ALLOC( Vec_Int_t*, Abc_NtkPoNum(pNtk)+1 ); |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk)+1; i++) |
| temp[i] = Vec_IntAlloc( 0 ); |
| |
| for(i = 0; i < Abc_NtkPiNum(pNtk); i++) |
| Vec_IntPush(temp[Vec_IntSize(iDep[i])], i); |
| |
| curr = 0; |
| for(i = 0; i < Abc_NtkPoNum(pNtk)+1; i++) |
| { |
| if(Vec_IntSize(temp[i]) == 0) |
| Vec_IntFree( temp[i] ); |
| else |
| { |
| iMatch[curr] = temp[i]; |
| for(j = 0; j < Vec_IntSize(iMatch[curr]); j++) |
| iGroup[Vec_IntEntry(iMatch[curr], j)] = curr; |
| curr++; |
| } |
| } |
| |
| *iLastItem = curr; |
| |
| ABC_FREE( temp ); |
| |
| /*printf("\n"); |
| for(j = 0; j < *iLastItem; j++) |
| { |
| printf("iMatch %d: ", j); |
| for(i = 0; i < Vec_IntSize(iMatch[j]); i++) |
| printf("%d ", Vec_IntEntry(iMatch[j], i)); |
| printf("\n"); |
| } |
| |
| for(i = 0; i < Abc_NtkPiNum(pNtk); i++) |
| printf("%d: %d ", i, iGroup[i]); |
| printf("\n");*/ |
| } |
| |
| void iSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, int* oGroup) |
| { |
| int i, j, k; |
| Vec_Int_t * temp; |
| Vec_Int_t * oGroupList; |
| |
| oGroupList = Vec_IntAlloc( 10 ); |
| |
| for(i = 0; i < Abc_NtkPiNum(pNtk); i++) |
| { |
| if(Vec_IntSize(iDep[i]) == 1) |
| continue; |
| |
| temp = Vec_IntAlloc( Vec_IntSize(iDep[i]) ); |
| |
| for(j = 0; j < Vec_IntSize(iDep[i]); j++) |
| Vec_IntPushUniqueOrder(oGroupList, oGroup[Vec_IntEntry(iDep[i], j)]); |
| |
| for(j = 0; j < Vec_IntSize(oGroupList); j++) |
| { |
| for(k = 0; k < Vec_IntSize(iDep[i]); k++) |
| if(oGroup[Vec_IntEntry(iDep[i], k)] == Vec_IntEntry(oGroupList, j)) |
| { |
| Vec_IntPush( temp, Vec_IntEntry(iDep[i], k) ); |
| Vec_IntRemove( iDep[i], Vec_IntEntry(iDep[i], k) ); |
| k--; |
| } |
| } |
| |
| Vec_IntFree( iDep[i] ); |
| iDep[i] = temp; |
| Vec_IntClear( oGroupList ); |
| |
| /*printf("Input %d: ", i); |
| for(j = 0; j < Vec_IntSize(iDep[i]); j++) |
| printf("%d ", Vec_IntEntry(iDep[i], j)); |
| printf("\n");*/ |
| } |
| |
| Vec_IntFree( oGroupList ); |
| } |
| |
| void oSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, int* iGroup) |
| { |
| int i, j, k; |
| Vec_Int_t * temp; |
| Vec_Int_t * iGroupList; |
| |
| iGroupList = Vec_IntAlloc( 10 ); |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk); i++) |
| { |
| if(Vec_IntSize(oDep[i]) == 1) |
| continue; |
| |
| temp = Vec_IntAlloc( Vec_IntSize(oDep[i]) ); |
| |
| for(j = 0; j < Vec_IntSize(oDep[i]); j++) |
| Vec_IntPushUniqueOrder(iGroupList, iGroup[Vec_IntEntry(oDep[i], j)]); |
| |
| for(j = 0; j < Vec_IntSize(iGroupList); j++) |
| { |
| for(k = 0; k < Vec_IntSize(oDep[i]); k++) |
| if(iGroup[Vec_IntEntry(oDep[i], k)] == Vec_IntEntry(iGroupList, j)) |
| { |
| Vec_IntPush( temp, Vec_IntEntry(oDep[i], k) ); |
| Vec_IntRemove( oDep[i], Vec_IntEntry(oDep[i], k) ); |
| k--; |
| } |
| } |
| |
| Vec_IntFree( oDep[i] ); |
| oDep[i] = temp; |
| Vec_IntClear( iGroupList ); |
| |
| /*printf("Output %d: ", i); |
| for(j = 0; j < Vec_IntSize(oDep[i]); j++) |
| printf("%d ", Vec_IntEntry(oDep[i], j)); |
| printf("\n");*/ |
| } |
| |
| Vec_IntFree( iGroupList ); |
| } |
| |
| int oSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, Vec_Int_t** oMatch, int* oGroup, int* oLastItem, int* iGroup) |
| { |
| int i, j, k; |
| int numOfItemsAdded; |
| Vec_Int_t * array, * sortedArray; |
| |
| numOfItemsAdded = 0; |
| |
| for(i = 0; i < *oLastItem; i++) |
| { |
| if(Vec_IntSize(oMatch[i]) == 1) |
| continue; |
| |
| array = Vec_IntAlloc( Vec_IntSize(oMatch[i]) ); |
| sortedArray = Vec_IntAlloc( Vec_IntSize(oMatch[i]) ); |
| |
| for(j = 0; j < Vec_IntSize(oMatch[i]); j++) |
| { |
| int factor, encode; |
| |
| encode = 0; |
| factor = 1; |
| |
| for(k = 0; k < Vec_IntSize(oDep[Vec_IntEntry(oMatch[i], j)]); k++) |
| encode += iGroup[Vec_IntEntry(oDep[Vec_IntEntry(oMatch[i], j)], k)] * factor; |
| |
| Vec_IntPush(array, encode); |
| Vec_IntPushUniqueOrder(sortedArray, encode); |
| |
| if( encode < 0) |
| printf("WARNING! Integer overflow!"); |
| |
| //printf("%d ", Vec_IntEntry(array, j)); |
| } |
| |
| while( Vec_IntSize(sortedArray) > 1 ) |
| { |
| for(k = 0; k < Vec_IntSize(oMatch[i]); k++) |
| { |
| if(Vec_IntEntry(array, k) == Vec_IntEntryLast(sortedArray)) |
| { |
| Vec_IntPush(oMatch[*oLastItem+numOfItemsAdded], Vec_IntEntry(oMatch[i], k)); |
| oGroup[Vec_IntEntry(oMatch[i], k)] = *oLastItem+numOfItemsAdded; |
| Vec_IntRemove( oMatch[i], Vec_IntEntry(oMatch[i], k) ); |
| Vec_IntRemove( array, Vec_IntEntry(array, k) ); |
| k--; |
| } |
| } |
| numOfItemsAdded++; |
| Vec_IntPop(sortedArray); |
| } |
| |
| Vec_IntFree( array ); |
| Vec_IntFree( sortedArray ); |
| //printf("\n"); |
| } |
| |
| *oLastItem += numOfItemsAdded; |
| |
| /*printf("\n"); |
| for(j = 0; j < *oLastItem ; j++) |
| { |
| printf("oMatch %d: ", j); |
| for(i = 0; i < Vec_IntSize(oMatch[j]); i++) |
| printf("%d ", Vec_IntEntry(oMatch[j], i)); |
| printf("\n"); |
| }*/ |
| |
| return numOfItemsAdded; |
| } |
| |
| int iSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** iMatch, int* iGroup, int* iLastItem, int* oGroup) |
| { |
| int i, j, k; |
| int numOfItemsAdded = 0; |
| Vec_Int_t * array, * sortedArray; |
| |
| for(i = 0; i < *iLastItem; i++) |
| { |
| if(Vec_IntSize(iMatch[i]) == 1) |
| continue; |
| |
| array = Vec_IntAlloc( Vec_IntSize(iMatch[i]) ); |
| sortedArray = Vec_IntAlloc( Vec_IntSize(iMatch[i]) ); |
| |
| for(j = 0; j < Vec_IntSize(iMatch[i]); j++) |
| { |
| int factor, encode; |
| |
| encode = 0; |
| factor = 1; |
| |
| for(k = 0; k < Vec_IntSize(iDep[Vec_IntEntry(iMatch[i], j)]); k++) |
| encode += oGroup[Vec_IntEntry(iDep[Vec_IntEntry(iMatch[i], j)], k)] * factor; |
| |
| Vec_IntPush(array, encode); |
| Vec_IntPushUniqueOrder(sortedArray, encode); |
| |
| //printf("%d ", Vec_IntEntry(array, j)); |
| } |
| |
| while( Vec_IntSize(sortedArray) > 1 ) |
| { |
| for(k = 0; k < Vec_IntSize(iMatch[i]); k++) |
| { |
| if(Vec_IntEntry(array, k) == Vec_IntEntryLast(sortedArray)) |
| { |
| Vec_IntPush(iMatch[*iLastItem+numOfItemsAdded], Vec_IntEntry(iMatch[i], k)); |
| iGroup[Vec_IntEntry(iMatch[i], k)] = *iLastItem+numOfItemsAdded; |
| Vec_IntRemove( iMatch[i], Vec_IntEntry(iMatch[i], k) ); |
| Vec_IntRemove( array, Vec_IntEntry(array, k) ); |
| k--; |
| } |
| } |
| numOfItemsAdded++; |
| Vec_IntPop(sortedArray); |
| } |
| |
| Vec_IntFree( array ); |
| Vec_IntFree( sortedArray ); |
| //printf("\n"); |
| } |
| |
| *iLastItem += numOfItemsAdded; |
| |
| /*printf("\n"); |
| for(j = 0; j < *iLastItem ; j++) |
| { |
| printf("iMatch %d: ", j); |
| for(i = 0; i < Vec_IntSize(iMatch[j]); i++) |
| printf("%d ", Vec_IntEntry(iMatch[j], i)); |
| printf("\n"); |
| }*/ |
| |
| return numOfItemsAdded; |
| } |
| |
| Vec_Ptr_t ** findTopologicalOrder( Abc_Ntk_t * pNtk ) |
| { |
| Vec_Ptr_t ** vNodes; |
| Abc_Obj_t * pObj, * pFanout; |
| int i, k; |
| |
| extern void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); |
| |
| // start the array of nodes |
| vNodes = ABC_ALLOC(Vec_Ptr_t *, Abc_NtkPiNum(pNtk)); |
| for(i = 0; i < Abc_NtkPiNum(pNtk); i++) |
| vNodes[i] = Vec_PtrAlloc(50); |
| |
| Abc_NtkForEachCi( pNtk, pObj, i ) |
| { |
| // set the traversal ID |
| Abc_NtkIncrementTravId( pNtk ); |
| Abc_NodeSetTravIdCurrent( pObj ); |
| pObj = Abc_ObjFanout0Ntk(pObj); |
| Abc_ObjForEachFanout( pObj, pFanout, k ) |
| Abc_NtkDfsReverse_rec( pFanout, vNodes[i] ); |
| } |
| |
| return vNodes; |
| } |
| |
| |
| int * Abc_NtkSimulateOneNode( Abc_Ntk_t * pNtk, int * pModel, int input, Vec_Ptr_t ** topOrder ) |
| { |
| Abc_Obj_t * pNode; |
| Vec_Ptr_t * vNodes; |
| int * pValues, Value0, Value1, i; |
| |
| vNodes = Vec_PtrAlloc( 50 ); |
| /* |
| printf( "Counter example: " ); |
| Abc_NtkForEachCi( pNtk, pNode, i ) |
| printf( " %d", pModel[i] ); |
| printf( "\n" ); |
| */ |
| // increment the trav ID |
| Abc_NtkIncrementTravId( pNtk ); |
| // set the CI values |
| Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)1; |
| pNode = Abc_NtkCi(pNtk, input); |
| pNode->iTemp = pModel[input]; |
| |
| // simulate in the topological order |
| for(i = Vec_PtrSize(topOrder[input])-1; i >= 0; i--) |
| { |
| pNode = (Abc_Obj_t *)Vec_PtrEntry(topOrder[input], i); |
| |
| Value0 = ((int)(ABC_PTRUINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); |
| Value1 = ((int)(ABC_PTRUINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); |
| |
| if( pNode->iTemp != (Value0 & Value1)) |
| { |
| pNode->iTemp = (Value0 & Value1); |
| Vec_PtrPush(vNodes, pNode); |
| } |
| |
| } |
| // fill the output values |
| pValues = ABC_ALLOC( int, Abc_NtkCoNum(pNtk) ); |
| Abc_NtkForEachCo( pNtk, pNode, i ) |
| pValues[i] = ((int)(ABC_PTRUINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); |
| |
| pNode = Abc_NtkCi(pNtk, input); |
| if(pNode->pCopy == (Abc_Obj_t *)1) |
| pNode->pCopy = (Abc_Obj_t *)0; |
| else |
| pNode->pCopy = (Abc_Obj_t *)1; |
| |
| for(i = 0; i < Vec_PtrSize(vNodes); i++) |
| { |
| pNode = (Abc_Obj_t *)Vec_PtrEntry(vNodes, i); |
| |
| if(pNode->pCopy == (Abc_Obj_t *)1) |
| pNode->pCopy = (Abc_Obj_t *)0; |
| else |
| pNode->pCopy = (Abc_Obj_t *)1; |
| } |
| |
| Vec_PtrFree( vNodes ); |
| |
| return pValues; |
| } |
| |
| int refineIOBySimulation(Abc_Ntk_t *pNtk, Vec_Int_t** iMatch, int* iLastItem, int * iGroup, Vec_Int_t** iDep, Vec_Int_t** oMatch, int* oLastItem, int * oGroup, Vec_Int_t** oDep, char * vPiValues, int * observability, Vec_Ptr_t ** topOrder) |
| { |
| Abc_Obj_t * pObj; |
| int * pModel;//, ** pModel2; |
| int * output, * output2; |
| int lastItem; |
| int i, j, k; |
| Vec_Int_t * iComputedNum, * iComputedNumSorted; |
| Vec_Int_t * oComputedNum; // encoding the number of flips |
| int factor; |
| int isRefined = FALSE; |
| |
| pModel = ABC_ALLOC( int, Abc_NtkCiNum(pNtk) ); |
| |
| Abc_NtkForEachPi( pNtk, pObj, i ) |
| pModel[i] = vPiValues[i] - '0'; |
| Abc_NtkForEachLatch( pNtk, pObj, i ) |
| pModel[Abc_NtkPiNum(pNtk)+i] = pObj->iData - 1; |
| |
| output = Abc_NtkVerifySimulatePattern( pNtk, pModel ); |
| |
| oComputedNum = Vec_IntAlloc( Abc_NtkPoNum(pNtk) ); |
| for(i = 0; i < Abc_NtkPoNum(pNtk); i++) |
| Vec_IntPush(oComputedNum, 0); |
| |
| /****************************************************************************************/ |
| /********** group outputs that produce 1 and outputs that produce 0 together ************/ |
| |
| lastItem = *oLastItem; |
| for(i = 0; i < lastItem && (*oLastItem) != Abc_NtkPoNum(pNtk); i++) |
| { |
| int flag = FALSE; |
| |
| if(Vec_IntSize(oMatch[i]) == 1) |
| continue; |
| |
| for(j = 1; j < Vec_IntSize(oMatch[i]); j++) |
| if(output[Vec_IntEntry(oMatch[i], 0)] != output[Vec_IntEntry(oMatch[i], j)]) |
| { |
| flag = TRUE; |
| break; |
| } |
| |
| if(flag) |
| { |
| for(j = 0; j < Vec_IntSize(oMatch[i]); j++) |
| if(output[Vec_IntEntry(oMatch[i], j)]) |
| { |
| Vec_IntPush(oMatch[*oLastItem], Vec_IntEntry(oMatch[i], j)); |
| oGroup[Vec_IntEntry(oMatch[i], j)] = *oLastItem; |
| Vec_IntRemove(oMatch[i], Vec_IntEntry(oMatch[i], j)); |
| j--; |
| } |
| |
| (*oLastItem)++; |
| } |
| } |
| |
| if( (*oLastItem) > lastItem ) |
| { |
| isRefined = TRUE; |
| iSortDependencies(pNtk, iDep, oGroup); |
| } |
| |
| /****************************************************************************************/ |
| /************* group inputs that make the same number of flips in outpus ****************/ |
| |
| lastItem = *iLastItem; |
| for(i = 0; i < lastItem && (*iLastItem) != Abc_NtkPiNum(pNtk); i++) |
| { |
| int num; |
| |
| if(Vec_IntSize(iMatch[i]) == 1) |
| continue; |
| |
| iComputedNum = Vec_IntAlloc( Vec_IntSize(iMatch[i]) ); |
| iComputedNumSorted = Vec_IntAlloc( Vec_IntSize(iMatch[i]) ); |
| |
| for(j = 0; j < Vec_IntSize(iMatch[i]); j++) |
| { |
| if( vPiValues[Vec_IntEntry(iMatch[i], j)] == '0' ) |
| pModel[Vec_IntEntry(iMatch[i], j)] = 1; |
| else |
| pModel[Vec_IntEntry(iMatch[i], j)] = 0; |
| |
| //output2 = Abc_NtkVerifySimulatePattern( pNtk, pModel ); |
| output2 = Abc_NtkSimulateOneNode( pNtk, pModel, Vec_IntEntry(iMatch[i], j), topOrder ); |
| |
| num = 0; |
| factor = 1; |
| for(k = 0; k < Vec_IntSize(iDep[Vec_IntEntry(iMatch[i], j)]); k++) |
| { |
| int outputIndex = Vec_IntEntry(iDep[Vec_IntEntry(iMatch[i], j)], k); |
| |
| if(output2[outputIndex]) |
| num += (oGroup[outputIndex] + 1) * factor; |
| |
| if(output[outputIndex] != output2[outputIndex]) |
| { |
| int temp = Vec_IntEntry(oComputedNum, outputIndex) + i + 1; |
| Vec_IntWriteEntry(oComputedNum, outputIndex, temp); |
| observability[Vec_IntEntry(iMatch[i], j)]++; |
| } |
| } |
| |
| Vec_IntPush(iComputedNum, num); |
| Vec_IntPushUniqueOrder(iComputedNumSorted, num); |
| |
| pModel[Vec_IntEntry(iMatch[i], j)] = vPiValues[Vec_IntEntry(iMatch[i], j)] - '0'; |
| ABC_FREE( output2 ); |
| } |
| |
| while( Vec_IntSize( iComputedNumSorted ) > 1 ) |
| { |
| for(k = 0; k < Vec_IntSize(iMatch[i]); k++) |
| { |
| if(Vec_IntEntry(iComputedNum, k) == Vec_IntEntryLast(iComputedNumSorted) ) |
| { |
| Vec_IntPush(iMatch[*iLastItem], Vec_IntEntry(iMatch[i], k)); |
| iGroup[Vec_IntEntry(iMatch[i], k)] = *iLastItem; |
| Vec_IntRemove( iMatch[i], Vec_IntEntry(iMatch[i], k) ); |
| Vec_IntRemove( iComputedNum, Vec_IntEntry(iComputedNum, k) ); |
| k--; |
| } |
| } |
| (*iLastItem)++; |
| Vec_IntPop( iComputedNumSorted ); |
| } |
| |
| Vec_IntFree( iComputedNum ); |
| Vec_IntFree( iComputedNumSorted ); |
| } |
| |
| if( (*iLastItem) > lastItem ) |
| { |
| isRefined = TRUE; |
| oSortDependencies(pNtk, oDep, iGroup); |
| } |
| |
| /****************************************************************************************/ |
| /********** encode the number of flips in each output by flipping the outputs ***********/ |
| /********** and group all the outputs that have the same encoding ***********/ |
| |
| lastItem = *oLastItem; |
| for(i = 0; i < lastItem && (*oLastItem) != Abc_NtkPoNum(pNtk); i++) |
| { |
| Vec_Int_t * encode, * sortedEncode; // encoding the number of flips |
| |
| if(Vec_IntSize(oMatch[i]) == 1) |
| continue; |
| |
| encode = Vec_IntAlloc( Vec_IntSize(oMatch[i]) ); |
| sortedEncode = Vec_IntAlloc( Vec_IntSize(oMatch[i]) ); |
| |
| for(j = 0; j < Vec_IntSize(oMatch[i]); j++) |
| { |
| Vec_IntPush(encode, Vec_IntEntry(oComputedNum, Vec_IntEntry(oMatch[i], j)) ); |
| Vec_IntPushUniqueOrder( sortedEncode, Vec_IntEntry(encode, j) ); |
| } |
| |
| while( Vec_IntSize(sortedEncode) > 1 ) |
| { |
| for(j = 0; j < Vec_IntSize(oMatch[i]); j++) |
| if(Vec_IntEntry(encode, j) == Vec_IntEntryLast(sortedEncode)) |
| { |
| Vec_IntPush(oMatch[*oLastItem], Vec_IntEntry(oMatch[i], j)); |
| oGroup[Vec_IntEntry(oMatch[i], j)] = *oLastItem; |
| Vec_IntRemove( oMatch[i], Vec_IntEntry(oMatch[i], j) ); |
| Vec_IntRemove( encode, Vec_IntEntry(encode, j) ); |
| j --; |
| } |
| |
| (*oLastItem)++; |
| Vec_IntPop( sortedEncode ); |
| } |
| |
| Vec_IntFree( encode ); |
| Vec_IntFree( sortedEncode ); |
| } |
| |
| if( (*oLastItem) > lastItem ) |
| isRefined = TRUE; |
| |
| ABC_FREE( pModel ); |
| ABC_FREE( output ); |
| Vec_IntFree( oComputedNum ); |
| |
| return isRefined; |
| } |
| |
| Abc_Ntk_t * Abc_NtkMiterBm( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Vec_Ptr_t * iCurrMatch, Vec_Ptr_t * oCurrMatch ) |
| { |
| char Buffer[1000]; |
| Abc_Ntk_t * pNtkMiter; |
| |
| pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); |
| sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName ); |
| pNtkMiter->pName = Extra_UtilStrsav(Buffer); |
| |
| //Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize ); |
| { |
| Abc_Obj_t * pObj, * pObjNew; |
| int i; |
| |
| Abc_AigConst1(pNtk1)->pCopy = Abc_AigConst1(pNtkMiter); |
| Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtkMiter); |
| |
| // create new PIs and remember them in the old PIs |
| if(iCurrMatch == NULL) |
| { |
| Abc_NtkForEachCi( pNtk1, pObj, i ) |
| { |
| pObjNew = Abc_NtkCreatePi( pNtkMiter ); |
| // remember this PI in the old PIs |
| pObj->pCopy = pObjNew; |
| pObj = Abc_NtkCi(pNtk2, i); |
| pObj->pCopy = pObjNew; |
| // add name |
| Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL ); |
| } |
| } |
| else |
| { |
| for(i = 0; i < Vec_PtrSize( iCurrMatch ); i += 2) |
| { |
| pObjNew = Abc_NtkCreatePi( pNtkMiter ); |
| pObj = (Abc_Obj_t *)Vec_PtrEntry(iCurrMatch, i); |
| pObj->pCopy = pObjNew; |
| pObj = (Abc_Obj_t *)Vec_PtrEntry(iCurrMatch, i+1); |
| pObj->pCopy = pObjNew; |
| // add name |
| Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL ); |
| } |
| } |
| |
| // create the only PO |
| pObjNew = Abc_NtkCreatePo( pNtkMiter ); |
| // add the PO name |
| Abc_ObjAssignName( pObjNew, "miter", NULL ); |
| } |
| |
| // Abc_NtkMiterAddOne( pNtk1, pNtkMiter ); |
| { |
| Abc_Obj_t * pNode; |
| int i; |
| assert( Abc_NtkIsDfsOrdered(pNtk1) ); |
| Abc_AigForEachAnd( pNtk1, pNode, i ) |
| pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); |
| } |
| |
| // Abc_NtkMiterAddOne( pNtk2, pNtkMiter ); |
| { |
| Abc_Obj_t * pNode; |
| int i; |
| assert( Abc_NtkIsDfsOrdered(pNtk2) ); |
| Abc_AigForEachAnd( pNtk2, pNode, i ) |
| pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); |
| } |
| |
| // Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize ); |
| { |
| Vec_Ptr_t * vPairs; |
| Abc_Obj_t * pMiter; |
| int i; |
| |
| vPairs = Vec_PtrAlloc( 100 ); |
| |
| // collect the CO nodes for the miter |
| if(oCurrMatch != NULL) |
| { |
| for(i = 0; i < Vec_PtrSize( oCurrMatch ); i += 2) |
| { |
| Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oCurrMatch, i)) ); |
| Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oCurrMatch, i+1)) ); |
| } |
| } |
| else |
| { |
| Abc_Obj_t * pNode; |
| |
| Abc_NtkForEachCo( pNtk1, pNode, i ) |
| { |
| Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) ); |
| pNode = Abc_NtkCo( pNtk2, i ); |
| Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) ); |
| } |
| } |
| |
| pMiter = Abc_AigMiter( (Abc_Aig_t *)pNtkMiter->pManFunc, vPairs, 0 ); |
| Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); |
| Vec_PtrFree(vPairs); |
| } |
| |
| //Abc_AigCleanup(pNtkMiter->pManFunc); |
| |
| return pNtkMiter; |
| } |
| |
| int * pValues1__, * pValues2__; |
| |
| void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, Vec_Int_t * mismatch ) |
| { |
| Vec_Ptr_t * vNodes; |
| Abc_Obj_t * pNode; |
| int nErrors, nPrinted, i, iNode = -1; |
| |
| assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) ); |
| assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) ); |
| // get the CO values under this model |
| pValues1__ = Abc_NtkVerifySimulatePattern( pNtk1, pModel ); |
| pValues2__ = Abc_NtkVerifySimulatePattern( pNtk2, pModel ); |
| // count the mismatches |
| nErrors = 0; |
| for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) |
| nErrors += (int)( pValues1__[i] != pValues2__[i] ); |
| //printf( "Verification failed for at least %d outputs: ", nErrors ); |
| // print the first 3 outputs |
| nPrinted = 0; |
| for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) |
| if ( pValues1__[i] != pValues2__[i] ) |
| { |
| if ( iNode == -1 ) |
| iNode = i; |
| //printf( " %s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) ); |
| if ( ++nPrinted == 3 ) |
| break; |
| } |
| /*if ( nPrinted != nErrors ) |
| printf( " ..." ); |
| printf( "\n" );*/ |
| // report mismatch for the first output |
| if ( iNode >= 0 ) |
| { |
| /*printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n", |
| Abc_ObjName(Abc_NtkCo(pNtk1,iNode)), pValues1[iNode], pValues2[iNode] ); |
| printf( "Input pattern: " );*/ |
| // collect PIs in the cone |
| pNode = Abc_NtkCo(pNtk1,iNode); |
| vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 ); |
| // set the PI numbers |
| Abc_NtkForEachCi( pNtk1, pNode, i ) |
| pNode->iTemp = i; |
| // print the model |
| pNode = (Abc_Obj_t *)Vec_PtrEntry( vNodes, 0 ); |
| if ( Abc_ObjIsCi(pNode) ) |
| { |
| Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i ) |
| { |
| assert( Abc_ObjIsCi(pNode) ); |
| //printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] ); |
| Vec_IntPush(mismatch, Abc_ObjId(pNode)-1); |
| Vec_IntPush(mismatch, pModel[(int)(size_t)pNode->pCopy]); |
| } |
| } |
| //printf( "\n" ); |
| Vec_PtrFree( vNodes ); |
| } |
| free( pValues1__ ); |
| free( pValues2__ ); |
| } |
| |
| int Abc_NtkMiterSatBm( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects) |
| { |
| static sat_solver * pSat = NULL; |
| lbool status; |
| int RetValue = 0; |
| abctime clk; |
| |
| extern int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ); |
| extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); |
| |
| if ( pNumConfs ) |
| *pNumConfs = 0; |
| if ( pNumInspects ) |
| *pNumInspects = 0; |
| |
| assert( Abc_NtkLatchNum(pNtk) == 0 ); |
| |
| // if ( Abc_NtkPoNum(pNtk) > 1 ) |
| // fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) ); |
| |
| // load clauses into the sat_solver |
| clk = Abc_Clock(); |
| |
| |
| |
| pSat = (sat_solver *)Abc_NtkMiterSatCreate( pNtk, 0 ); |
| |
| if ( pSat == NULL ) |
| return 1; |
| //printf( "%d \n", pSat->clauses.size ); |
| //sat_solver_delete( pSat ); |
| //return 1; |
| |
| // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); |
| // PRT( "Time", Abc_Clock() - clk ); |
| |
| // simplify the problem |
| clk = Abc_Clock(); |
| status = sat_solver_simplify(pSat); |
| // printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) ); |
| // PRT( "Time", Abc_Clock() - clk ); |
| if ( status == 0 ) |
| { |
| sat_solver_delete( pSat ); |
| // printf( "The problem is UNSATISFIABLE after simplification.\n" ); |
| return 1; |
| } |
| |
| // solve the miter |
| clk = Abc_Clock(); |
| if ( fVerbose ) |
| pSat->verbosity = 1; |
| status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 ); |
| if ( status == l_Undef ) |
| { |
| // printf( "The problem timed out.\n" ); |
| RetValue = -1; |
| } |
| else if ( status == l_True ) |
| { |
| // printf( "The problem is SATISFIABLE.\n" ); |
| RetValue = 0; |
| } |
| else if ( status == l_False ) |
| { |
| // printf( "The problem is UNSATISFIABLE.\n" ); |
| RetValue = 1; |
| } |
| else |
| assert( 0 ); |
| // PRT( "SAT sat_solver time", Abc_Clock() - clk ); |
| // printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); |
| |
| // if the problem is SAT, get the counterexample |
| if ( status == l_True ) |
| { |
| // Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk ); |
| Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk ); |
| pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); |
| Vec_IntFree( vCiIds ); |
| } |
| // free the sat_solver |
| if ( fVerbose ) |
| Sat_SolverPrintStats( stdout, pSat ); |
| |
| if ( pNumConfs ) |
| *pNumConfs = (int)pSat->stats.conflicts; |
| if ( pNumInspects ) |
| *pNumInspects = (int)pSat->stats.inspects; |
| |
| //sat_solver_store_write( pSat, "trace.cnf" ); |
| sat_solver_store_free( pSat ); |
| sat_solver_delete( pSat ); |
| return RetValue; |
| } |
| |
| int Abc_NtkBmSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Vec_Ptr_t * iMatchPairs, Vec_Ptr_t * oMatchPairs, Vec_Int_t * mismatch, int mode) |
| { |
| extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor ); |
| |
| Abc_Ntk_t * pMiter = NULL; |
| Abc_Ntk_t * pCnf; |
| int RetValue = 0; |
| |
| // get the miter of the two networks |
| if( mode == 0 ) |
| { |
| //Abc_NtkDelete( pMiter ); |
| pMiter = Abc_NtkMiterBm( pNtk1, pNtk2, iMatchPairs, oMatchPairs ); |
| } |
| else if( mode == 1 ) // add new outputs |
| { |
| int i; |
| Abc_Obj_t * pObj; |
| Vec_Ptr_t * vPairs; |
| Abc_Obj_t * pNtkMiter; |
| |
| vPairs = Vec_PtrAlloc( 100 ); |
| |
| Abc_NtkForEachCo( pMiter, pObj, i ) |
| Abc_ObjRemoveFanins( pObj ); |
| |
| for(i = 0; i < Vec_PtrSize( oMatchPairs ); i += 2) |
| { |
| Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oMatchPairs, i)) ); |
| Vec_PtrPush( vPairs, Abc_ObjChild0Copy((Abc_Obj_t *)Vec_PtrEntry(oMatchPairs, i+1)) ); |
| } |
| pNtkMiter = Abc_AigMiter( (Abc_Aig_t *)pMiter->pManFunc, vPairs, 0 ); |
| Abc_ObjAddFanin( Abc_NtkPo(pMiter,0), pNtkMiter ); |
| Vec_PtrFree( vPairs); |
| } |
| else if( mode == 2 ) // add some outputs |
| { |
| |
| } |
| else if( mode == 3) // remove all outputs |
| { |
| } |
| |
| if ( pMiter == NULL ) |
| { |
| printf("Miter computation has failed."); |
| return -1; |
| } |
| RetValue = Abc_NtkMiterIsConstant( pMiter ); |
| if ( RetValue == 0) |
| { |
| /*printf("Networks are NOT EQUIVALENT after structural hashing."); */ |
| // report the error |
| if(mismatch != NULL) |
| { |
| pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 ); |
| Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel, mismatch ); |
| ABC_FREE( pMiter->pModel ); |
| } |
| Abc_NtkDelete( pMiter ); |
| return RetValue; |
| } |
| if( RetValue == 1 ) |
| { |
| /*printf("Networks are equivalent after structural hashing."); */ |
| Abc_NtkDelete( pMiter ); |
| return RetValue; |
| } |
| |
| // convert the miter into a CNF |
| //if(mode == 0) |
| pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 ); |
| Abc_NtkDelete( pMiter ); |
| if ( pCnf == NULL ) |
| { |
| printf("Renoding for CNF has failed."); |
| return -1; |
| } |
| |
| // solve the CNF using the SAT solver |
| RetValue = Abc_NtkMiterSat( pCnf, (ABC_INT64_T)10000, (ABC_INT64_T)0, 0, NULL, NULL); |
| /*if ( RetValue == -1 ) |
| printf("Networks are undecided (SAT solver timed out)."); |
| else if ( RetValue == 0 ) |
| printf("Networks are NOT EQUIVALENT after SAT."); |
| else |
| printf("Networks are equivalent after SAT."); */ |
| if ( mismatch != NULL && pCnf->pModel ) |
| Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel, mismatch ); |
| |
| ABC_FREE( pCnf->pModel ); |
| Abc_NtkDelete( pCnf ); |
| |
| return RetValue; |
| } |
| |
| int checkEquivalence( Abc_Ntk_t * pNtk1, Vec_Int_t* matchedInputs1, Vec_Int_t * matchedOutputs1, |
| Abc_Ntk_t * pNtk2, Vec_Int_t* matchedInputs2, Vec_Int_t * matchedOutputs2) |
| { |
| Vec_Ptr_t * iMatchPairs, * oMatchPairs; |
| int i; |
| int result; |
| |
| iMatchPairs = Vec_PtrAlloc( Abc_NtkPiNum( pNtk1 ) * 2); |
| oMatchPairs = Vec_PtrAlloc( Abc_NtkPoNum( pNtk1 ) * 2); |
| |
| for(i = 0; i < Abc_NtkPiNum(pNtk1); i++) |
| { |
| Vec_PtrPush(iMatchPairs, Abc_NtkPi(pNtk2, Vec_IntEntry(matchedInputs2, i))); |
| Vec_PtrPush(iMatchPairs, Abc_NtkPi(pNtk1, Vec_IntEntry(matchedInputs1, i))); |
| } |
| |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk1); i++) |
| { |
| Vec_PtrPush(oMatchPairs, Abc_NtkPo(pNtk2, Vec_IntEntry(matchedOutputs2, i))); |
| Vec_PtrPush(oMatchPairs, Abc_NtkPo(pNtk1, Vec_IntEntry(matchedOutputs1, i))); |
| } |
| |
| result = Abc_NtkBmSat(pNtk1, pNtk2, iMatchPairs, oMatchPairs, NULL, 0); |
| |
| if( result ) |
| printf("*** Circuits are equivalent ***\n"); |
| else |
| printf("*** Circuits are NOT equivalent ***\n"); |
| |
| Vec_PtrFree( iMatchPairs ); |
| Vec_PtrFree( oMatchPairs ); |
| |
| return result; |
| } |
| |
| Abc_Ntk_t * computeCofactor(Abc_Ntk_t * pNtk, Vec_Ptr_t ** nodesInLevel, int * bitVector, Vec_Int_t * currInputs) |
| { |
| Abc_Ntk_t * subNtk; |
| Abc_Obj_t * pObj, * pObjNew; |
| int i, j, numOfLevels; |
| |
| numOfLevels = Abc_AigLevel( pNtk ); // number of levels excludes PI/POs |
| |
| // start a new network |
| subNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); |
| subNtk->pName = Extra_UtilStrsav("subNtk"); |
| |
| Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(subNtk); |
| |
| // clean the node copy fields and mark the nodes that need to be copied to the new network |
| Abc_NtkCleanCopy( pNtk ); |
| |
| if(bitVector != NULL) |
| { |
| for(i = 0; i < Abc_NtkPiNum(pNtk); i++) |
| if(bitVector[i]) |
| { |
| pObj = Abc_NtkPi(pNtk, i); |
| pObj->pCopy = (Abc_Obj_t *)(1); |
| } |
| } |
| |
| for(i = 0; i < Vec_IntSize(currInputs); i++) |
| { |
| pObj = Abc_NtkPi(pNtk, Vec_IntEntry(currInputs, i)); |
| pObjNew = Abc_NtkDupObj( subNtk, pObj, 1 ); |
| pObj->pCopy = pObjNew; |
| } |
| |
| |
| // i = 0 are the inputs and the inputs are not added to the 2d array ( nodesInLevel ) |
| for( i = 0; i <= numOfLevels; i++ ) |
| for( j = 0; j < Vec_PtrSize( nodesInLevel[i] ); j++) |
| { |
| pObj = (Abc_Obj_t *)Vec_PtrEntry( nodesInLevel[i], j ); |
| |
| if(Abc_ObjChild0Copy(pObj) == NULL && Abc_ObjChild1Copy(pObj) == NULL) |
| pObj->pCopy = NULL; |
| else if(Abc_ObjChild0Copy(pObj) == NULL && Abc_ObjChild1Copy(pObj) == (void*)(1)) |
| pObj->pCopy = NULL; |
| else if(Abc_ObjChild0Copy(pObj) == NULL && (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) ) |
| pObj->pCopy = NULL; |
| else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && Abc_ObjChild1Copy(pObj) == NULL) |
| pObj->pCopy = NULL; |
| else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && Abc_ObjChild1Copy(pObj) == (void*)(1)) |
| pObj->pCopy = (Abc_Obj_t *)(1); |
| else if(Abc_ObjChild0Copy(pObj) == (void*)(1) && (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) ) |
| pObj->pCopy = Abc_ObjChild1Copy(pObj); |
| else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) && Abc_ObjChild1Copy(pObj) == NULL ) |
| pObj->pCopy = NULL; |
| else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) && Abc_ObjChild1Copy(pObj) == (void*)(1) ) |
| pObj->pCopy = Abc_ObjChild0Copy(pObj); |
| else if( (Abc_ObjChild0Copy(pObj) != (NULL) && Abc_ObjChild0Copy(pObj) != (void*)(1)) && |
| (Abc_ObjChild1Copy(pObj) != (NULL) && Abc_ObjChild1Copy(pObj) != (void*)(1)) ) |
| pObj->pCopy = Abc_AigAnd( (Abc_Aig_t *)subNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); |
| } |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk); i++) |
| { |
| pObj = Abc_NtkPo(pNtk, i); |
| pObjNew = Abc_NtkDupObj( subNtk, pObj, 1 ); |
| |
| if( Abc_ObjChild0Copy(pObj) == NULL) |
| { |
| Abc_ObjAddFanin( pObjNew, Abc_AigConst1(subNtk)); |
| pObjNew->fCompl0 = 1; |
| } |
| else if( Abc_ObjChild0Copy(pObj) == (void*)(1) ) |
| { |
| Abc_ObjAddFanin( pObjNew, Abc_AigConst1(subNtk)); |
| pObjNew->fCompl0 = 0; |
| } |
| else |
| Abc_ObjAddFanin( pObjNew, Abc_ObjChild0Copy(pObj) ); |
| } |
| |
| return subNtk; |
| } |
| |
| FILE *matchFile; |
| |
| int matchNonSingletonOutputs(Abc_Ntk_t * pNtk1, Vec_Ptr_t ** nodesInLevel1, Vec_Int_t ** iMatch1, Vec_Int_t ** iDep1, Vec_Int_t * matchedInputs1, int * iGroup1, Vec_Int_t ** oMatch1, int * oGroup1, |
| Abc_Ntk_t * pNtk2, Vec_Ptr_t ** nodesInLevel2, Vec_Int_t ** iMatch2, Vec_Int_t ** iDep2, Vec_Int_t * matchedInputs2, int * iGroup2, Vec_Int_t ** oMatch2, int * oGroup2, |
| Vec_Int_t * matchedOutputs1, Vec_Int_t * matchedOutputs2, Vec_Int_t * oMatchedGroups, Vec_Int_t * iNonSingleton, |
| Abc_Ntk_t * subNtk1, Abc_Ntk_t * subNtk2, Vec_Ptr_t * oMatchPairs, |
| Vec_Int_t * oNonSingleton, int oI, int idx, int ii, int iidx) |
| { |
| static int MATCH_FOUND; |
| int i; |
| int j, temp; |
| Vec_Int_t * mismatch; |
| int * skipList; |
| static int counter = 0; |
| |
| MATCH_FOUND = FALSE; |
| |
| if( oI == Vec_IntSize( oNonSingleton ) ) |
| { |
| if( iNonSingleton != NULL) |
| if( match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1, |
| pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2, |
| matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, ii, iidx) ) |
| MATCH_FOUND = TRUE; |
| |
| if( iNonSingleton == NULL) |
| MATCH_FOUND = TRUE; |
| |
| return MATCH_FOUND; |
| } |
| |
| i = Vec_IntEntry(oNonSingleton, oI); |
| |
| mismatch = Vec_IntAlloc(10); |
| |
| skipList = ABC_ALLOC(int, Vec_IntSize(oMatch1[i])); |
| |
| for(j = 0; j < Vec_IntSize(oMatch1[i]); j++) |
| skipList[j] = FALSE; |
| |
| Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk1, Vec_IntEntry(oMatch1[i], idx)) ); |
| Vec_IntPush(matchedOutputs1, Vec_IntEntry(oMatch1[i], idx)); |
| |
| for(j = 0; j < Vec_IntSize( oMatch2[i] ) && MATCH_FOUND == FALSE; j++) |
| { |
| if( Vec_IntEntry(oMatch2[i], j) == -1 || skipList[j] == TRUE) |
| continue; |
| |
| Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk2, Vec_IntEntry(oMatch2[i], j))); |
| Vec_IntPush(matchedOutputs2, Vec_IntEntry(oMatch2[i], j)); |
| |
| counter++; |
| if( Abc_NtkBmSat( subNtk1, subNtk2, NULL, oMatchPairs, mismatch, 0) ) |
| { |
| /*fprintf(matchFile, "%s matched to %s\n", Abc_ObjName(Abc_NtkPo(pNtk1, Vec_IntEntry(oMatch1[i], idx))), |
| Abc_ObjName(Abc_NtkPo(pNtk2, Vec_IntEntry(oMatch2[i], j)))); */ |
| |
| temp = Vec_IntEntry(oMatch2[i], j); |
| Vec_IntWriteEntry(oMatch2[i], j, -1); |
| |
| if(idx != Vec_IntSize( oMatch1[i] ) - 1) |
| // call the same function with idx+1 |
| matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1, |
| pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2, |
| matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, |
| subNtk1, subNtk2, oMatchPairs, |
| oNonSingleton, oI, idx+1, ii, iidx); |
| else |
| // call the same function with idx = 0 and oI++ |
| matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1, |
| pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2, |
| matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, |
| subNtk1, subNtk2, oMatchPairs, |
| oNonSingleton, oI+1, 0, ii, iidx); |
| |
| Vec_IntWriteEntry(oMatch2[i], j, temp); |
| } |
| else |
| { |
| int * output1, * output2; |
| int k; |
| Abc_Obj_t * pObj; |
| int * pModel; |
| char * vPiValues; |
| |
| |
| vPiValues = ABC_ALLOC( char, Abc_NtkPiNum(subNtk1) + 1); |
| vPiValues[Abc_NtkPiNum(subNtk1)] = '\0'; |
| |
| for(k = 0; k < Abc_NtkPiNum(subNtk1); k++) |
| vPiValues[k] = '0'; |
| |
| for(k = 0; k < Vec_IntSize(mismatch); k += 2) |
| vPiValues[Vec_IntEntry(mismatch, k)] = Vec_IntEntry(mismatch, k+1); |
| |
| pModel = ABC_ALLOC( int, Abc_NtkCiNum(subNtk1) ); |
| |
| Abc_NtkForEachPi( subNtk1, pObj, k ) |
| pModel[k] = vPiValues[k] - '0'; |
| Abc_NtkForEachLatch( subNtk1, pObj, k ) |
| pModel[Abc_NtkPiNum(subNtk1)+k] = pObj->iData - 1; |
| |
| output1 = Abc_NtkVerifySimulatePattern( subNtk1, pModel ); |
| |
| Abc_NtkForEachLatch( subNtk2, pObj, k ) |
| pModel[Abc_NtkPiNum(subNtk2)+k] = pObj->iData - 1; |
| |
| output2 = Abc_NtkVerifySimulatePattern( subNtk2, pModel ); |
| |
| |
| for(k = 0; k < Vec_IntSize( oMatch1[i] ); k++) |
| if(output1[Vec_IntEntry(oMatch1[i], idx)] != output2[Vec_IntEntry(oMatch2[i], k)]) |
| { |
| skipList[k] = TRUE; |
| /*printf("Output is SKIPPED");*/ |
| } |
| |
| ABC_FREE( vPiValues ); |
| ABC_FREE( pModel ); |
| ABC_FREE( output1 ); |
| ABC_FREE( output2 ); |
| } |
| |
| if(MATCH_FOUND == FALSE ) |
| { |
| Vec_PtrPop(oMatchPairs); |
| Vec_IntPop(matchedOutputs2); |
| } |
| } |
| |
| if(MATCH_FOUND == FALSE ) |
| { |
| Vec_PtrPop(oMatchPairs); |
| Vec_IntPop(matchedOutputs1); |
| } |
| |
| if(MATCH_FOUND && counter != 0) |
| { |
| /*printf("Number of OUTPUT SAT instances = %d", counter);*/ |
| counter = 0; |
| } |
| |
| ABC_FREE( mismatch ); |
| ABC_FREE( skipList ); |
| |
| return MATCH_FOUND; |
| } |
| |
| int match1by1(Abc_Ntk_t * pNtk1, Vec_Ptr_t ** nodesInLevel1, Vec_Int_t ** iMatch1, Vec_Int_t ** iDep1, Vec_Int_t * matchedInputs1, int * iGroup1, Vec_Int_t ** oMatch1, int * oGroup1, |
| Abc_Ntk_t * pNtk2, Vec_Ptr_t ** nodesInLevel2, Vec_Int_t ** iMatch2, Vec_Int_t ** iDep2, Vec_Int_t * matchedInputs2, int * iGroup2, Vec_Int_t ** oMatch2, int * oGroup2, |
| Vec_Int_t * matchedOutputs1, Vec_Int_t * matchedOutputs2, Vec_Int_t * oMatchedGroups, Vec_Int_t * iNonSingleton, int ii, int idx) |
| { |
| static int MATCH_FOUND = FALSE; |
| Abc_Ntk_t * subNtk1, * subNtk2; |
| Vec_Int_t * oNonSingleton; |
| Vec_Ptr_t * oMatchPairs; |
| int * skipList; |
| int j, m; |
| int i; |
| static int counter = 0; |
| |
| MATCH_FOUND = FALSE; |
| |
| if( ii == Vec_IntSize(iNonSingleton) ) |
| { |
| MATCH_FOUND = TRUE; |
| return TRUE; |
| } |
| |
| i = Vec_IntEntry(iNonSingleton, ii); |
| |
| if( idx == Vec_IntSize(iMatch1[i]) ) |
| { |
| // call again with the next element in iNonSingleton |
| return match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1, |
| pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2, |
| matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, ii+1, 0); |
| |
| } |
| |
| oNonSingleton = Vec_IntAlloc(10); |
| oMatchPairs = Vec_PtrAlloc(100); |
| skipList = ABC_ALLOC(int, Vec_IntSize(iMatch1[i])); |
| |
| for(j = 0; j < Vec_IntSize(iMatch1[i]); j++) |
| skipList[j] = FALSE; |
| |
| Vec_IntPush(matchedInputs1, Vec_IntEntry(iMatch1[i], idx)); |
| idx++; |
| |
| if(idx == 1) |
| { |
| for(j = 0; j < Vec_IntSize(iDep1[Vec_IntEntryLast(iMatch1[i])]); j++) |
| { |
| if( Vec_IntSize(oMatch1[oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]]) == 1 ) |
| continue; |
| if( Vec_IntFind( oMatchedGroups, oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]) != -1) |
| continue; |
| |
| Vec_IntPushUnique(oNonSingleton, oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]); |
| Vec_IntPushUnique(oMatchedGroups, oGroup1[Vec_IntEntry(iDep1[Vec_IntEntryLast(iMatch1[i])], j)]); |
| } |
| } |
| |
| subNtk1 = computeCofactor(pNtk1, nodesInLevel1, NULL, matchedInputs1); |
| |
| for(j = idx-1; j < Vec_IntSize(iMatch2[i]) && MATCH_FOUND == FALSE; j++) |
| { |
| int tempJ; |
| Vec_Int_t * mismatch; |
| |
| if( skipList[j] ) |
| continue; |
| |
| mismatch = Vec_IntAlloc(10); |
| |
| Vec_IntPush(matchedInputs2, Vec_IntEntry(iMatch2[i], j)); |
| |
| subNtk2 = computeCofactor(pNtk2, nodesInLevel2, NULL, matchedInputs2); |
| |
| for(m = 0; m < Vec_IntSize(matchedOutputs1); m++) |
| { |
| Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk1, Vec_IntEntry(matchedOutputs1, m))); |
| Vec_PtrPush(oMatchPairs, Abc_NtkPo(subNtk2, Vec_IntEntry(matchedOutputs2, m))); |
| } |
| |
| counter++; |
| |
| if( Abc_NtkBmSat( subNtk2, subNtk1, NULL, oMatchPairs, mismatch, 0) ) |
| { |
| if(idx-1 != j) |
| { |
| tempJ = Vec_IntEntry(iMatch2[i], idx-1); |
| Vec_IntWriteEntry(iMatch2[i], idx-1, Vec_IntEntry(iMatch2[i], j)); |
| Vec_IntWriteEntry(iMatch2[i], j, tempJ); |
| } |
| |
| /*fprintf(matchFile, "%s matched to %s\n", Abc_ObjName(Abc_NtkPi(pNtk1, Vec_IntEntry(iMatch1[i], idx-1))), |
| Abc_ObjName(Abc_NtkPi(pNtk2, Vec_IntEntry(iMatch2[i], j))));*/ |
| |
| // we look for a match for outputs in oNonSingleton |
| matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1, |
| pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2, |
| matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, |
| subNtk1, subNtk2, oMatchPairs, oNonSingleton, 0, 0, ii, idx); |
| |
| |
| if(idx-1 != j) |
| { |
| tempJ = Vec_IntEntry(iMatch2[i], idx-1); |
| Vec_IntWriteEntry(iMatch2[i], idx-1, Vec_IntEntry(iMatch2[i], j)); |
| Vec_IntWriteEntry(iMatch2[i], j, tempJ); |
| } |
| } |
| else |
| { |
| Abc_Ntk_t * FpNtk1, * FpNtk2; |
| int * bitVector1, * bitVector2; |
| Vec_Int_t * currInputs1, * currInputs2; |
| Vec_Ptr_t * vSupp; |
| Abc_Obj_t * pObj; |
| int suppNum1 = 0; |
| int * suppNum2; |
| |
| bitVector1 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk1) ); |
| bitVector2 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk2) ); |
| |
| currInputs1 = Vec_IntAlloc(10); |
| currInputs2 = Vec_IntAlloc(10); |
| |
| suppNum2 = ABC_ALLOC(int, Vec_IntSize(iMatch2[i])-idx+1); |
| |
| for(m = 0; m < Abc_NtkPiNum(pNtk1); m++) |
| { |
| bitVector1[m] = 0; |
| bitVector2[m] = 0; |
| } |
| |
| for(m = 0; m < Vec_IntSize(iMatch2[i])-idx+1; m++) |
| suppNum2[m]= 0; |
| |
| // First of all set the value of the inputs that are already matched and are in mismatch |
| for(m = 0; m < Vec_IntSize(mismatch); m += 2) |
| { |
| int n = Vec_IntEntry(mismatch, m); |
| |
| bitVector1[Vec_IntEntry(matchedInputs1, n)] = Vec_IntEntry(mismatch, m+1); |
| bitVector2[Vec_IntEntry(matchedInputs2, n)] = Vec_IntEntry(mismatch, m+1); |
| |
| } |
| |
| for(m = idx-1; m < Vec_IntSize(iMatch1[i]); m++) |
| { |
| Vec_IntPush(currInputs1, Vec_IntEntry(iMatch1[i], m)); |
| Vec_IntPush(currInputs2, Vec_IntEntry(iMatch2[i], m)); |
| } |
| |
| // Then add all the inputs that are not yet matched to the currInputs |
| for(m = 0; m < Abc_NtkPiNum(pNtk1); m++) |
| { |
| if(Vec_IntFind( matchedInputs1, m ) == -1) |
| Vec_IntPushUnique(currInputs1, m); |
| |
| if(Vec_IntFind( matchedInputs2, m ) == -1) |
| Vec_IntPushUnique(currInputs2, m); |
| } |
| |
| FpNtk1 = computeCofactor(pNtk1, nodesInLevel1, bitVector1, currInputs1); |
| FpNtk2 = computeCofactor(pNtk2, nodesInLevel2, bitVector2, currInputs2); |
| |
| Abc_NtkForEachPo( FpNtk1, pObj, m ) |
| { |
| int n; |
| vSupp = Abc_NtkNodeSupport( FpNtk1, &pObj, 1 ); |
| |
| for(n = 0; n < vSupp->nSize; n++) |
| if( Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n]) == 1 ) |
| suppNum1 += Vec_IntFind( matchedOutputs1, m) + 1; |
| |
| Vec_PtrFree( vSupp ); |
| } |
| |
| Abc_NtkForEachPo( FpNtk2, pObj, m ) |
| { |
| int n; |
| vSupp = Abc_NtkNodeSupport( FpNtk2, &pObj, 1 ); |
| |
| for(n = 0; n < vSupp->nSize; n++) |
| if( (int)Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1 < (Vec_IntSize(iMatch2[i]))-idx+1 && |
| (int)Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1 >= 0) |
| suppNum2[Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1] += Vec_IntFind( matchedOutputs2, m) + 1; |
| |
| Vec_PtrFree( vSupp ); |
| } |
| |
| /*if(suppNum1 != 0) |
| printf("Ntk1 is trigged"); |
| |
| if(suppNum2[0] != 0) |
| printf("Ntk2 is trigged");*/ |
| |
| for(m = 0; m < Vec_IntSize(iMatch2[i])-idx+1; m++) |
| if(suppNum2[m] != suppNum1) |
| { |
| skipList[m+idx-1] = TRUE; |
| /*printf("input is skipped");*/ |
| } |
| |
| Abc_NtkDelete( FpNtk1 ); |
| Abc_NtkDelete( FpNtk2 ); |
| ABC_FREE( bitVector1 ); |
| ABC_FREE( bitVector2 ); |
| Vec_IntFree( currInputs1 ); |
| Vec_IntFree( currInputs2 ); |
| ABC_FREE( suppNum2 ); |
| } |
| |
| Vec_PtrClear(oMatchPairs); |
| Abc_NtkDelete( subNtk2 ); |
| Vec_IntFree(mismatch); |
| |
| //Vec_IntWriteEntry(iMatch2[i], j, tempJ); |
| |
| if( MATCH_FOUND == FALSE ) |
| Vec_IntPop(matchedInputs2); |
| } |
| |
| if( MATCH_FOUND == FALSE ) |
| { |
| Vec_IntPop(matchedInputs1); |
| |
| if(idx == 1) |
| { |
| for(m = 0; m < Vec_IntSize(oNonSingleton); m++) |
| Vec_IntPop( oMatchedGroups ); |
| } |
| } |
| |
| Vec_IntFree( oNonSingleton ); |
| Vec_PtrFree( oMatchPairs ); |
| ABC_FREE( skipList ); |
| Abc_NtkDelete( subNtk1 ); |
| |
| if(MATCH_FOUND && counter != 0) |
| { |
| /*printf("Number of INPUT SAT instances = %d\n", counter);*/ |
| |
| counter = 0; |
| } |
| |
| return MATCH_FOUND; |
| } |
| |
| float refineBySAT(Abc_Ntk_t * pNtk1, Vec_Int_t ** iMatch1, int * iGroup1, Vec_Int_t ** iDep1, int* iLastItem1, Vec_Int_t ** oMatch1, int * oGroup1, Vec_Int_t ** oDep1, int* oLastItem1, int * observability1, |
| Abc_Ntk_t * pNtk2, Vec_Int_t ** iMatch2, int * iGroup2, Vec_Int_t ** iDep2, int* iLastItem2, Vec_Int_t ** oMatch2, int * oGroup2, Vec_Int_t ** oDep2, int* oLastItem2, int * observability2) |
| { |
| int i, j; |
| Abc_Obj_t * pObj; |
| Vec_Int_t * iNonSingleton; |
| Vec_Int_t * matchedInputs1, * matchedInputs2; |
| Vec_Int_t * matchedOutputs1, * matchedOutputs2; |
| Vec_Ptr_t ** nodesInLevel1, ** nodesInLevel2; |
| Vec_Int_t * oMatchedGroups; |
| FILE *result; |
| int matchFound; |
| abctime clk = Abc_Clock(); |
| float satTime = 0.0; |
| |
| /*matchFile = fopen("satmatch.txt", "w");*/ |
| |
| iNonSingleton = Vec_IntAlloc(10); |
| |
| matchedInputs1 = Vec_IntAlloc( Abc_NtkPiNum(pNtk1) ); |
| matchedInputs2 = Vec_IntAlloc( Abc_NtkPiNum(pNtk2) ); |
| |
| matchedOutputs1 = Vec_IntAlloc( Abc_NtkPoNum(pNtk1) ); |
| matchedOutputs2 = Vec_IntAlloc( Abc_NtkPoNum(pNtk2) ); |
| |
| nodesInLevel1 = ABC_ALLOC( Vec_Ptr_t *, Abc_AigLevel( pNtk1 ) + 1); // why numOfLevels+1? because the inputs are in level 0 |
| for(i = 0; i <= Abc_AigLevel( pNtk1 ); i++) |
| nodesInLevel1[i] = Vec_PtrAlloc( 20 ); |
| |
| // bucket sort the objects based on their levels |
| Abc_AigForEachAnd( pNtk1, pObj, i ) |
| Vec_PtrPush(nodesInLevel1[Abc_ObjLevel(pObj)], pObj); |
| |
| nodesInLevel2 = ABC_ALLOC( Vec_Ptr_t *, Abc_AigLevel( pNtk2 ) + 1); // why numOfLevels+1? because the inputs are in level 0 |
| for(i = 0; i <= Abc_AigLevel( pNtk2 ); i++) |
| nodesInLevel2[i] = Vec_PtrAlloc( 20 ); |
| |
| // bucket sort the objects based on their levels |
| Abc_AigForEachAnd( pNtk2, pObj, i ) |
| Vec_PtrPush(nodesInLevel2[Abc_ObjLevel(pObj)], pObj); |
| |
| oMatchedGroups = Vec_IntAlloc( 10 ); |
| |
| for(i = 0; i < *iLastItem1; i++) |
| { |
| if(Vec_IntSize(iMatch1[i]) == 1) |
| { |
| Vec_IntPush(matchedInputs1, Vec_IntEntryLast(iMatch1[i])); |
| Vec_IntPush(matchedInputs2, Vec_IntEntryLast(iMatch2[i])); |
| } |
| else |
| Vec_IntPush(iNonSingleton, i); |
| } |
| |
| for(i = 0; i < *oLastItem1; i++) |
| { |
| if(Vec_IntSize(oMatch1[i]) == 1) |
| { |
| Vec_IntPush(matchedOutputs1, Vec_IntEntryLast(oMatch1[i])); |
| Vec_IntPush(matchedOutputs2, Vec_IntEntryLast(oMatch2[i])); |
| } |
| } |
| |
| for(i = 0; i < Vec_IntSize(iNonSingleton) - 1; i++) |
| { |
| for(j = i + 1; j < Vec_IntSize(iNonSingleton); j++) |
| if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] > |
| observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] ) |
| { |
| int temp = Vec_IntEntry(iNonSingleton, i); |
| Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) ); |
| Vec_IntWriteEntry( iNonSingleton, j, temp ); |
| } |
| else if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] == |
| observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] ) |
| { |
| if( Vec_IntSize(iMatch2[Vec_IntEntry(iNonSingleton, j)]) < Vec_IntSize(iMatch2[Vec_IntEntry(iNonSingleton, i)]) ) |
| { |
| int temp = Vec_IntEntry(iNonSingleton, i); |
| Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) ); |
| Vec_IntWriteEntry( iNonSingleton, j, temp ); |
| } |
| } |
| } |
| |
| /*for(i = 0; i < Vec_IntSize(iNonSingleton) - 1; i++) |
| { |
| for(j = i + 1; j < Vec_IntSize(iNonSingleton); j++) |
| if( Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, j)])]]) > |
| Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, i)])]]) ) |
| { |
| int temp = Vec_IntEntry(iNonSingleton, i); |
| Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) ); |
| Vec_IntWriteEntry( iNonSingleton, j, temp ); |
| } |
| else if( Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, j)])]]) == |
| Vec_IntSize(oDep2[oGroup2[Vec_IntEntryLast(iMatch2[Vec_IntEntry(iNonSingleton, i)])]]) ) |
| { |
| if( observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, j)], 0)] > |
| observability2[Vec_IntEntry(iMatch2[Vec_IntEntry(iNonSingleton, i)], 0)] ) |
| { |
| int temp = Vec_IntEntry(iNonSingleton, i); |
| Vec_IntWriteEntry( iNonSingleton, i, Vec_IntEntry(iNonSingleton, j) ); |
| Vec_IntWriteEntry( iNonSingleton, j, temp ); |
| } |
| } |
| }*/ |
| |
| matchFound = match1by1(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1, |
| pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup2, oMatch2, oGroup2, |
| matchedOutputs1, matchedOutputs2, oMatchedGroups, iNonSingleton, 0, 0); |
| |
| if( matchFound && Vec_IntSize(matchedOutputs1) != Abc_NtkPoNum(pNtk1) ) |
| { |
| Vec_Int_t * oNonSingleton; |
| Vec_Ptr_t * oMatchPairs; |
| Abc_Ntk_t * subNtk1, * subNtk2; |
| |
| oNonSingleton = Vec_IntAlloc( 10 ); |
| |
| oMatchPairs = Vec_PtrAlloc(Abc_NtkPoNum(pNtk1) * 2); |
| |
| for(i = 0; i < *oLastItem1; i++) |
| if( Vec_IntSize(oMatch1[i]) > 1 && Vec_IntFind( oMatchedGroups, i) == -1 ) |
| Vec_IntPush(oNonSingleton, i); |
| |
| subNtk1 = computeCofactor(pNtk1, nodesInLevel1, NULL, matchedInputs1); |
| subNtk2 = computeCofactor(pNtk2, nodesInLevel2, NULL, matchedInputs2); |
| |
| matchFound = matchNonSingletonOutputs(pNtk1, nodesInLevel1, iMatch1, iDep1, matchedInputs1, iGroup1, oMatch1, oGroup1, |
| pNtk2, nodesInLevel2, iMatch2, iDep2, matchedInputs2, iGroup1, oMatch2, oGroup2, |
| matchedOutputs1, matchedOutputs2, oMatchedGroups, NULL, |
| subNtk1, subNtk2, oMatchPairs, oNonSingleton, 0, 0, 0, 0); |
| |
| Vec_IntFree( oNonSingleton ); |
| Vec_PtrFree( oMatchPairs ); |
| |
| Abc_NtkDelete(subNtk1); |
| Abc_NtkDelete(subNtk2); |
| } |
| |
| satTime = (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC); |
| |
| if( matchFound ) |
| { |
| checkEquivalence( pNtk1, matchedInputs1, matchedOutputs1, pNtk2, matchedInputs2, matchedOutputs2); |
| |
| result = fopen("IOmatch.txt", "w"); |
| |
| fprintf(result, "I/O = %d / %d \n\n", Abc_NtkPiNum(pNtk1), Abc_NtkPoNum(pNtk1)); |
| |
| for(i = 0; i < Vec_IntSize(matchedInputs1) ; i++) |
| fprintf(result, "{%s}\t{%s}\n", Abc_ObjName(Abc_NtkPi(pNtk1, Vec_IntEntry(matchedInputs1, i))), Abc_ObjName(Abc_NtkPi(pNtk2, Vec_IntEntry(matchedInputs2, i))) ); |
| |
| fprintf(result, "\n-----------------------------------------\n"); |
| |
| for(i = 0; i < Vec_IntSize(matchedOutputs1) ; i++) |
| fprintf(result, "{%s}\t{%s}\n", Abc_ObjName(Abc_NtkPo(pNtk1, Vec_IntEntry(matchedOutputs1, i))), Abc_ObjName(Abc_NtkPo(pNtk2, Vec_IntEntry(matchedOutputs2, i))) ); |
| |
| fclose( result ); |
| } |
| |
| Vec_IntFree( matchedInputs1 ); |
| Vec_IntFree( matchedInputs2 ); |
| Vec_IntFree( matchedOutputs1 ); |
| Vec_IntFree( matchedOutputs2 ); |
| Vec_IntFree( iNonSingleton ); |
| Vec_IntFree( oMatchedGroups ); |
| |
| for(i = 0; i <= Abc_AigLevel( pNtk1 ); i++) |
| Vec_PtrFree( nodesInLevel1[i] ); |
| for(i = 0; i <= Abc_AigLevel( pNtk2 ); i++) |
| Vec_PtrFree( nodesInLevel2[i] ); |
| |
| |
| ABC_FREE( nodesInLevel1 ); |
| ABC_FREE( nodesInLevel2 ); |
| /*fclose(matchFile);*/ |
| |
| return satTime; |
| } |
| |
| int checkListConsistency(Vec_Int_t ** iMatch1, Vec_Int_t ** oMatch1, Vec_Int_t ** iMatch2, Vec_Int_t ** oMatch2, int iLastItem1, int oLastItem1, int iLastItem2, int oLastItem2) |
| { |
| //int i; |
| |
| if(iLastItem1 != iLastItem2 || oLastItem1 != oLastItem2) |
| return FALSE; |
| |
| /*for(i = 0; i < iLastItem1; i++) { |
| if(Vec_IntSize(iMatch1[i]) != Vec_IntSize(iMatch2[i])) |
| return FALSE; |
| } |
| |
| for(i = 0; i < oLastItem1; i++) { |
| if(Vec_IntSize(oMatch1[i]) != Vec_IntSize(oMatch2[i])) |
| return FALSE; |
| }*/ |
| |
| return TRUE; |
| } |
| |
| |
| void bmGateWay( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int p_equivalence ) |
| { |
| Vec_Int_t ** iDep1, ** oDep1; |
| Vec_Int_t ** iDep2, ** oDep2; |
| Vec_Int_t ** iMatch1, ** oMatch1; |
| Vec_Int_t ** iMatch2, ** oMatch2; |
| int * iGroup1, * oGroup1; |
| int * iGroup2, * oGroup2; |
| int iLastItem1, oLastItem1; |
| int iLastItem2, oLastItem2; |
| int i, j; |
| |
| char * vPiValues1, * vPiValues2; |
| int * observability1, * observability2; |
| abctime clk = Abc_Clock(); |
| float initTime; |
| float simulTime; |
| float satTime; |
| Vec_Ptr_t ** topOrder1 = NULL, ** topOrder2 = NULL; |
| |
| extern void getDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep); |
| extern void initMatchList(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** oDep, Vec_Int_t** iMatch, int* iLastItem, Vec_Int_t** oMatch, int* oLastItem, int* iGroup, int* oGroup, int p_equivalence); |
| extern void iSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, int* oGroup); |
| extern void oSortDependencies(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, int* iGroup); |
| extern int iSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** iDep, Vec_Int_t** iMatch, int* iGroup, int* iLastItem, int* oGroup); |
| extern int oSplitByDep(Abc_Ntk_t *pNtk, Vec_Int_t** oDep, Vec_Int_t** oMatch, int* oGroup, int* oLastItem, int* iGroup); |
| extern Vec_Ptr_t ** findTopologicalOrder(Abc_Ntk_t * pNtk); |
| extern int refineIOBySimulation(Abc_Ntk_t *pNtk, Vec_Int_t** iMatch, int* iLastItem, int * iGroup, Vec_Int_t** iDep, Vec_Int_t** oMatch, int* oLastItem, int * oGroup, Vec_Int_t** oDep, char * vPiValues, int * observability, Vec_Ptr_t ** topOrder); |
| extern float refineBySAT(Abc_Ntk_t * pNtk1, Vec_Int_t ** iMatch1, int * iGroup1, Vec_Int_t ** iDep1, int* iLastItem1, Vec_Int_t ** oMatch1, int * oGroup1, Vec_Int_t ** oDep1, int* oLastItem1, int * observability1, |
| Abc_Ntk_t * pNtk2, Vec_Int_t ** iMatch2, int * iGroup2, Vec_Int_t ** iDep2, int* iLastItem2, Vec_Int_t ** oMatch2, int * oGroup2, Vec_Int_t ** oDep2, int* oLastItem2, int * observability2); |
| int checkListConsistency(Vec_Int_t ** iMatch1, Vec_Int_t ** oMatch1, Vec_Int_t ** iMatch2, Vec_Int_t ** oMatch2, int iLastItem1, int oLastItem1, int iLastItem2, int oLastItem2); |
| |
| iDep1 = ABC_ALLOC( Vec_Int_t*, (unsigned)Abc_NtkPiNum(pNtk1) ); |
| oDep1 = ABC_ALLOC( Vec_Int_t*, (unsigned)Abc_NtkPoNum(pNtk1) ); |
| |
| iDep2 = ABC_ALLOC( Vec_Int_t*, (unsigned)Abc_NtkPiNum(pNtk2) ); |
| oDep2 = ABC_ALLOC( Vec_Int_t*, (unsigned)Abc_NtkPoNum(pNtk2) ); |
| |
| iMatch1 = ABC_ALLOC( Vec_Int_t*, (unsigned)Abc_NtkPiNum(pNtk1) ); |
| oMatch1 = ABC_ALLOC( Vec_Int_t*, (unsigned)Abc_NtkPoNum(pNtk1) ); |
| |
| iMatch2 = ABC_ALLOC( Vec_Int_t*, (unsigned)Abc_NtkPiNum(pNtk2) ); |
| oMatch2 = ABC_ALLOC( Vec_Int_t*, (unsigned)Abc_NtkPoNum(pNtk2) ); |
| |
| iGroup1 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk1) ); |
| oGroup1 = ABC_ALLOC( int, Abc_NtkPoNum(pNtk1) ); |
| |
| iGroup2 = ABC_ALLOC( int, Abc_NtkPiNum(pNtk2) ); |
| oGroup2 = ABC_ALLOC( int, Abc_NtkPoNum(pNtk2) ); |
| |
| vPiValues1 = ABC_ALLOC( char, Abc_NtkPiNum(pNtk1) + 1); |
| vPiValues1[Abc_NtkPiNum(pNtk1)] = '\0'; |
| |
| vPiValues2 = ABC_ALLOC( char, Abc_NtkPiNum(pNtk2) + 1); |
| vPiValues2[Abc_NtkPiNum(pNtk2)] = '\0'; |
| |
| observability1 = ABC_ALLOC(int, (unsigned)Abc_NtkPiNum(pNtk1)); |
| observability2 = ABC_ALLOC(int, (unsigned)Abc_NtkPiNum(pNtk2)); |
| |
| for(i = 0; i < Abc_NtkPiNum(pNtk1); i++) |
| { |
| iDep1[i] = Vec_IntAlloc( 1 ); |
| iMatch1[i] = Vec_IntAlloc( 1 ); |
| |
| iDep2[i] = Vec_IntAlloc( 1 ); |
| iMatch2[i] = Vec_IntAlloc( 1 ); |
| |
| vPiValues1[i] = '0'; |
| vPiValues2[i] = '0'; |
| |
| observability1[i] = 0; |
| observability2[i] = 0; |
| } |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk1); i++) |
| { |
| oDep1[i] = Vec_IntAlloc( 1 ); |
| oMatch1[i] = Vec_IntAlloc( 1 ); |
| |
| oDep2[i] = Vec_IntAlloc( 1 ); |
| oMatch2[i] = Vec_IntAlloc( 1 ); |
| } |
| |
| /************* Strashing ************/ |
| pNtk1 = Abc_NtkStrash( pNtk1, 0, 0, 0 ); |
| pNtk2 = Abc_NtkStrash( pNtk2, 0, 0, 0 ); |
| printf("Network strashing is done!\n"); |
| /************************************/ |
| |
| /******* Getting Dependencies *******/ |
| getDependencies(pNtk1, iDep1, oDep1); |
| getDependencies(pNtk2, iDep2, oDep2); |
| printf("Getting dependencies is done!\n"); |
| /************************************/ |
| |
| /***** Intializing match lists ******/ |
| initMatchList(pNtk1, iDep1, oDep1, iMatch1, &iLastItem1, oMatch1, &oLastItem1, iGroup1, oGroup1, p_equivalence); |
| initMatchList(pNtk2, iDep2, oDep2, iMatch2, &iLastItem2, oMatch2, &oLastItem2, iGroup2, oGroup2, p_equivalence); |
| printf("Initializing match lists is done!\n"); |
| /************************************/ |
| |
| if( !checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2) ) |
| { |
| fprintf( stdout, "I/O dependencies of two circuits are different.\n"); |
| goto freeAndExit; |
| } |
| |
| printf("Refining IOs by dependencies ..."); |
| // split match lists further by checking dependencies |
| do |
| { |
| int iNumOfItemsAdded = 1, oNumOfItemsAdded = 1; |
| |
| do |
| { |
| if( oNumOfItemsAdded ) |
| { |
| iSortDependencies(pNtk1, iDep1, oGroup1); |
| iSortDependencies(pNtk2, iDep2, oGroup2); |
| } |
| |
| if( iNumOfItemsAdded ) |
| { |
| oSortDependencies(pNtk1, oDep1, iGroup1); |
| oSortDependencies(pNtk2, oDep2, iGroup2); |
| } |
| |
| if( iLastItem1 < Abc_NtkPiNum(pNtk1) ) |
| { |
| iSplitByDep(pNtk1, iDep1, iMatch1, iGroup1, &iLastItem1, oGroup1); |
| if( oLastItem1 < Abc_NtkPoNum(pNtk1) ) |
| oSplitByDep(pNtk1, oDep1, oMatch1, oGroup1, &oLastItem1, iGroup1); |
| } |
| |
| if( iLastItem2 < Abc_NtkPiNum(pNtk2) ) |
| iNumOfItemsAdded = iSplitByDep(pNtk2, iDep2, iMatch2, iGroup2, &iLastItem2, oGroup2); |
| else |
| iNumOfItemsAdded = 0; |
| |
| if( oLastItem2 < Abc_NtkPoNum(pNtk2) ) |
| oNumOfItemsAdded = oSplitByDep(pNtk2, oDep2, oMatch2, oGroup2, &oLastItem2, iGroup2); |
| else |
| oNumOfItemsAdded = 0; |
| |
| if(!checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2)) |
| { |
| fprintf( stdout, "I/O dependencies of two circuits are different.\n"); |
| goto freeAndExit; |
| } |
| }while(iNumOfItemsAdded != 0 || oNumOfItemsAdded != 0); |
| |
| }while(0); |
| |
| printf(" done!\n"); |
| |
| initTime = ((float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC)); |
| clk = Abc_Clock(); |
| |
| topOrder1 = findTopologicalOrder(pNtk1); |
| topOrder2 = findTopologicalOrder(pNtk2); |
| |
| printf("Refining IOs by simulation ..."); |
| |
| do |
| { |
| int counter = 0; |
| int ioSuccess1, ioSuccess2; |
| |
| do |
| { |
| for(i = 0; i < iLastItem1; i++) |
| { |
| int temp = (int)(SIM_RANDOM_UNSIGNED % 2); |
| |
| if(Vec_IntSize(iMatch1[i]) != Vec_IntSize(iMatch2[i])) |
| { |
| fprintf( stdout, "Input refinement by simulation finds two circuits different.\n"); |
| goto freeAndExit; |
| } |
| |
| for(j = 0; j < Vec_IntSize(iMatch1[i]); j++) |
| { |
| vPiValues1[Vec_IntEntry(iMatch1[i], j)] = temp + '0'; |
| vPiValues2[Vec_IntEntry(iMatch2[i], j)] = temp + '0'; |
| } |
| } |
| |
| ioSuccess1 = refineIOBySimulation(pNtk1, iMatch1, &iLastItem1, iGroup1, iDep1, oMatch1, &oLastItem1, oGroup1, oDep1, vPiValues1, observability1, topOrder1); |
| ioSuccess2 = refineIOBySimulation(pNtk2, iMatch2, &iLastItem2, iGroup2, iDep2, oMatch2, &oLastItem2, oGroup2, oDep2, vPiValues2, observability2, topOrder2); |
| |
| if(ioSuccess1 && ioSuccess2) |
| counter = 0; |
| else |
| counter++; |
| |
| if(ioSuccess1 != ioSuccess2 || |
| !checkListConsistency(iMatch1, oMatch1, iMatch2, oMatch2, iLastItem1, oLastItem1, iLastItem2, oLastItem2)) |
| { |
| fprintf( stdout, "Input refinement by simulation finds two circuits different.\n"); |
| goto freeAndExit; |
| } |
| }while(counter <= 200); |
| |
| }while(0); |
| |
| printf(" done!\n"); |
| |
| simulTime = (float)(Abc_Clock() - clk)/(float)(CLOCKS_PER_SEC); |
| printf("SAT-based search started ...\n"); |
| |
| satTime = refineBySAT(pNtk1, iMatch1, iGroup1, iDep1, &iLastItem1, oMatch1, oGroup1, oDep1, &oLastItem1, observability1, |
| pNtk2, iMatch2, iGroup2, iDep2, &iLastItem2, oMatch2, oGroup2, oDep2, &oLastItem2, observability2); |
| |
| printf( "Init Time = %4.2f\n", initTime ); |
| printf( "Simulation Time = %4.2f\n", simulTime ); |
| printf( "SAT Time = %4.2f\n", satTime ); |
| printf( "Overall Time = %4.2f\n", initTime + simulTime + satTime ); |
| |
| freeAndExit: |
| |
| for(i = 0; i < iLastItem1 ; i++) |
| { |
| |
| Vec_IntFree( iMatch1[i] ); |
| Vec_IntFree( iMatch2[i] ); |
| } |
| |
| for(i = 0; i < oLastItem1 ; i++) |
| { |
| |
| Vec_IntFree( oMatch1[i] ); |
| Vec_IntFree( oMatch2[i] ); |
| } |
| |
| for(i = 0; i < Abc_NtkPiNum(pNtk1); i++) |
| { |
| Vec_IntFree( iDep1[i] ); |
| Vec_IntFree( iDep2[i] ); |
| if(topOrder1 != NULL) { |
| Vec_PtrFree( topOrder1[i] ); |
| Vec_PtrFree( topOrder2[i] ); |
| } |
| } |
| |
| for(i = 0; i < Abc_NtkPoNum(pNtk1); i++) |
| { |
| Vec_IntFree( oDep1[i] ); |
| Vec_IntFree( oDep2[i] ); |
| } |
| |
| ABC_FREE( iMatch1 ); |
| ABC_FREE( iMatch2 ); |
| ABC_FREE( oMatch1 ); |
| ABC_FREE( oMatch2 ); |
| ABC_FREE( iDep1 ); |
| ABC_FREE( iDep2 ); |
| ABC_FREE( oDep1 ); |
| ABC_FREE( oDep2 ); |
| ABC_FREE( iGroup1 ); |
| ABC_FREE( iGroup2 ); |
| ABC_FREE( oGroup1 ); |
| ABC_FREE( oGroup2 ); |
| ABC_FREE( vPiValues1 ); |
| ABC_FREE( vPiValues2 ); |
| ABC_FREE( observability1 ); |
| ABC_FREE( observability2 ); |
| if(topOrder1 != NULL) { |
| ABC_FREE( topOrder1 ); |
| ABC_FREE( topOrder2 ); |
| } |
| }ABC_NAMESPACE_IMPL_END |
| |
