/**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