| /**CFile**************************************************************** |
| |
| FileName [simSymStr.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Network and node package.] |
| |
| Synopsis [Structural detection of symmetries.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: simSymStr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "base/abc/abc.h" |
| #include "sim.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #define SIM_READ_SYMMS(pNode) ((Vec_Int_t *)pNode->pCopy) |
| #define SIM_SET_SYMMS(pNode,vVect) (pNode->pCopy = (Abc_Obj_t *)(vVect)) |
| |
| static void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap ); |
| static void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); |
| static void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther ); |
| static void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap ); |
| static void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap ); |
| static int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap ); |
| static int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap ); |
| static void Sim_SymmsPrint( Vec_Int_t * vSymms ); |
| static void Sim_SymmsTrans( Vec_Int_t * vSymms ); |
| static void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport ); |
| static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes symmetries for a single output function.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * vSuppFun ) |
| { |
| Vec_Ptr_t * vNodes; |
| Abc_Obj_t * pTemp; |
| int * pMap, i; |
| |
| assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) ); |
| |
| // get the structural support |
| pNtk->vSupps = Sim_ComputeStrSupp( pNtk ); |
| // set elementary info for the CIs |
| Abc_NtkForEachCi( pNtk, pTemp, i ) |
| SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) ); |
| // create the map of CI ids into their numbers |
| pMap = Sim_SymmsCreateMap( pNtk ); |
| // collect the nodes in the TFI cone of this output |
| vNodes = Abc_NtkDfs( pNtk, 0 ); |
| Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i ) |
| { |
| // if ( Abc_NodeIsConst(pTemp) ) |
| // continue; |
| Sim_SymmsStructComputeOne( pNtk, pTemp, pMap ); |
| } |
| // collect the results for the COs; |
| Abc_NtkForEachCo( pNtk, pTemp, i ) |
| { |
| //printf( "Output %d:\n", i ); |
| pTemp = Abc_ObjFanin0(pTemp); |
| if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) ) |
| continue; |
| Sim_SymmsTransferToMatrix( (Extra_BitMat_t *)Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), (unsigned *)Vec_PtrEntry(vSuppFun, i) ); |
| } |
| // clean the intermediate results |
| Sim_UtilInfoFree( pNtk->vSupps ); |
| pNtk->vSupps = NULL; |
| Abc_NtkForEachCi( pNtk, pTemp, i ) |
| Vec_IntFree( SIM_READ_SYMMS(pTemp) ); |
| Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i ) |
| // if ( !Abc_NodeIsConst(pTemp) ) |
| Vec_IntFree( SIM_READ_SYMMS(pTemp) ); |
| Vec_PtrFree( vNodes ); |
| ABC_FREE( pMap ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Recursively computes symmetries. ] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap ) |
| { |
| Vec_Ptr_t * vNodes, * vNodesPi0, * vNodesPi1, * vNodesOther; |
| Vec_Int_t * vSymms; |
| Abc_Obj_t * pTemp; |
| int i; |
| |
| // allocate the temporary arrays |
| vNodes = Vec_PtrAlloc( 10 ); |
| vNodesPi0 = Vec_PtrAlloc( 10 ); |
| vNodesPi1 = Vec_PtrAlloc( 10 ); |
| vNodesOther = Vec_PtrAlloc( 10 ); |
| |
| // collect the fanins of the implication supergate |
| Sim_SymmsBalanceCollect_rec( pNode, vNodes ); |
| |
| // sort the nodes in the implication supergate |
| Sim_SymmsPartitionNodes( vNodes, vNodesPi0, vNodesPi1, vNodesOther ); |
| |
| // start the resulting set |
| vSymms = Vec_IntAlloc( 10 ); |
| // generate symmetries from the groups |
| Sim_SymmsAppendFromGroup( pNtk, vNodesPi0, vNodesOther, vSymms, pMap ); |
| Sim_SymmsAppendFromGroup( pNtk, vNodesPi1, vNodesOther, vSymms, pMap ); |
| // add symmetries from other inputs |
| for ( i = 0; i < vNodesOther->nSize; i++ ) |
| { |
| pTemp = Abc_ObjRegular((Abc_Obj_t *)vNodesOther->pArray[i]); |
| Sim_SymmsAppendFromNode( pNtk, SIM_READ_SYMMS(pTemp), vNodesOther, vNodesPi0, vNodesPi1, vSymms, pMap ); |
| } |
| Vec_PtrFree( vNodes ); |
| Vec_PtrFree( vNodesPi0 ); |
| Vec_PtrFree( vNodesPi1 ); |
| Vec_PtrFree( vNodesOther ); |
| |
| // set the symmetry at the node |
| SIM_SET_SYMMS( pNode, vSymms ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) |
| { |
| // if the new node is complemented, another gate begins |
| if ( Abc_ObjIsComplement(pNode) ) |
| { |
| Vec_PtrPushUnique( vNodes, pNode ); |
| return; |
| } |
| // if pNew is the PI node, return |
| if ( Abc_ObjIsCi(pNode) ) |
| { |
| Vec_PtrPushUnique( vNodes, pNode ); |
| return; |
| } |
| // go through the branches |
| Sim_SymmsBalanceCollect_rec( Abc_ObjChild0(pNode), vNodes ); |
| Sim_SymmsBalanceCollect_rec( Abc_ObjChild1(pNode), vNodes ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Divides PI variables into groups.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, |
| Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther ) |
| { |
| Abc_Obj_t * pNode; |
| int i; |
| Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i ) |
| { |
| if ( !Abc_ObjIsCi(Abc_ObjRegular(pNode)) ) |
| Vec_PtrPush( vNodesOther, pNode ); |
| else if ( Abc_ObjIsComplement(pNode) ) |
| Vec_PtrPush( vNodesPis0, pNode ); |
| else |
| Vec_PtrPush( vNodesPis1, pNode ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Makes the product of two partitions.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap ) |
| { |
| Abc_Obj_t * pNode1, * pNode2; |
| unsigned uSymm; |
| int i, k; |
| |
| if ( vNodesPi->nSize == 0 ) |
| return; |
| |
| // go through the pairs |
| for ( i = 0; i < vNodesPi->nSize; i++ ) |
| for ( k = i+1; k < vNodesPi->nSize; k++ ) |
| { |
| // get the two PI nodes |
| pNode1 = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[i]); |
| pNode2 = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[k]); |
| assert( pMap[pNode1->Id] != pMap[pNode2->Id] ); |
| assert( pMap[pNode1->Id] >= 0 ); |
| assert( pMap[pNode2->Id] >= 0 ); |
| // generate symmetry |
| if ( pMap[pNode1->Id] < pMap[pNode2->Id] ) |
| uSymm = ((pMap[pNode1->Id] << 16) | pMap[pNode2->Id]); |
| else |
| uSymm = ((pMap[pNode2->Id] << 16) | pMap[pNode1->Id]); |
| // check if symmetry belongs |
| if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) ) |
| Vec_IntPushUnique( vSymms, (int)uSymm ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Add the filters symmetries from the nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, |
| Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap ) |
| { |
| unsigned uSymm; |
| int i; |
| |
| if ( vSymms0->nSize == 0 ) |
| return; |
| |
| // go through the pairs |
| for ( i = 0; i < vSymms0->nSize; i++ ) |
| { |
| uSymm = (unsigned)vSymms0->pArray[i]; |
| // check if symmetry belongs |
| if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) && |
| Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi0, pMap ) && |
| Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi1, pMap ) ) |
| Vec_IntPushUnique( vSymms, (int)uSymm ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if symmetry is compatible with the group of nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap ) |
| { |
| Vec_Int_t * vSymmsNode; |
| Abc_Obj_t * pNode; |
| int i, s, Ind1, Ind2, fIsVar1, fIsVar2; |
| |
| if ( vNodesOther->nSize == 0 ) |
| return 1; |
| |
| // get the indices of the PI variables |
| Ind1 = (uSymm & 0xffff); |
| Ind2 = (uSymm >> 16); |
| |
| // go through the nodes |
| // if they do not belong to a support, it is okay |
| // if one belongs, the other does not belong, quit |
| // if they belong, but are not part of symmetry, quit |
| for ( i = 0; i < vNodesOther->nSize; i++ ) |
| { |
| pNode = Abc_ObjRegular((Abc_Obj_t *)vNodesOther->pArray[i]); |
| fIsVar1 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind1 ); |
| fIsVar2 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind2 ); |
| |
| if ( !fIsVar1 && !fIsVar2 ) |
| continue; |
| if ( fIsVar1 ^ fIsVar2 ) |
| return 0; |
| // both belong |
| // check if there is a symmetry |
| vSymmsNode = SIM_READ_SYMMS( pNode ); |
| for ( s = 0; s < vSymmsNode->nSize; s++ ) |
| if ( uSymm == (unsigned)vSymmsNode->pArray[s] ) |
| break; |
| if ( s == vSymmsNode->nSize ) |
| return 0; |
| } |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if symmetry is compatible with the group of PIs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap ) |
| { |
| Abc_Obj_t * pNode; |
| int i, Ind1, Ind2, fHasVar1, fHasVar2; |
| |
| if ( vNodesPi->nSize == 0 ) |
| return 1; |
| |
| // get the indices of the PI variables |
| Ind1 = (uSymm & 0xffff); |
| Ind2 = (uSymm >> 16); |
| |
| // go through the PI nodes |
| fHasVar1 = fHasVar2 = 0; |
| for ( i = 0; i < vNodesPi->nSize; i++ ) |
| { |
| pNode = Abc_ObjRegular((Abc_Obj_t *)vNodesPi->pArray[i]); |
| if ( pMap[pNode->Id] == Ind1 ) |
| fHasVar1 = 1; |
| else if ( pMap[pNode->Id] == Ind2 ) |
| fHasVar2 = 1; |
| } |
| return fHasVar1 == fHasVar2; |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Improvements due to transitivity.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SymmsTrans( Vec_Int_t * vSymms ) |
| { |
| unsigned uSymm, uSymma, uSymmr; |
| int i, Ind1, Ind2; |
| int k, Ind1a, Ind2a; |
| int j; |
| int nTrans = 0; |
| |
| for ( i = 0; i < vSymms->nSize; i++ ) |
| { |
| uSymm = (unsigned)vSymms->pArray[i]; |
| Ind1 = (uSymm & 0xffff); |
| Ind2 = (uSymm >> 16); |
| // find other symmetries that have Ind1 |
| for ( k = i+1; k < vSymms->nSize; k++ ) |
| { |
| uSymma = (unsigned)vSymms->pArray[k]; |
| if ( uSymma == uSymm ) |
| continue; |
| Ind1a = (uSymma & 0xffff); |
| Ind2a = (uSymma >> 16); |
| if ( Ind1a == Ind1 ) |
| { |
| // find the symmetry (Ind2,Ind2a) |
| if ( Ind2 < Ind2a ) |
| uSymmr = ((Ind2 << 16) | Ind2a); |
| else |
| uSymmr = ((Ind2a << 16) | Ind2); |
| for ( j = 0; j < vSymms->nSize; j++ ) |
| if ( uSymmr == (unsigned)vSymms->pArray[j] ) |
| break; |
| if ( j == vSymms->nSize ) |
| nTrans++; |
| } |
| } |
| |
| } |
| printf( "Trans = %d.\n", nTrans ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Transfers from the vector to the matrix.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, unsigned * pSupport ) |
| { |
| int i, Ind1, Ind2, nInputs; |
| unsigned uSymm; |
| // add diagonal elements |
| nInputs = Extra_BitMatrixReadSize( pMatSymm ); |
| for ( i = 0; i < nInputs; i++ ) |
| Extra_BitMatrixInsert1( pMatSymm, i, i ); |
| // add non-diagonal elements |
| for ( i = 0; i < vSymms->nSize; i++ ) |
| { |
| uSymm = (unsigned)vSymms->pArray[i]; |
| Ind1 = (uSymm & 0xffff); |
| Ind2 = (uSymm >> 16); |
| //printf( "%d,%d ", Ind1, Ind2 ); |
| // skip variables that are not in the true support |
| assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) ); |
| if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) ) |
| continue; |
| Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 ); |
| Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Mapping of indices into numbers.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk ) |
| { |
| int * pMap; |
| Abc_Obj_t * pNode; |
| int i; |
| pMap = ABC_ALLOC( int, Abc_NtkObjNumMax(pNtk) ); |
| for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ ) |
| pMap[i] = -1; |
| Abc_NtkForEachCi( pNtk, pNode, i ) |
| pMap[pNode->Id] = i; |
| return pMap; |
| } |
| |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
