mirror of
https://github.com/YosysHQ/abc.git
synced 2026-09-05 00:51:01 +02:00
771 lines
24 KiB
C
771 lines
24 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [rsbDec6.c]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [Truth-table-based resubstitution.]
|
|
|
|
Synopsis [Implementation of the algorithm.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - June 20, 2005.]
|
|
|
|
Revision [$Id: rsbDec6.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "rsbInt.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static inline unsigned Rsb_DecTry0( word c )
|
|
{
|
|
return (unsigned)(c != 0);
|
|
}
|
|
static inline unsigned Rsb_DecTry1( word c, word f1 )
|
|
{
|
|
return (Rsb_DecTry0(c&f1) << 1) | Rsb_DecTry0(c&~f1);
|
|
}
|
|
static inline unsigned Rsb_DecTry2( word c, word f1, word f2 )
|
|
{
|
|
return (Rsb_DecTry1(c&f2, f1) << 2) | Rsb_DecTry1(c&~f2, f1);
|
|
}
|
|
static inline unsigned Rsb_DecTry3( word c, word f1, word f2, word f3 )
|
|
{
|
|
return (Rsb_DecTry2(c&f3, f1, f2) << 4) | Rsb_DecTry2(c&~f3, f1, f2);
|
|
}
|
|
static inline unsigned Rsb_DecTry4( word c, word f1, word f2, word f3, word f4 )
|
|
{
|
|
return (Rsb_DecTry3(c&f4, f1, f2, f3) << 8) | Rsb_DecTry3(c&~f4, f1, f2, f3);
|
|
}
|
|
static inline unsigned Rsb_DecTry5( word c, word f1, word f2, word f3, word f4, word f5 )
|
|
{
|
|
return (Rsb_DecTry4(c&f5, f1, f2, f3, f4) << 16) | Rsb_DecTry4(c&~f5, f1, f2, f3, f4);
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static inline int Rsb_DecTryCex( word * g, int iCexA, int iCexB )
|
|
{
|
|
return Abc_TtGetBit(g, iCexA) == Abc_TtGetBit(g, iCexB);
|
|
}
|
|
static inline void Rsb_DecVerifyCex( word * f, word ** g, int nGs, int iCexA, int iCexB )
|
|
{
|
|
int i;
|
|
// f distinquished it
|
|
if ( Rsb_DecTryCex( f, iCexA, iCexB ) )
|
|
printf( "Verification of CEX has failed: f(A) == f(B)!!!\n" );
|
|
// g do not distinguish it
|
|
for ( i = 0; i < nGs; i++ )
|
|
if ( !Rsb_DecTryCex( g[i], iCexA, iCexB ) )
|
|
printf( "Verification of CEX has failed: g[%d](A) != g[%d](B)!!!\n", i, i );
|
|
}
|
|
static inline void Rsb_DecRecordCex( word ** g, int nGs, int iCexA, int iCexB, word * pCexes, int nCexes )
|
|
{
|
|
int i;
|
|
assert( nCexes < 64 );
|
|
for ( i = 0; i < nGs; i++ )
|
|
if ( Rsb_DecTryCex(g[i], iCexA, iCexB) )
|
|
Abc_TtSetBit( pCexes + i, nCexes );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Checks decomposability of f with divisors g.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
static inline word Rsb_DecCofactor( word ** g, int nGs, int w, int iMint )
|
|
{
|
|
int i;
|
|
word Cof = ~(word)0;
|
|
for ( i = 0; i < nGs; i++ )
|
|
Cof &= ((iMint >> i) & 1) ? g[i][w] : ~g[i][w];
|
|
return Cof;
|
|
}
|
|
unsigned Rsb_DecCheck( int nVars, word * f, word ** g, int nGs, unsigned * pPat, int * pCexA, int * pCexB )
|
|
{
|
|
word CofA, CofB;
|
|
int nWords = Abc_TtWordNum( nVars );
|
|
int w, k, iMint, iShift = ( 1 << nGs );
|
|
unsigned uMask = (~(unsigned)0) >> (32-iShift);
|
|
unsigned uTotal = 0;
|
|
assert( nGs > 0 && nGs < 5 );
|
|
for ( w = 0; w < nWords; w++ )
|
|
{
|
|
// generate decomposition pattern
|
|
if ( nGs == 1 )
|
|
pPat[w] = Rsb_DecTry2( ~(word)0, g[0][w], f[w] );
|
|
else if ( nGs == 2 )
|
|
pPat[w] = Rsb_DecTry3( ~(word)0, g[0][w], g[1][w], f[w] );
|
|
else if ( nGs == 3 )
|
|
pPat[w] = Rsb_DecTry4( ~(word)0, g[0][w], g[1][w], g[2][w], f[w] );
|
|
else if ( nGs == 4 )
|
|
pPat[w] = Rsb_DecTry5( ~(word)0, g[0][w], g[1][w], g[2][w], g[3][w], f[w] );
|
|
// check if it is consistent
|
|
iMint = Abc_Tt6FirstBit( (pPat[w] >> iShift) & pPat[w] & uMask );
|
|
if ( iMint >= 0 )
|
|
{ // generate a cex
|
|
CofA = Rsb_DecCofactor( g, nGs, w, iMint );
|
|
assert( (~f[w] & CofA) && (f[w] & CofA) );
|
|
*pCexA = w * 64 + Abc_Tt6FirstBit( ~f[w] & CofA );
|
|
*pCexB = w * 64 + Abc_Tt6FirstBit( f[w] & CofA );
|
|
return 0;
|
|
}
|
|
uTotal |= pPat[w];
|
|
if ( w == 0 )
|
|
continue;
|
|
// check if it is consistent with other patterns seen so far
|
|
iMint = Abc_Tt6FirstBit( (uTotal >> iShift) & uTotal & uMask );
|
|
if ( iMint == -1 )
|
|
continue;
|
|
// find an overlap and generate a cex
|
|
for ( k = 0; k < w; k++ )
|
|
{
|
|
iMint = Abc_Tt6FirstBit( ((pPat[k] | pPat[w]) >> iShift) & (pPat[k] | pPat[w]) & uMask );
|
|
if ( iMint == -1 )
|
|
continue;
|
|
CofA = Rsb_DecCofactor( g, nGs, k, iMint );
|
|
CofB = Rsb_DecCofactor( g, nGs, w, iMint );
|
|
if ( (~f[k] & CofA) && (f[w] & CofB) )
|
|
{
|
|
*pCexA = k * 64 + Abc_Tt6FirstBit( ~f[k] & CofA );
|
|
*pCexB = w * 64 + Abc_Tt6FirstBit( f[w] & CofB );
|
|
}
|
|
else
|
|
{
|
|
assert( (f[k] & CofA) && (~f[w] & CofB) );
|
|
*pCexA = k * 64 + Abc_Tt6FirstBit( f[k] & CofA );
|
|
*pCexB = w * 64 + Abc_Tt6FirstBit( ~f[w] & CofB );
|
|
}
|
|
return 0;
|
|
}
|
|
}
|
|
return uTotal;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Rsb_DecPrintTable( word * pCexes, int nGs, int nGsAll, Vec_Int_t * vTries )
|
|
{
|
|
int pCands[16], nCands;
|
|
int i, c, Cand, iStart = 0;
|
|
if ( Vec_IntSize(vTries) == 0 )
|
|
return;
|
|
|
|
// printf( "\n" );
|
|
for ( i = 0; i < 4; i++ )
|
|
printf( " " );
|
|
printf( " " );
|
|
for ( i = 0; i < nGs; i++ )
|
|
printf( "%d", (i % 100) / 10 );
|
|
printf( "|" );
|
|
for ( ; i < nGsAll; i++ )
|
|
printf( "%d", (i % 100) / 10 );
|
|
printf( "\n" );
|
|
|
|
for ( i = 0; i < 4; i++ )
|
|
printf( " " );
|
|
printf( " " );
|
|
for ( i = 0; i < nGs; i++ )
|
|
printf( "%d", i % 10 );
|
|
printf( "|" );
|
|
for ( ; i < nGsAll; i++ )
|
|
printf( "%d", i % 10 );
|
|
printf( "\n" );
|
|
printf( "\n" );
|
|
|
|
for ( c = 0; iStart < Vec_IntSize(vTries); c++ )
|
|
{
|
|
// collect candidates
|
|
for ( i = 0; i < 4; i++ )
|
|
pCands[i] = -1;
|
|
nCands = 0;
|
|
Vec_IntForEachEntryStart( vTries, Cand, i, iStart )
|
|
if ( Cand == -1 )
|
|
{
|
|
iStart = i + 1;
|
|
break;
|
|
}
|
|
else
|
|
pCands[nCands++] = Cand;
|
|
assert( nCands <= 4 );
|
|
// print them
|
|
for ( i = 0; i < 4; i++ )
|
|
if ( pCands[i] >= 0 )
|
|
printf( "%4d", pCands[i] );
|
|
else
|
|
printf( " " );
|
|
// print the bit-string
|
|
printf( " " );
|
|
for ( i = 0; i < nGs; i++ )
|
|
printf( "%c", Abc_TtGetBit( pCexes + i, c ) ? '.' : '+' );
|
|
printf( "|" );
|
|
for ( ; i < nGsAll; i++ )
|
|
printf( "%c", Abc_TtGetBit( pCexes + i, c ) ? '.' : '+' );
|
|
printf( " %3d\n", c );
|
|
}
|
|
printf( "\n" );
|
|
|
|
// write the number of ones
|
|
for ( i = 0; i < 4; i++ )
|
|
printf( " " );
|
|
printf( " " );
|
|
for ( i = 0; i < nGs; i++ )
|
|
printf( "%d", Abc_TtCountOnes(pCexes[i]) / 10 );
|
|
printf( "|" );
|
|
for ( ; i < nGsAll; i++ )
|
|
printf( "%d", Abc_TtCountOnes(pCexes[i]) / 10 );
|
|
printf( "\n" );
|
|
|
|
for ( i = 0; i < 4; i++ )
|
|
printf( " " );
|
|
printf( " " );
|
|
for ( i = 0; i < nGs; i++ )
|
|
printf( "%d", Abc_TtCountOnes(pCexes[i]) % 10 );
|
|
printf( "|" );
|
|
for ( ; i < nGsAll; i++ )
|
|
printf( "%d", Abc_TtCountOnes(pCexes[i]) % 10 );
|
|
printf( "\n" );
|
|
printf( "\n" );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Init ]
|
|
|
|
Description [Returns the numbers of the decomposition functions and
|
|
the truth table of a function up to 4 variables.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Rsb_DecInitCexes( int nVars, word * f, word ** g, int nGs, int nGsAll, word * pCexes, Vec_Int_t * vTries )
|
|
{
|
|
int nWords = Abc_TtWordNum( nVars );
|
|
int ValueB = Abc_TtGetBit( f, 0 );
|
|
int ValueE = Abc_TtGetBit( f, 64*nWords-1 );
|
|
int iCexT0, iCexT1, iCexF0, iCexF1;
|
|
|
|
iCexT0 = ValueB ? 0 : Abc_TtFindFirstBit( f, nVars );
|
|
iCexT1 = ValueE ? 64*nWords-1 : Abc_TtFindLastBit( f, nVars );
|
|
|
|
iCexF0 = !ValueB ? 0 : Abc_TtFindFirstZero( f, nVars );
|
|
iCexF1 = !ValueE ? 64*nWords-1 : Abc_TtFindLastZero( f, nVars );
|
|
|
|
assert( !Rsb_DecTryCex( f, iCexT0, iCexF0 ) );
|
|
assert( !Rsb_DecTryCex( f, iCexT0, iCexF1 ) );
|
|
assert( !Rsb_DecTryCex( f, iCexT1, iCexF0 ) );
|
|
assert( !Rsb_DecTryCex( f, iCexT1, iCexF1 ) );
|
|
|
|
Rsb_DecRecordCex( g, nGsAll, iCexT0, iCexF0, pCexes, 0 );
|
|
Rsb_DecRecordCex( g, nGsAll, iCexT0, iCexF1, pCexes, 1 );
|
|
Rsb_DecRecordCex( g, nGsAll, iCexT1, iCexF0, pCexes, 2 );
|
|
Rsb_DecRecordCex( g, nGsAll, iCexT1, iCexF1, pCexes, 3 );
|
|
|
|
if ( vTries )
|
|
{
|
|
Vec_IntPush( vTries, -1 );
|
|
Vec_IntPush( vTries, -1 );
|
|
Vec_IntPush( vTries, -1 );
|
|
Vec_IntPush( vTries, -1 );
|
|
}
|
|
return 4;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Finds a setset of gs to decompose f.]
|
|
|
|
Description [Returns the numbers of the decomposition functions and
|
|
the truth table of a function up to 4 variables.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fFindAll )
|
|
{
|
|
word * pCexes = Vec_WrdArray(p->vCexes);
|
|
unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats);
|
|
/*
|
|
The following filtering hueristic can be used:
|
|
after the first round (if there is more than 5 cexes,
|
|
remove all the divisors, except fanins of the node
|
|
This should lead to a speadup without sacrifying quality.
|
|
|
|
Another idea is to precompute several counter-examples
|
|
like the first and last 0 and 1 mints of the function
|
|
which yields 4 cexes.
|
|
*/
|
|
|
|
word * pDivs[16];
|
|
unsigned uTruth = 0;
|
|
int i, k, j, n, iCexA, iCexB, nCexes = 0;
|
|
memset( pCexes, 0, sizeof(word) * nGsAll );
|
|
Vec_IntClear( p->vTries );
|
|
// populate the counter-examples with the three most obvious
|
|
// nCexes = Rsb_DecInitCexes( nVars, f, g, nGs, nGsAll, pCexes, vTries );
|
|
// start by checking each function
|
|
p->vFanins->nSize = 1;
|
|
for ( i = 0; i < nGs; i++ )
|
|
{
|
|
if ( pCexes[i] )
|
|
continue;
|
|
pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
|
|
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
|
|
if ( uTruth )
|
|
{
|
|
if ( fFindAll )
|
|
{
|
|
uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 1 );
|
|
Kit_DsdPrintFromTruth( &uTruth, 1 ); printf( " " );
|
|
Vec_IntPrint(p->vFanins);
|
|
continue;
|
|
}
|
|
else
|
|
return uTruth;
|
|
}
|
|
if ( nCexes == 64 )
|
|
return 0;
|
|
Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
|
|
Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
|
|
if ( !p->fVerbose )
|
|
continue;
|
|
Vec_IntPush( p->vTries, i );
|
|
Vec_IntPush( p->vTries, -1 );
|
|
}
|
|
if ( p->nDecMax == 1 )
|
|
return 0;
|
|
// continue by checking pairs
|
|
p->vFanins->nSize = 2;
|
|
for ( i = 1; i < nGs; i++ )
|
|
for ( k = 0; k < i; k++ )
|
|
{
|
|
if ( pCexes[i] & pCexes[k] )
|
|
continue;
|
|
pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
|
|
pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
|
|
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
|
|
if ( uTruth )
|
|
{
|
|
if ( fFindAll )
|
|
{
|
|
uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 2 );
|
|
Kit_DsdPrintFromTruth( &uTruth, 2 ); printf( " " );
|
|
Vec_IntPrint(p->vFanins);
|
|
continue;
|
|
}
|
|
else
|
|
return uTruth;
|
|
}
|
|
if ( nCexes == 64 )
|
|
return 0;
|
|
Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
|
|
Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
|
|
if ( !p->fVerbose )
|
|
continue;
|
|
Vec_IntPush( p->vTries, i );
|
|
Vec_IntPush( p->vTries, k );
|
|
Vec_IntPush( p->vTries, -1 );
|
|
}
|
|
if ( p->nDecMax == 2 )
|
|
return 0;
|
|
// continue by checking triples
|
|
p->vFanins->nSize = 3;
|
|
for ( i = 2; i < nGs; i++ )
|
|
for ( k = 1; k < i; k++ )
|
|
for ( j = 0; j < k; j++ )
|
|
{
|
|
if ( pCexes[i] & pCexes[k] & pCexes[j] )
|
|
continue;
|
|
pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
|
|
pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
|
|
pDivs[2] = g[j]; p->vFanins->pArray[2] = j;
|
|
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
|
|
if ( uTruth )
|
|
{
|
|
if ( fFindAll )
|
|
{
|
|
uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 3 );
|
|
Kit_DsdPrintFromTruth( &uTruth, 3 ); printf( " " );
|
|
Vec_IntPrint(p->vFanins);
|
|
continue;
|
|
}
|
|
else
|
|
return uTruth;
|
|
}
|
|
if ( nCexes == 64 )
|
|
return 0;
|
|
Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
|
|
Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
|
|
if ( !p->fVerbose )
|
|
continue;
|
|
Vec_IntPush( p->vTries, i );
|
|
Vec_IntPush( p->vTries, k );
|
|
Vec_IntPush( p->vTries, j );
|
|
Vec_IntPush( p->vTries, -1 );
|
|
}
|
|
if ( p->nDecMax == 3 )
|
|
return 0;
|
|
// continue by checking quadras
|
|
p->vFanins->nSize = 4;
|
|
for ( i = 3; i < nGs; i++ )
|
|
for ( k = 2; k < i; k++ )
|
|
for ( j = 1; j < k; j++ )
|
|
for ( n = 0; n < j; n++ )
|
|
{
|
|
if ( pCexes[i] & pCexes[k] & pCexes[j] & pCexes[n] )
|
|
continue;
|
|
pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
|
|
pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
|
|
pDivs[2] = g[j]; p->vFanins->pArray[2] = j;
|
|
pDivs[3] = g[n]; p->vFanins->pArray[3] = n;
|
|
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
|
|
if ( uTruth )
|
|
{
|
|
if ( fFindAll )
|
|
{
|
|
uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 4 );
|
|
Kit_DsdPrintFromTruth( &uTruth, 4 ); printf( " " );
|
|
Vec_IntPrint(p->vFanins);
|
|
continue;
|
|
}
|
|
else
|
|
return uTruth;
|
|
}
|
|
if ( nCexes == 64 )
|
|
return 0;
|
|
Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
|
|
Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
|
|
if ( !p->fVerbose )
|
|
continue;
|
|
Vec_IntPush( p->vTries, i );
|
|
Vec_IntPush( p->vTries, k );
|
|
Vec_IntPush( p->vTries, j );
|
|
Vec_IntPush( p->vTries, n );
|
|
Vec_IntPush( p->vTries, -1 );
|
|
}
|
|
// printf( "%d ", nCexes );
|
|
if ( p->nDecMax == 4 )
|
|
return 0;
|
|
return 0;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Verifies 4-input decomposition.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Rsb_DecPrintFunc( Rsb_Man_t * p, unsigned Truth4, word * f, word ** ppGs, int nGs, int nVarsAll )
|
|
{
|
|
int nVars = Vec_IntSize(p->vFanins);
|
|
word Copy = Truth4;
|
|
word wOn = Abc_Tt6Stretch( Copy >> (1 << nVars), nVars );
|
|
word wOnDc = ~Abc_Tt6Stretch( Copy, nVars );
|
|
word wIsop = Abc_Tt6Isop( wOn, wOnDc, nVars, NULL );
|
|
int i;
|
|
|
|
printf( "Offset : " );
|
|
Abc_TtPrintBinary( &Copy, nVars ); //printf( "\n" );
|
|
Copy >>= ((word)1 << nVars);
|
|
printf( "Onset : " );
|
|
Abc_TtPrintBinary( &Copy, nVars ); //printf( "\n" );
|
|
printf( "Result : " );
|
|
Abc_TtPrintBinary( &wIsop, nVars ); //printf( "\n" );
|
|
Kit_DsdPrintFromTruth( (unsigned *)&wIsop, nVars ); printf( "\n" );
|
|
|
|
// print functions
|
|
printf( "Func : " );
|
|
Abc_TtPrintBinary( f, nVarsAll ); //printf( "\n" );
|
|
Kit_DsdPrintFromTruth( (unsigned *)f, nVarsAll ); printf( "\n" );
|
|
for ( i = 0; i < nGs; i++ )
|
|
{
|
|
printf( "Div%3d : ", i );
|
|
Kit_DsdPrintFromTruth( (unsigned *)ppGs[i], nVarsAll ); printf( "\n" );
|
|
}
|
|
printf( "Solution : " );
|
|
for ( i = 0; i < Vec_IntSize(p->vFanins); i++ )
|
|
printf( "%d ", Vec_IntEntry(p->vFanins, i) );
|
|
printf( "\n" );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Verifies 4-input decomposition.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Rsb_DecVerify( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, unsigned Truth4, word * pTemp1, word * pTemp2 )
|
|
{
|
|
word * pFanins[16];
|
|
int b, m, Num, nSuppSize;
|
|
int nWords = Abc_TtWordNum(nVars);
|
|
Truth4 >>= (1 << Vec_IntSize(p->vFanins));
|
|
Truth4 = (unsigned)Abc_Tt6Stretch( (word)Truth4, Vec_IntSize(p->vFanins) );
|
|
//Kit_DsdPrintFromTruth( (unsigned *)&Truth4, Vec_IntSize(p->vFanins) );
|
|
//printf( "\n" );
|
|
// nSuppSize = Rsb_Word6SupportSize( Truth4 );
|
|
// assert( nSuppSize == Vec_IntSize(p->vFanins) );
|
|
nSuppSize = Vec_IntSize(p->vFanins);
|
|
// collect the fanins
|
|
Vec_IntForEachEntry( p->vFanins, Num, b )
|
|
{
|
|
assert( Num < nGs );
|
|
pFanins[b] = g[Num];
|
|
}
|
|
// create the or of ands
|
|
Abc_TtClear( pTemp1, nWords );
|
|
for ( m = 0; m < (1<<nSuppSize); m++ )
|
|
{
|
|
if ( ((Truth4 >> m) & 1) == 0 )
|
|
continue;
|
|
Abc_TtFill( pTemp2, nWords );
|
|
for ( b = 0; b < nSuppSize; b++ )
|
|
if ( (m >> b) & 1 )
|
|
Abc_TtAnd( pTemp2, pTemp2, pFanins[b], nWords, 0 );
|
|
else
|
|
Abc_TtSharp( pTemp2, pTemp2, pFanins[b], nWords );
|
|
Abc_TtOr( pTemp1, pTemp1, pTemp2, nWords );
|
|
}
|
|
// check the function
|
|
if ( !Abc_TtEqual( pTemp1, f, nWords ) )
|
|
printf( "Verification failed.\n" );
|
|
// else
|
|
// printf( "Verification passed.\n" );
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Finds a setset of gs to decompose f.]
|
|
|
|
Description [Returns the numbers of the decomposition functions and
|
|
the truth table of a function up to 4 variables.]
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
unsigned Rsb_ManPerform( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fVerbose0 )
|
|
{
|
|
word * pCexes = Vec_WrdArray(p->vCexes);
|
|
unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats);
|
|
int fVerbose = 0;//(nGs > 40);
|
|
Vec_Int_t * vTries = NULL;
|
|
unsigned uTruth;
|
|
|
|
// verify original decomposition
|
|
if ( Vec_IntSize(p->vFaninsOld) && Vec_IntSize(p->vFaninsOld) <= 4 )
|
|
{
|
|
word * pDivs[8];
|
|
int i, Entry, iCexA, iCexB;
|
|
Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
|
|
pDivs[i] = g[Entry];
|
|
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFaninsOld), pPat, &iCexA, &iCexB );
|
|
// assert( uTruth != 0 );
|
|
if ( fVerbose )
|
|
{
|
|
printf( "Verified orig decomp with %d vars {", Vec_IntSize(p->vFaninsOld) );
|
|
Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
|
|
printf( " %d", Entry );
|
|
printf( " }\n" );
|
|
}
|
|
if ( uTruth )
|
|
{
|
|
// if ( fVerbose )
|
|
// Rsb_DecPrintFunc( p, uTruth );
|
|
}
|
|
else
|
|
{
|
|
printf( "Verified orig decomp with %d vars {", Vec_IntSize(p->vFaninsOld) );
|
|
Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
|
|
printf( " %d", Entry );
|
|
printf( " }\n" );
|
|
printf( "Verification FAILED.\n" );
|
|
}
|
|
}
|
|
// start tries
|
|
if ( fVerbose )
|
|
vTries = Vec_IntAlloc( 100 );
|
|
assert( nGs < nGsAll );
|
|
uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll, 0 );
|
|
|
|
if ( uTruth )
|
|
{
|
|
if ( fVerbose )
|
|
{
|
|
int i, Entry;
|
|
printf( "Found decomp with %d vars {", Vec_IntSize(p->vFanins) );
|
|
Vec_IntForEachEntry( p->vFanins, Entry, i )
|
|
printf( " %d", Entry );
|
|
printf( " }\n" );
|
|
// Rsb_DecPrintFunc( p, uTruth );
|
|
// Rsb_DecVerify( nVars, f, g, nGs, p->vFanins, uTruth, g[nGsAll], g[nGsAll+1] );
|
|
}
|
|
}
|
|
else
|
|
{
|
|
Vec_IntShrink( p->vFanins, 0 );
|
|
if ( fVerbose )
|
|
printf( "Did not find decomposition with 4 variables.\n" );
|
|
}
|
|
|
|
if ( fVerbose )
|
|
Rsb_DecPrintTable( pCexes, nGs, nGsAll, vTries );
|
|
if ( fVerbose )
|
|
Vec_IntFree( vTries );
|
|
return uTruth;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Rsb_ManPerformResub6( Rsb_Man_t * p, int nVarsAll, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose )
|
|
{
|
|
word * pGs[200];
|
|
unsigned uTruthRes;
|
|
int i, nVars, nGs = Vec_WrdSize(vDivTruths);
|
|
assert( nGs < 200 );
|
|
for ( i = 0; i < nGs; i++ )
|
|
pGs[i] = Vec_WrdEntryP(vDivTruths,i);
|
|
uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs, 0 );
|
|
if ( uTruthRes == 0 )
|
|
return 0;
|
|
|
|
if ( fVerbose )
|
|
Rsb_DecPrintFunc( p, uTruthRes, &uTruth, pGs, nGs, nVarsAll );
|
|
if ( fVerbose )
|
|
Rsb_DecPrintTable( Vec_WrdArray(p->vCexes), nGs, nGs, p->vTries );
|
|
|
|
nVars = Vec_IntSize(p->vFanins);
|
|
*puTruth0 = Abc_Tt6Stretch( uTruthRes, nVars );
|
|
*puTruth1 = Abc_Tt6Stretch( uTruthRes >> (1 << nVars), nVars );
|
|
return 1;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis []
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Rsb_ManPerformResub6Test()
|
|
{
|
|
Rsb_Man_t * p;
|
|
Vec_Wrd_t * vDivTruths;
|
|
int RetValue;
|
|
word a = s_Truths6[0];
|
|
word b = s_Truths6[1];
|
|
word c = s_Truths6[2];
|
|
word d = s_Truths6[3];
|
|
word e = s_Truths6[4];
|
|
word f = s_Truths6[5];
|
|
word ab = a & b;
|
|
word cd = c & d;
|
|
word ef = e & f;
|
|
word F = ab | cd | ef;
|
|
word uTruth0, uTruth1;
|
|
|
|
vDivTruths = Vec_WrdAlloc( 100 );
|
|
Vec_WrdPush( vDivTruths, a );
|
|
Vec_WrdPush( vDivTruths, b );
|
|
Vec_WrdPush( vDivTruths, c );
|
|
Vec_WrdPush( vDivTruths, d );
|
|
Vec_WrdPush( vDivTruths, e );
|
|
Vec_WrdPush( vDivTruths, f );
|
|
Vec_WrdPush( vDivTruths, ab );
|
|
Vec_WrdPush( vDivTruths, cd );
|
|
Vec_WrdPush( vDivTruths, ef );
|
|
|
|
p = Rsb_ManAlloc( 6, 64, 4, 1 );
|
|
|
|
RetValue = Rsb_ManPerformResub6( p, 6, F, vDivTruths, &uTruth0, &uTruth1, 1 );
|
|
|
|
Rsb_ManFree( p );
|
|
Vec_WrdFree( vDivTruths );
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_IMPL_END
|
|
|