abc/src/aig/gia/giaDecs.c

351 lines
13 KiB
C

/**CFile****************************************************************
FileName [giaDecs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Calling various decomposition engines.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaDecs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"
#include "bool/bdc/bdc.h"
#include "bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut );
extern Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc, int Depth );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ResubVarNum( Vec_Int_t * vResub )
{
if ( Vec_IntSize(vResub) == 1 )
return Vec_IntEntryLast(vResub) >= 2;
return Vec_IntEntryLast(vResub)/2 - Vec_IntSize(vResub)/2 - 1;
}
word Gia_ResubToTruth6_rec( Vec_Int_t * vResub, int iNode, int nVars )
{
assert( iNode >= 0 && nVars <= 6 );
if ( iNode < nVars )
return s_Truths6[iNode];
else
{
int iLit0 = Vec_IntEntry( vResub, Abc_Var2Lit(iNode-nVars, 0) );
int iLit1 = Vec_IntEntry( vResub, Abc_Var2Lit(iNode-nVars, 1) );
word Res0 = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iLit0)-2, nVars );
word Res1 = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iLit1)-2, nVars );
Res0 = Abc_LitIsCompl(iLit0) ? ~Res0 : Res0;
Res1 = Abc_LitIsCompl(iLit1) ? ~Res1 : Res1;
return iLit0 > iLit1 ? Res0 ^ Res1 : Res0 & Res1;
}
}
word Gia_ResubToTruth6( Vec_Int_t * vResub )
{
word Res;
int iRoot = Vec_IntEntryLast(vResub);
if ( iRoot < 2 )
return iRoot ? ~(word)0 : 0;
assert( iRoot != 2 && iRoot != 3 );
Res = Gia_ResubToTruth6_rec( vResub, Abc_Lit2Var(iRoot)-2, Gia_ResubVarNum(vResub) );
return Abc_LitIsCompl(iRoot) ? ~Res : Res;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wrd_t * Gia_ManDeriveTruths( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords )
{
int nTtWords = Abc_Truth6WordNum(Vec_IntSize(vSet));
int nFuncs = Vec_WrdSize(vIsfs) / 2 / nWords;
Vec_Wrd_t * vRes = Vec_WrdStart( 2 * nFuncs * nTtWords );
Vec_Wrd_t * vIn = Vec_WrdStart( 64*nWords ), * vOut;
int i, f, m, iObj; word Func;
assert( Vec_IntSize(vSet) <= 64 );
Vec_IntForEachEntry( vSet, iObj, i )
Abc_TtCopy( Vec_WrdEntryP(vIn, i*nWords), Vec_WrdEntryP(vSims, Vec_IntEntry(vCands, iObj)*nWords), nWords, 0 );
vOut = Vec_WrdStart( Vec_WrdSize(vIn) );
Extra_BitMatrixTransposeP( vIn, nWords, vOut, 1 );
for ( f = 0; f < nFuncs; f++ )
{
word * pIsf[2] = { Vec_WrdEntryP(vIsfs, (2*f+0)*nWords),
Vec_WrdEntryP(vIsfs, (2*f+1)*nWords) };
word * pTruth[2] = { Vec_WrdEntryP(vRes, (2*f+0)*nTtWords),
Vec_WrdEntryP(vRes, (2*f+1)*nTtWords) };
for ( m = 0; m < 64*nWords; m++ )
{
int iMint = (int)Vec_WrdEntry(vOut, m);
int Value0 = Abc_TtGetBit( pIsf[0], m );
int Value1 = Abc_TtGetBit( pIsf[1], m );
if ( !Value0 && !Value1 )
continue;
if ( Value0 && Value1 )
printf( "Internal error: Onset and Offset overlap.\n" );
assert( !Value0 || !Value1 );
Abc_TtSetBit( pTruth[Value1], iMint );
}
if ( Abc_TtCountOnesVecMask(pTruth[0], pTruth[1], nTtWords, 0) )
printf( "Verification for function %d failed for %d minterm pairs.\n", f,
Abc_TtCountOnesVecMask(pTruth[0], pTruth[1], nTtWords, 0) );
}
if ( Vec_IntSize(vSet) < 6 )
Vec_WrdForEachEntry( vRes, Func, i )
Vec_WrdWriteEntry( vRes, i, Abc_Tt6Stretch(Func, Vec_IntSize(vSet)) );
Vec_WrdFree( vIn );
Vec_WrdFree( vOut );
return vRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCountResub( Vec_Wrd_t * vTruths, int nVars, int fVerbose )
{
Vec_Int_t * vResub; int nNodes;
int nTtWords = Abc_Truth6WordNum(nVars);
int v, nFuncs = Vec_WrdSize(vTruths) / 2 / nTtWords;
Vec_Wrd_t * vElems = Vec_WrdStartTruthTables( nVars );
Vec_Ptr_t * vDivs = Vec_PtrAlloc( 2 + nVars );
assert( Vec_WrdSize(vElems) == nTtWords * nVars );
assert( nFuncs == 1 );
Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+0)*nTtWords) );
Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+1)*nTtWords) );
for ( v = 0; v < nVars; v++ )
Vec_PtrPush( vDivs, Vec_WrdEntryP(vElems, v*nTtWords) );
vResub = Gia_ManResubOne( vDivs, nTtWords, 30, 100, 0, 0, 0, fVerbose, NULL, 0 );
Vec_PtrFree( vDivs );
Vec_WrdFree( vElems );
nNodes = Vec_IntSize(vResub) ? Vec_IntSize(vResub)/2 : 999;
Vec_IntFree( vResub );
return nNodes;
}
Vec_Int_t * Gia_ManDeriveResub( Vec_Wrd_t * vTruths, int nVars )
{
Vec_Int_t * vResub;
int nTtWords = Abc_Truth6WordNum(nVars);
int v, nFuncs = Vec_WrdSize(vTruths) / 2 / nTtWords;
Vec_Wrd_t * vElems = Vec_WrdStartTruthTables( nVars );
Vec_Ptr_t * vDivs = Vec_PtrAlloc( 2 + nVars );
assert( Vec_WrdSize(vElems) == nTtWords * nVars );
assert( nFuncs == 1 );
Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+0)*nTtWords) );
Vec_PtrPush( vDivs, Vec_WrdEntryP(vTruths, (2*0+1)*nTtWords) );
for ( v = 0; v < nVars; v++ )
Vec_PtrPush( vDivs, Vec_WrdEntryP(vElems, v*nTtWords) );
vResub = Gia_ManResubOne( vDivs, nTtWords, 30, 100, 0, 0, 0, 0, NULL, 0 );
Vec_PtrFree( vDivs );
Vec_WrdFree( vElems );
return vResub;
}
int Gia_ManCountBidec( Vec_Wrd_t * vTruths, int nVars, int fVerbose )
{
int nNodes, nTtWords = Abc_Truth6WordNum(nVars);
word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords),
Vec_WrdEntryP(vTruths, 1*nTtWords) };
Abc_TtOr( pTruth[0], pTruth[0], pTruth[1], nTtWords );
nNodes = Bdc_ManBidecNodeNum( pTruth[1], pTruth[0], nVars, fVerbose );
Abc_TtSharp( pTruth[0], pTruth[0], pTruth[1], nTtWords );
return nNodes;
}
Vec_Int_t * Gia_ManDeriveBidec( Vec_Wrd_t * vTruths, int nVars )
{
Vec_Int_t * vRes = NULL;
int nTtWords = Abc_Truth6WordNum(nVars);
word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords),
Vec_WrdEntryP(vTruths, 1*nTtWords) };
Abc_TtOr( pTruth[0], pTruth[0], pTruth[1], nTtWords );
vRes = Bdc_ManBidecResub( pTruth[1], pTruth[0], nVars );
Abc_TtSharp( pTruth[0], pTruth[0], pTruth[1], nTtWords );
return vRes;
}
int Gia_ManCountIsop( Vec_Wrd_t * vTruths, int nVars, int fVerbose )
{
int nTtWords = Abc_Truth6WordNum(nVars);
word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords),
Vec_WrdEntryP(vTruths, 1*nTtWords) };
int nNodes = Kit_IsopNodeNum( (unsigned *)pTruth[0], (unsigned *)pTruth[1], nVars, NULL );
return nNodes;
}
Vec_Int_t * Gia_ManDeriveIsop( Vec_Wrd_t * vTruths, int nVars )
{
Vec_Int_t * vRes = NULL;
int nTtWords = Abc_Truth6WordNum(nVars);
word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords),
Vec_WrdEntryP(vTruths, 1*nTtWords) };
vRes = Kit_IsopResub( (unsigned *)pTruth[0], (unsigned *)pTruth[1], nVars, NULL );
return vRes;
}
int Gia_ManCountBdd( Vec_Wrd_t * vTruths, int nVars, int fVerbose )
{
extern Gia_Man_t * Gia_TryPermOptNew( word * pTruths, int nIns, int nOuts, int nWords, int nRounds, int fVerbose );
int nTtWords = Abc_Truth6WordNum(nVars);
word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords),
Vec_WrdEntryP(vTruths, 1*nTtWords) };
Gia_Man_t * pGia; int nNodes;
Abc_TtOr( pTruth[1], pTruth[1], pTruth[0], nTtWords );
Abc_TtNot( pTruth[0], nTtWords );
pGia = Gia_TryPermOptNew( pTruth[0], nVars, 1, nTtWords, 50, 0 );
Abc_TtNot( pTruth[0], nTtWords );
Abc_TtSharp( pTruth[1], pTruth[1], pTruth[0], nTtWords );
nNodes = Gia_ManAndNum(pGia);
Gia_ManStop( pGia );
return nNodes;
}
Vec_Int_t * Gia_ManDeriveBdd( Vec_Wrd_t * vTruths, int nVars )
{
extern Vec_Int_t * Gia_ManToGates( Gia_Man_t * p );
Vec_Int_t * vRes = NULL;
extern Gia_Man_t * Gia_TryPermOptNew( word * pTruths, int nIns, int nOuts, int nWords, int nRounds, int fVerbose );
int nTtWords = Abc_Truth6WordNum(nVars);
word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords),
Vec_WrdEntryP(vTruths, 1*nTtWords) };
Gia_Man_t * pGia;
Abc_TtOr( pTruth[1], pTruth[1], pTruth[0], nTtWords );
Abc_TtNot( pTruth[0], nTtWords );
pGia = Gia_TryPermOptNew( pTruth[0], nVars, 1, nTtWords, 50, 0 );
Abc_TtNot( pTruth[0], nTtWords );
Abc_TtSharp( pTruth[1], pTruth[1], pTruth[0], nTtWords );
vRes = Gia_ManToGates( pGia );
Gia_ManStop( pGia );
return vRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManEvalSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int fVerbose )
{
Vec_Wrd_t * vTruths = Gia_ManDeriveTruths( p, vSims, vIsfs, vCands, vSet, nWords );
int nTtWords = Vec_WrdSize(vTruths)/2, nVars = Vec_IntSize(vSet);
word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords),
Vec_WrdEntryP(vTruths, 1*nTtWords) };
int nNodesResub = Gia_ManCountResub( vTruths, nVars, 0 );
int nNodesBidec = nVars > 2 ? Gia_ManCountBidec( vTruths, nVars, 0 ) : 999;
int nNodesIsop = nVars > 2 ? Gia_ManCountIsop( vTruths, nVars, 0 ) : 999;
int nNodesBdd = nVars > 2 ? Gia_ManCountBdd( vTruths, nVars, 0 ) : 999;
int nNodesMin = Abc_MinInt( Abc_MinInt(nNodesResub, nNodesBidec), Abc_MinInt(nNodesIsop, nNodesBdd) );
if ( fVerbose )
{
printf( "Size = %2d ", nVars );
printf( "Resub =%3d ", nNodesResub );
printf( "Bidec =%3d ", nNodesBidec );
printf( "Isop =%3d ", nNodesIsop );
printf( "Bdd =%3d ", nNodesBdd );
Abc_TtIsfPrint( pTruth[0], pTruth[1], nTtWords );
if ( nVars <= 6 )
{
printf( " " );
Extra_PrintHex( stdout, (unsigned*)pTruth[0], nVars );
printf( " " );
Extra_PrintHex( stdout, (unsigned*)pTruth[1], nVars );
}
printf( "\n" );
}
Vec_WrdFree( vTruths );
if ( nNodesMin > 500 )
return -1;
if ( nNodesMin == nNodesResub )
return (nNodesMin << 2) | 0;
if ( nNodesMin == nNodesBidec )
return (nNodesMin << 2) | 1;
if ( nNodesMin == nNodesIsop )
return (nNodesMin << 2) | 2;
if ( nNodesMin == nNodesBdd )
return (nNodesMin << 2) | 3;
return -1;
}
Vec_Int_t * Gia_ManDeriveSolutionOne( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * vSet, int nWords, int Type )
{
Vec_Int_t * vRes = NULL;
Vec_Wrd_t * vTruths = Gia_ManDeriveTruths( p, vSims, vIsfs, vCands, vSet, nWords );
int nTtWords = Vec_WrdSize(vTruths)/2, nVars = Vec_IntSize(vSet);
word * pTruth[2] = { Vec_WrdEntryP(vTruths, 0*nTtWords),
Vec_WrdEntryP(vTruths, 1*nTtWords) };
if ( Type == 0 )
vRes = Gia_ManDeriveResub( vTruths, nVars );
else if ( Type == 1 )
vRes = Gia_ManDeriveBidec( vTruths, nVars );
else if ( Type == 2 )
vRes = Gia_ManDeriveIsop( vTruths, nVars );
else if ( Type == 3 )
vRes = Gia_ManDeriveBdd( vTruths, nVars );
if ( vRes && Gia_ResubVarNum(vRes) <= 6 )
{
word Func = Gia_ResubToTruth6( vRes );
assert( !(Func & pTruth[0][0]) );
assert( !(pTruth[1][0] & ~Func) );
}
Vec_WrdFree( vTruths );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END