/**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 "src/base/abc/abc.h" #include "src/opt/sim/sim.h" #include "src/sat/bsat/satSolver.h" #include "src/misc/extra/extraBdd.h" ABC_NAMESPACE_IMPL_START 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; clock_t 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 = 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", clock() - clk ); // simplify the problem clk = 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", clock() - clk ); if ( status == 0 ) { sat_solver_delete( pSat ); // printf( "The problem is UNSATISFIABLE after simplification.\n" ); return 1; } // solve the miter clk = 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", 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; // 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( Abc_ObjId((Abc_Obj_t *)vSupp->pArray[n])-1 < (unsigned)(Vec_IntSize(iMatch2[i]))-idx+1 && 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; clock_t clk = 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)(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; clock_t clk = 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); if( oLastItem2 < Abc_NtkPoNum(pNtk2) ) oNumOfItemsAdded = oSplitByDep(pNtk2, oDep2, oMatch2, oGroup2, &oLastItem2, iGroup2); else oNumOfItemsAdded = 0; } else iNumOfItemsAdded = 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)(clock() - clk)/(float)(CLOCKS_PER_SEC)); clk = 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)(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