/**CFile****************************************************************
FileName [amapPerm.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Technology mapper for standard cells.]
Synopsis [Deriving permutation for the gate.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: amapPerm.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "amapInt.h"
#include "bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Collects fanins of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Amap_LibCollectFanins_rec( Amap_Lib_t * pLib, Amap_Nod_t * pNod, Vec_Int_t * vFanins )
{
Amap_Nod_t * pFan0, * pFan1;
if ( pNod->Id == 0 )
{
Vec_IntPush( vFanins, 0 );
return;
}
pFan0 = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan0) );
if ( Abc_LitIsCompl(pNod->iFan0) || pFan0->Type != pNod->Type )
Vec_IntPush( vFanins, pNod->iFan0 );
else
Amap_LibCollectFanins_rec( pLib, pFan0, vFanins );
pFan1 = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan1) );
if ( Abc_LitIsCompl(pNod->iFan1) || pFan1->Type != pNod->Type )
Vec_IntPush( vFanins, pNod->iFan1 );
else
Amap_LibCollectFanins_rec( pLib, pFan1, vFanins );
}
/**Function*************************************************************
Synopsis [Collects fanins of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Amap_LibCollectFanins( Amap_Lib_t * pLib, Amap_Nod_t * pNod )
{
Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
Amap_LibCollectFanins_rec( pLib, pNod, vFanins );
return vFanins;
}
/**Function*************************************************************
Synopsis [Matches the node with the DSD node.]
Description [Returns perm if the node can be matched.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Amap_LibDeriveGatePerm_rec( Amap_Lib_t * pLib, Kit_DsdNtk_t * pNtk, int iLit, Amap_Nod_t * pNod )
{
Vec_Int_t * vPerm, * vPermFanin, * vNodFanin, * vDsdLits;
Kit_DsdObj_t * pDsdObj, * pDsdFanin;
Amap_Nod_t * pNodFanin;
int iDsdFanin, iNodFanin, Value, iDsdLit, i, k, j;
assert( !Abc_LitIsCompl(iLit) );
pDsdObj = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iLit) );
if ( pDsdObj == NULL )
{
vPerm = Vec_IntAlloc( 1 );
Vec_IntPush( vPerm, iLit );
return vPerm;
}
if ( pDsdObj->Type == KIT_DSD_PRIME && pNod->Type == AMAP_OBJ_MUX )
{
vPerm = Vec_IntAlloc( 10 );
iDsdFanin = Abc_LitRegular(pDsdObj->pFans[0]);
pNodFanin = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan0) );
vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
if ( vPermFanin == NULL )
{
Vec_IntFree( vPerm );
return NULL;
}
Vec_IntForEachEntry( vPermFanin, Value, k )
Vec_IntPush( vPerm, Value );
Vec_IntFree( vPermFanin );
iDsdFanin = Abc_LitRegular(pDsdObj->pFans[1]);
pNodFanin = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan1) );
vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
if ( vPermFanin == NULL )
{
Vec_IntFree( vPerm );
return NULL;
}
Vec_IntForEachEntry( vPermFanin, Value, k )
Vec_IntPush( vPerm, Value );
Vec_IntFree( vPermFanin );
iDsdFanin = Abc_LitRegular(pDsdObj->pFans[2]);
pNodFanin = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan2) );
vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, iDsdFanin, pNodFanin );
if ( vPermFanin == NULL )
{
Vec_IntFree( vPerm );
return NULL;
}
Vec_IntForEachEntry( vPermFanin, Value, k )
Vec_IntPush( vPerm, Value );
Vec_IntFree( vPermFanin );
return vPerm;
}
// return if wrong types
if ( pDsdObj->Type == KIT_DSD_PRIME || pNod->Type == AMAP_OBJ_MUX )
return NULL;
// return if sizes do not agree
vNodFanin = Amap_LibCollectFanins( pLib, pNod );
if ( Vec_IntSize(vNodFanin) != (int)pDsdObj->nFans )
{
Vec_IntFree( vNodFanin );
return NULL;
}
// match fanins of DSD with fanins of nodes
// clean the mark and save variable literals
vPerm = Vec_IntAlloc( 10 );
vDsdLits = Vec_IntAlloc( 10 );
Kit_DsdObjForEachFaninReverse( pNtk, pDsdObj, iDsdFanin, i )
{
pDsdFanin = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iDsdFanin) );
if ( pDsdFanin )
pDsdFanin->fMark = 0;
else
Vec_IntPush( vDsdLits, iDsdFanin );
}
// match each fanins of the node
iDsdLit = 0;
Vec_IntForEachEntry( vNodFanin, iNodFanin, k )
{
if ( iNodFanin == 0 )
{
if ( iDsdLit >= Vec_IntSize(vDsdLits) )
{
Vec_IntFree( vPerm );
Vec_IntFree( vDsdLits );
Vec_IntFree( vNodFanin );
return NULL;
}
iDsdFanin = Vec_IntEntry( vDsdLits, iDsdLit++ );
Vec_IntPush( vPerm, iDsdFanin );
continue;
}
// find a matching component
pNodFanin = Amap_LibNod( pLib, Abc_Lit2Var(iNodFanin) );
Kit_DsdObjForEachFaninReverse( pNtk, pDsdObj, iDsdFanin, i )
{
pDsdFanin = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iDsdFanin) );
if ( pDsdFanin == NULL )
continue;
if ( pDsdFanin->fMark == 1 )
continue;
if ( !((pDsdFanin->Type == KIT_DSD_AND && pNodFanin->Type == AMAP_OBJ_AND) ||
(pDsdFanin->Type == KIT_DSD_XOR && pNodFanin->Type == AMAP_OBJ_XOR) ||
(pDsdFanin->Type == KIT_DSD_PRIME && pNodFanin->Type == AMAP_OBJ_MUX)) )
continue;
vPermFanin = Amap_LibDeriveGatePerm_rec( pLib, pNtk, Abc_LitRegular(iDsdFanin), pNodFanin );
if ( vPermFanin == NULL )
{
Vec_IntFree( vNodFanin );
Vec_IntFree( vDsdLits );
Vec_IntFree( vPerm );
return NULL;
}
pDsdFanin->fMark = 1;
Vec_IntForEachEntry( vPermFanin, Value, j )
Vec_IntPush( vPerm, Value );
Vec_IntFree( vPermFanin );
break;
}
}
// assert( iDsdLit == Vec_IntSize(vDsdLits) );
if ( iDsdLit != Vec_IntSize(vDsdLits) )
Vec_IntFreeP( &vPerm );
Vec_IntFree( vNodFanin );
Vec_IntFree( vDsdLits );
return vPerm;
}
/**Function*************************************************************
Synopsis [Performs verification of one gate and one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Amap_LibVerifyPerm_rec( Amap_Lib_t * pLib, Amap_Nod_t * pNod,
Vec_Ptr_t * vTtElems, Vec_Int_t * vTruth, int nWords, int * piInput )
{
Amap_Nod_t * pFan0, * pFan1;
unsigned * pTruth0, * pTruth1, * pTruth;
int i;
assert( pNod->Type != AMAP_OBJ_MUX );
if ( pNod->Id == 0 )
return (unsigned *)Vec_PtrEntry( vTtElems, (*piInput)++ );
pFan0 = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan0) );
pTruth0 = Amap_LibVerifyPerm_rec( pLib, pFan0, vTtElems, vTruth, nWords, piInput );
pFan1 = Amap_LibNod( pLib, Abc_Lit2Var(pNod->iFan1) );
pTruth1 = Amap_LibVerifyPerm_rec( pLib, pFan1, vTtElems, vTruth, nWords, piInput );
pTruth = Vec_IntFetch( vTruth, nWords );
if ( pNod->Type == AMAP_OBJ_XOR )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] ^ pTruth1[i];
else if ( !Abc_LitIsCompl(pNod->iFan0) && !Abc_LitIsCompl(pNod->iFan1) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & pTruth1[i];
else if ( !Abc_LitIsCompl(pNod->iFan0) && Abc_LitIsCompl(pNod->iFan1) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & ~pTruth1[i];
else if ( Abc_LitIsCompl(pNod->iFan0) && !Abc_LitIsCompl(pNod->iFan1) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & pTruth1[i];
else // if ( Abc_LitIsCompl(pNod->iFan0) && Hop_ObjFaninC1(pObj) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
return pTruth;
}
/**Function*************************************************************
Synopsis [Performs verification of one gate and one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Amap_LibVerifyPerm( Amap_Lib_t * pLib, Amap_Gat_t * pGate, Kit_DsdNtk_t * pNtk, Amap_Nod_t * pNod, int * pArray )
{
Vec_Ptr_t * vTtElems;
Vec_Ptr_t * vTtElemsPol;
Vec_Int_t * vTruth;
unsigned * pTruth;
int i, nWords;
int iInput = 0;
// allocate storage for truth tables
assert( pGate->nPins > 1 );
nWords = Kit_TruthWordNum( pGate->nPins );
vTruth = Vec_IntAlloc( nWords * AMAP_MAXINS );
vTtElems = Vec_PtrAllocTruthTables( pGate->nPins );
vTtElemsPol = Vec_PtrAlloc( pGate->nPins );
for ( i = 0; i < (int)pGate->nPins; i++ )
{
pTruth = (unsigned *)Vec_PtrEntry( vTtElems, Abc_Lit2Var(pArray[i]) );
if ( Abc_LitIsCompl( pArray[i] ) )
Kit_TruthNot( pTruth, pTruth, pGate->nPins );
Vec_PtrPush( vTtElemsPol, pTruth );
}
//Extra_PrintBinary( stdout, Vec_PtrEntry(vTtElemsPol, 0), 4 ); printf("\n" );
//Extra_PrintBinary( stdout, Vec_PtrEntry(vTtElemsPol, 1), 4 ); printf("\n" );
// compute the truth table recursively
pTruth = Amap_LibVerifyPerm_rec( pLib, pNod, vTtElemsPol, vTruth, nWords, &iInput );
assert( iInput == (int)pGate->nPins );
if ( Abc_LitIsCompl(pNtk->Root) )
Kit_TruthNot( pTruth, pTruth, pGate->nPins );
//Extra_PrintBinary( stdout, pTruth, 4 ); printf("\n" );
//Extra_PrintBinary( stdout, pGate->pFunc, 4 ); printf("\n" );
// compare
if ( !Kit_TruthIsEqual(pGate->pFunc, pTruth, pGate->nPins) )
printf( "Verification failed for gate %d (%s) and node %d.\n",
pGate->Id, pGate->pForm, pNod->Id );
Vec_IntFree( vTruth );
Vec_PtrFree( vTtElems );
Vec_PtrFree( vTtElemsPol );
}
/**Function*************************************************************
Synopsis [Matches the node with the DSD of a gate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Amap_LibDeriveGatePerm( Amap_Lib_t * pLib, Amap_Gat_t * pGate, Kit_DsdNtk_t * pNtk, Amap_Nod_t * pNod, char * pArray )
{
int fVerbose = 0;
Vec_Int_t * vPerm;
int Entry, Entry2, i, k;
// Kit_DsdPrint( stdout, pNtk );
vPerm = Amap_LibDeriveGatePerm_rec( pLib, pNtk, Abc_LitRegular(pNtk->Root), pNod );
if ( vPerm == NULL )
return 0;
// check that the permutation is valid
assert( Vec_IntSize(vPerm) == (int)pNod->nSuppSize );
Vec_IntForEachEntry( vPerm, Entry, i )
Vec_IntForEachEntryStart( vPerm, Entry2, k, i+1 )
if ( Abc_Lit2Var(Entry) == Abc_Lit2Var(Entry2) )
{
Vec_IntFree( vPerm );
return 0;
}
// reverse the permutation
Vec_IntForEachEntry( vPerm, Entry, i )
{
assert( Entry < 2 * (int)pNod->nSuppSize );
pArray[Abc_Lit2Var(Entry)] = Abc_Var2Lit( i, Abc_LitIsCompl(Entry) );
// pArray[i] = Entry;
//printf( "%d=%d%c ", Abc_Lit2Var(Entry), i, Abc_LitIsCompl(Entry)?'-':'+' );
}
//printf( "\n" );
// if ( Kit_DsdNonDsdSizeMax(pNtk) < 3 )
// Amap_LibVerifyPerm( pLib, pGate, pNtk, pNod, Vec_IntArray(vPerm) );
Vec_IntFree( vPerm );
// print the result
if ( fVerbose )
{
printf( "node %4d : ", pNod->Id );
for ( i = 0; i < (int)pNod->nSuppSize; i++ )
printf( "%d=%d%c ", i, Abc_Lit2Var(pArray[i]), Abc_LitIsCompl(pArray[i])?'-':'+' );
printf( "\n" );
}
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END