luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experimental resubstitution.

This commit is contained in:
Alan Mishchenko 2020-05-07 20:06:39 -07:00
parent f8b6d615bf
commit 372eb7bdef
2 changed files with 444 additions and 227 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

663
src/aig/gia/giaResub.c
View File

@ -26,7 +26,6 @@
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@ -290,6 +289,7 @@ typedef struct Gia_ResbMan_t_ Gia_ResbMan_t;
struct Gia_ResbMan_t_
{
int nWords;
int fVerbose;
Vec_Ptr_t * vDivs;
Vec_Int_t * vGates;
Vec_Int_t * vUnateLits[2];
@ -298,15 +298,15 @@ struct Gia_ResbMan_t_
Vec_Int_t * vBinateVars;
Vec_Int_t * vUnateLitsW[2];
Vec_Int_t * vUnatePairsW[2];
word * pSets[2];
word * pDivA;
word * pDivB;
Vec_Wrd_t * vSims;
};
Gia_ResbMan_t * Gia_ResbAlloc( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates )
Gia_ResbMan_t * Gia_ResbAlloc( int nWords )
{
Gia_ResbMan_t * p = ABC_CALLOC( Gia_ResbMan_t, 1 );
p->nWords = nWords;
p->vDivs = vDivs;
p->vGates = vGates;
p->vUnateLits[0] = Vec_IntAlloc( 100 );
p->vUnateLits[1] = Vec_IntAlloc( 100 );
p->vNotUnateVars[0] = Vec_IntAlloc( 100 );
@ -318,12 +318,22 @@ Gia_ResbMan_t * Gia_ResbAlloc( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates
p->vUnatePairsW[0] = Vec_IntAlloc( 100 );
p->vUnatePairsW[1] = Vec_IntAlloc( 100 );
p->vBinateVars = Vec_IntAlloc( 100 );
p->pSets[0] = ABC_CALLOC( word, nWords );
p->pSets[1] = ABC_CALLOC( word, nWords );
p->pDivA = ABC_CALLOC( word, nWords );
p->pDivB = ABC_CALLOC( word, nWords );
p->vSims = Vec_WrdAlloc( 100 );
return p;
}
void Gia_ResbReset( Gia_ResbMan_t * p )
void Gia_ResbInit( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates, int fVerbose )
{
assert( p->nWords == nWords );
p->fVerbose = fVerbose;
Abc_TtCopy( p->pSets[0], (word *)Vec_PtrEntry(vDivs, 0), nWords, 0 );
Abc_TtCopy( p->pSets[1], (word *)Vec_PtrEntry(vDivs, 1), nWords, 0 );
p->vDivs = vDivs;
p->vGates = vGates;
Vec_IntClear( p->vGates );
Vec_IntClear( p->vUnateLits[0] );
Vec_IntClear( p->vUnateLits[1] );
Vec_IntClear( p->vNotUnateVars[0] );
@ -349,11 +359,69 @@ void Gia_ResbFree( Gia_ResbMan_t * p )
Vec_IntFree( p->vUnatePairsW[0] );
Vec_IntFree( p->vUnatePairsW[1] );
Vec_IntFree( p->vBinateVars );
Vec_WrdFree( p->vSims );
ABC_FREE( p->pSets[0] );
ABC_FREE( p->pSets[1] );
ABC_FREE( p->pDivA );
ABC_FREE( p->pDivB );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Print resubstitution.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManResubPrintNode( Vec_Int_t * vRes, int nVars, int Node, int fCompl )
{
extern void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit );
int iLit0 = Vec_IntEntry( vRes, 2*Node + 0 );
int iLit1 = Vec_IntEntry( vRes, 2*Node + 1 );
assert( iLit0 != iLit1 );
if ( iLit0 > iLit1 && Abc_LitIsCompl(fCompl) ) // xor
{
printf( "~" );
fCompl = 0;
}
printf( "(" );
Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit0, fCompl) );
printf( " %c ", iLit0 > iLit1 ? '^' : (fCompl ? '|' : '&') );
Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit1, fCompl) );
printf( ")" );
}
void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit )
{
if ( Abc_Lit2Var(iLit) < nVars )
{
if ( nVars < 26 )
printf( "%s%c", Abc_LitIsCompl(iLit) ? "~":"", 'a' + Abc_Lit2Var(iLit)-2 );
else
printf( "%si%d", Abc_LitIsCompl(iLit) ? "~":"", Abc_Lit2Var(iLit)-2 );
}
else
Gia_ManResubPrintNode( vRes, nVars, Abc_Lit2Var(iLit) - nVars, Abc_LitIsCompl(iLit) );
}
int Gia_ManResubPrint( Vec_Int_t * vRes, int nVars )
{
int iTopLit;
if ( Vec_IntSize(vRes) == 0 )
return printf( "none" );
assert( Vec_IntSize(vRes) % 2 == 1 );
iTopLit = Vec_IntEntryLast(vRes);
if ( iTopLit == 0 )
return printf( "const0" );
if ( iTopLit == 1 )
return printf( "const1" );
Gia_ManResubPrintLit( vRes, nVars, iTopLit );
return 0;
}
/**Function*************************************************************
Synopsis [Verify resubstitution.]
@ -365,54 +433,54 @@ void Gia_ResbFree( Gia_ResbMan_t * p )
SeeAlso []
***********************************************************************/
int Gia_ManResubVerify( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates, int iTopLit )
int Gia_ManResubVerify( Gia_ResbMan_t * p )
{
int i, iLit0, iLit1, RetValue, nDivs = Vec_PtrSize(vDivs);
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int nVars = Vec_PtrSize(p->vDivs);
int iTopLit, RetValue;
word * pDivRes;
Vec_Wrd_t * vSims = NULL;
if ( iTopLit <= -1 )
if ( Vec_IntSize(p->vGates) == 0 )
return -1;
iTopLit = Vec_IntEntryLast(p->vGates);
assert( iTopLit >= 0 );
if ( iTopLit == 0 )
return Abc_TtIsConst0( pOnSet, nWords );
return Abc_TtIsConst0( p->pSets[1], p->nWords );
if ( iTopLit == 1 )
return Abc_TtIsConst0( pOffSet, nWords );
if ( Abc_Lit2Var(iTopLit) < nDivs )
return Abc_TtIsConst0( p->pSets[0], p->nWords );
if ( Abc_Lit2Var(iTopLit) < nVars )
{
assert( Vec_IntSize(vGates) == 0 );
pDivRes = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iTopLit) );
assert( Vec_IntSize(p->vGates) == 1 );
pDivRes = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iTopLit) );
}
else
{
assert( Vec_IntSize(vGates) > 0 );
assert( Vec_IntSize(vGates) % 2 == 0 );
assert( Abc_Lit2Var(iTopLit)-nDivs == Vec_IntSize(vGates)/2-1 );
vSims = Vec_WrdStart( nWords * Vec_IntSize(vGates)/2 );
Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i )
int i, iLit0, iLit1;
assert( Vec_IntSize(p->vGates) > 1 );
assert( Vec_IntSize(p->vGates) % 2 == 1 );
assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(p->vGates)/2-1 );
Vec_WrdFill( p->vSims, p->nWords * Vec_IntSize(p->vGates)/2, 0 );
Vec_IntForEachEntryDouble( p->vGates, iLit0, iLit1, i )
{
int iVar0 = Abc_Lit2Var(iLit0);
int iVar1 = Abc_Lit2Var(iLit1);
word * pDiv0 = iVar0 < nDivs ? (word *)Vec_PtrEntry(vDivs, iVar0) : Vec_WrdEntryP(vSims, nWords*(nDivs - iVar0));
word * pDiv1 = iVar1 < nDivs ? (word *)Vec_PtrEntry(vDivs, iVar1) : Vec_WrdEntryP(vSims, nWords*(nDivs - iVar1));
word * pDiv = Vec_WrdEntryP(vSims, nWords*i/2);
word * pDiv0 = iVar0 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar0) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar0 - nVars));
word * pDiv1 = iVar1 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar1) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar1 - nVars));
word * pDiv = Vec_WrdEntryP(p->vSims, p->nWords*i/2);
if ( iVar0 < iVar1 )
Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords );
Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), p->nWords );
else if ( iVar0 > iVar1 )
{
assert( !Abc_LitIsCompl(iLit0) );
assert( !Abc_LitIsCompl(iLit1) );
Abc_TtXor( pDiv, pDiv0, pDiv1, nWords, 0 );
Abc_TtXor( pDiv, pDiv0, pDiv1, p->nWords, 0 );
}
else assert( 0 );
}
pDivRes = Vec_WrdEntryP( vSims, nWords*(Vec_IntSize(vGates)/2-1) );
pDivRes = Vec_WrdEntryP( p->vSims, p->nWords*(Vec_IntSize(p->vGates)/2-1) );
}
if ( Abc_LitIsCompl(iTopLit) )
RetValue = !Abc_TtIntersectOne(pOnSet, 0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 1, nWords);
RetValue = !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 1, p->nWords);
else
RetValue = !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOnSet, 0, pDivRes, 1, nWords);
Vec_WrdFreeP( &vSims );
RetValue = !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 1, p->nWords);
return RetValue;
}
@ -433,32 +501,36 @@ int Gia_ManGetVar( Gia_Man_t * pNew, Vec_Int_t * vUsed, int iVar )
Vec_IntWriteEntry( vUsed, iVar, Gia_ManAppendCi(pNew) );
return Vec_IntEntry(vUsed, iVar);
}
Gia_Man_t * Gia_ManConstructFromGates( int nVars, Vec_Int_t * vGates, int iTopLit )
Gia_Man_t * Gia_ManConstructFromGates( Vec_Int_t * vGates, int nVars )
{
int i, iLit0, iLit1, iLitRes;
Gia_Man_t * pNew = Gia_ManStart( 100 );
int i, iLit0, iLit1, iTopLit, iLitRes;
Gia_Man_t * pNew;
if ( Vec_IntSize(vGates) == 0 )
return NULL;
assert( Vec_IntSize(vGates) % 2 == 1 );
pNew = Gia_ManStart( 100 );
pNew->pName = Abc_UtilStrsav( "resub" );
assert( iTopLit >= 0 );
iTopLit = Vec_IntEntryLast( vGates );
if ( iTopLit == 0 || iTopLit == 1 )
iLitRes = 0;
else if ( Abc_Lit2Var(iTopLit) < nVars )
{
assert( Vec_IntSize(vGates) == 0 );
assert( Vec_IntSize(vGates) == 1 );
iLitRes = Gia_ManAppendCi(pNew);
}
else
{
Vec_Int_t * vUsed = Vec_IntStartFull( nVars );
Vec_Int_t * vCopy = Vec_IntAlloc( Vec_IntSize(vGates)/2 );
assert( Vec_IntSize(vGates) > 0 );
assert( Vec_IntSize(vGates) % 2 == 0 );
assert( Vec_IntSize(vGates) > 1 );
assert( Vec_IntSize(vGates) % 2 == 1 );
assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(vGates)/2-1 );
Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i )
{
int iVar0 = Abc_Lit2Var(iLit0);
int iVar1 = Abc_Lit2Var(iLit1);
int iRes0 = iVar0 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar0) : Vec_IntEntry(vCopy, nVars - iVar0);
int iRes1 = iVar1 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar1) : Vec_IntEntry(vCopy, nVars - iVar1);
int iRes0 = iVar0 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar0) : Vec_IntEntry(vCopy, iVar0 - nVars);
int iRes1 = iVar1 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar1) : Vec_IntEntry(vCopy, iVar1 - nVars);
if ( iVar0 < iVar1 )
iLitRes = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) );
else if ( iVar0 > iVar1 )
@ -491,7 +563,7 @@ Gia_Man_t * Gia_ManConstructFromGates( int nVars, Vec_Int_t * vGates, int iTopLi
SeeAlso []
***********************************************************************/
static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2, int fVerbose )
{
int * pBeg1 = vArr1->pArray;
int * pBeg2 = vArr2->pArray;
@ -521,7 +593,7 @@ static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr
*pStart2++ = *pBeg2++;
Vec_IntShrink( vArr1, pStart1 - vArr1->pArray );
Vec_IntShrink( vArr2, pStart2 - vArr2->pArray );
printf( "Removed %d duplicated entries. Array1 = %d. Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) );
if ( fVerbose ) printf( "Removed %d duplicated entries. Array1 = %d. Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) );
return -1;
}
@ -538,20 +610,17 @@ void Gia_ManFindOneUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, i
else
Vec_IntPush( vNotUnateVars, i );
}
int Gia_ManFindOneUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2] )
int Gia_ManFindOneUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2], int fVerbose )
{
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int n;
for ( n = 0; n < 2; n++ )
{
Vec_IntClear( vUnateLits[n] );
Vec_IntClear( vNotUnateVars[n] );
Gia_ManFindOneUnateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vNotUnateVars[n] );
ABC_SWAP( word *, pOffSet, pOnSet );
printf( "Found %d %d-unate divs.\n", Vec_IntSize(vUnateLits[n]), n );
Gia_ManFindOneUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vNotUnateVars[n] );
if ( fVerbose ) printf( "Found %d %d-unate divs.\n", Vec_IntSize(vUnateLits[n]), n );
}
return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1], fVerbose );
}
static inline int Gia_ManDivCover( word * pOffSet, word * pOnSet, word * pDivA, int ComplA, word * pDivB, int ComplB, int nWords )
@ -568,61 +637,54 @@ int Gia_ManFindTwoUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, in
{
word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1));
if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords) )
return Abc_Var2Lit((Abc_LitNot(iDiv0) << 16) | Abc_LitNot(iDiv1), 0);
if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv1, Abc_LitIsCompl(iDiv1), pDiv0, Abc_LitIsCompl(iDiv0), nWords) )
return Abc_Var2Lit((Abc_LitNot(iDiv1) << 15) | Abc_LitNot(iDiv0), 1);
}
return -1;
}
int Gia_ManFindTwoUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2] )
int Gia_ManFindTwoUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], int fVerbose )
{
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int n, iLit;
for ( n = 0; n < 2; n++ )
{
printf( "Trying %d pairs of %d-unate divs.\n", Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2, n );
iLit = Gia_ManFindTwoUnateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n] );
int nPairs = Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2;
if ( fVerbose ) printf( "Trying %d pairs of %d-unate divs.\n", nPairs, n );
iLit = Gia_ManFindTwoUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n] );
if ( iLit >= 0 )
return Abc_LitNotCond(iLit, !n);
ABC_SWAP( word *, pOffSet, pOnSet );
return Abc_LitNotCond(iLit, n);
}
return -1;
}
void Gia_ManFindXorInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits )
void Gia_ManFindXorInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs )
{
int i, k, iDiv0, iDiv1;
Vec_IntClear( vUnateLits );
Vec_IntForEachEntry( vBinate, iDiv1, i )
Vec_IntForEachEntryStop( vBinate, iDiv0, k, i )
{
word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0);
word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1);
if ( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 0, nWords ) )
Vec_IntPush( vUnateLits, Abc_Var2Lit((Abc_Var2Lit(iDiv1, 0) << 16) | Abc_Var2Lit(iDiv0, 0), 0) );
Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 0) );
else if ( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 1, nWords ) )
Vec_IntPush( vUnateLits, Abc_Var2Lit((Abc_Var2Lit(iDiv1, 0) << 16) | Abc_Var2Lit(iDiv0, 0), 1) );
Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 1) );
}
}
int Gia_ManFindXor( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] )
int Gia_ManFindXor( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose )
{
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int n;
for ( n = 0; n < 2; n++ )
{
Vec_IntClear( vUnateLits[n] );
Gia_ManFindXorInt( pOffSet, pOnSet, vBinateVars, vDivs, nWords, vUnateLits[n] );
ABC_SWAP( word *, pOffSet, pOnSet );
printf( "Found %d %d-unate XOR divs.\n", Vec_IntSize(vUnateLits[n]), n );
Vec_IntClear( vUnatePairs[n] );
Gia_ManFindXorInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] );
if ( fVerbose ) printf( "Found %d %d-unate XOR divs.\n", Vec_IntSize(vUnatePairs[n]), n );
}
return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
return Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose );
}
void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits )
void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs )
{
int n, i, k, iDiv0, iDiv1;
Vec_IntClear( vUnateLits );
Vec_IntForEachEntry( vBinate, iDiv1, i )
Vec_IntForEachEntryStop( vBinate, iDiv0, k, i )
{
@ -632,56 +694,67 @@ void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinat
{
int iLit0 = Abc_Var2Lit( iDiv0, n&1 );
int iLit1 = Abc_Var2Lit( iDiv1, n>>1 );
if ( !Abc_TtIntersectTwo( pOffSet, 0, pDiv0, n&1, pDiv1, n>>1, nWords ) )
Vec_IntPush( vUnateLits, Abc_Var2Lit((iLit0 << 16) | iLit1, 0) );
if ( !Abc_TtIntersectTwo( pOffSet, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) )
Vec_IntPush( vUnatePairs, Abc_Var2Lit((iLit1 << 15) | iLit0, 0) );
}
}
}
void Gia_ManFindUnatePairs( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] )
void Gia_ManFindUnatePairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose )
{
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int n, RetValue;
for ( n = 0; n < 2; n++ )
{
int nBefore = Vec_IntSize(vUnateLits[n]);
Gia_ManFindUnatePairsInt( pOffSet, pOnSet, vBinateVars, vDivs, nWords, vUnateLits[n] );
ABC_SWAP( word *, pOffSet, pOnSet );
printf( "Found %d %d-unate pair divs.\n", Vec_IntSize(vUnateLits[n])-nBefore, n );
int nBefore = Vec_IntSize(vUnatePairs[n]);
Gia_ManFindUnatePairsInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] );
if ( fVerbose ) printf( "Found %d %d-unate pair divs.\n", Vec_IntSize(vUnatePairs[n])-nBefore, n );
}
RetValue = Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] );
RetValue = Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose );
assert( RetValue == -1 );
}
int Gia_ManFindAndGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, word * pDivTemp )
void Gia_ManDeriveDivPair( int iDiv, Vec_Ptr_t * vDivs, int nWords, word * pRes )
{
int fComp = Abc_LitIsCompl(iDiv);
int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF;
int iDiv1 = Abc_Lit2Var(iDiv) >> 15;
word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1));
if ( iDiv0 < iDiv1 )
{
assert( !fComp );
Abc_TtAndCompl( pRes, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords );
}
else
{
assert( !Abc_LitIsCompl(iDiv0) );
assert( !Abc_LitIsCompl(iDiv1) );
Abc_TtXor( pRes, pDiv0, pDiv1, nWords, 0 );
}
}
int Gia_ManFindDivGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, word * pDivTemp )
{
int i, k, iDiv0, iDiv1;
Vec_IntForEachEntry( vUnateLits, iDiv0, i )
Vec_IntForEachEntry( vUnatePairs, iDiv1, k )
int Limit1 = Abc_MinInt( Vec_IntSize(vUnateLits), 1000 );
int Limit2 = Abc_MinInt( Vec_IntSize(vUnatePairs), 1000 );
Vec_IntForEachEntryStop( vUnateLits, iDiv0, i, Limit1 )
Vec_IntForEachEntryStop( vUnatePairs, iDiv1, k, Limit2 )
{
int fCompl = Abc_LitIsCompl(iDiv1);
int iDiv10 = Abc_Lit2Var(iDiv1) >> 16;
int iDiv11 = Abc_Lit2Var(iDiv1) & 0xFFF;
word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
word * pDiv10 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv10));
word * pDiv11 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv11));
Abc_TtAndCompl( pDivTemp, pDiv10, Abc_LitIsCompl(iDiv10), pDiv11, Abc_LitIsCompl(iDiv11), nWords );
if ( Gia_ManDivCover(pOnSet, pOffSet, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fCompl, nWords) )
return Abc_Var2Lit((Abc_LitNot(iDiv0) << 16) | Abc_Var2Lit(k, 1), 0);
word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0));
int fComp1 = Abc_LitIsCompl(iDiv1);
Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTemp );
if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fComp1, nWords) )
return Abc_Var2Lit((Abc_Var2Lit(k, 1) << 15) | Abc_LitNot(iDiv0), 1);
}
return -1;
}
int Gia_ManFindAndGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], word * pDivTemp )
int Gia_ManFindDivGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], word * pDivTemp )
{
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int n, iLit;
for ( n = 0; n < 2; n++ )
{
iLit = Gia_ManFindAndGateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vUnatePairs[n], pDivTemp );
if ( iLit > 0 )
return Abc_LitNotCond( iLit, !n );
ABC_SWAP( word *, pOffSet, pOnSet );
iLit = Gia_ManFindDivGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnatePairs[n], pDivTemp );
if ( iLit >= 0 )
return Abc_LitNotCond( iLit, n );
}
return -1;
}
@ -689,39 +762,29 @@ int Gia_ManFindAndGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2]
int Gia_ManFindGateGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, word * pDivTempA, word * pDivTempB )
{
int i, k, iDiv0, iDiv1;
Vec_IntForEachEntry( vUnatePairs, iDiv0, i )
int Limit2 = Abc_MinInt( Vec_IntSize(vUnatePairs), 1000 );
Vec_IntForEachEntryStop( vUnatePairs, iDiv1, i, Limit2 )
{
int fCompA = Abc_LitIsCompl(iDiv0);
int iDiv00 = Abc_Lit2Var(iDiv0 >> 16);
int iDiv01 = Abc_Lit2Var(iDiv0 & 0xFFF);
word * pDiv00 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv00));
word * pDiv01 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv01));
Abc_TtAndCompl( pDivTempA, pDiv00, Abc_LitIsCompl(iDiv00), pDiv01, Abc_LitIsCompl(iDiv01), nWords );
Vec_IntForEachEntryStop( vUnatePairs, iDiv1, k, i )
int fCompB = Abc_LitIsCompl(iDiv1);
Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTempB );
Vec_IntForEachEntryStop( vUnatePairs, iDiv0, k, i )
{
int fCompB = Abc_LitIsCompl(iDiv1);
int iDiv10 = Abc_Lit2Var(iDiv1 >> 16);
int iDiv11 = Abc_Lit2Var(iDiv1 & 0xFFF);
word * pDiv10 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv10));
word * pDiv11 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv11));
Abc_TtAndCompl( pDivTempB, pDiv10, Abc_LitIsCompl(iDiv10), pDiv11, Abc_LitIsCompl(iDiv11), nWords );
if ( Gia_ManDivCover(pOnSet, pOffSet, pDivTempA, fCompA, pDivTempB, fCompB, nWords) )
return Abc_Var2Lit((iDiv1 << 16) | iDiv0, 0);
int fCompA = Abc_LitIsCompl(iDiv0);
Gia_ManDeriveDivPair( iDiv0, vDivs, nWords, pDivTempA );
if ( Gia_ManDivCover(pOffSet, pOnSet, pDivTempA, fCompA, pDivTempB, fCompB, nWords) )
return Abc_Var2Lit((Abc_Var2Lit(i, 1) << 15) | Abc_Var2Lit(k, 1), 1);
}
}
return -1;
}
int Gia_ManFindGateGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], word * pDivTempA, word * pDivTempB )
int Gia_ManFindGateGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], word * pDivTempA, word * pDivTempB )
{
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int n, iLit;
for ( n = 0; n < 2; n++ )
{
iLit = Gia_ManFindGateGateInt( pOffSet, pOnSet, vDivs, nWords, vUnatePairs[n], pDivTempA, pDivTempB );
ABC_SWAP( word *, pOffSet, pOnSet );
if ( iLit > 0 )
return iLit;
iLit = Gia_ManFindGateGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], pDivTempA, pDivTempB );
if ( iLit >= 0 )
return Abc_LitNotCond( iLit, n );
}
return -1;
}
@ -734,33 +797,36 @@ void Gia_ManComputeLitWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDi
{
word * pDiv = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit) );
assert( !Abc_TtIntersectOne( pOffSet, 0, pDiv, Abc_LitIsCompl(iLit), nWords ) );
Vec_IntPush( vUnateLitsW, Abc_TtCountOnesVecMask(pDiv, pOnSet, nWords, Abc_LitIsCompl(iLit)) );
Vec_IntPush( vUnateLitsW, -Abc_TtCountOnesVecMask(pDiv, pOnSet, nWords, Abc_LitIsCompl(iLit)) );
}
}
void Gia_ManComputeLitWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2] )
void Gia_ManComputeLitWeights( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], int TopW[2], int fVerbose )
{
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int n;
int n, TopNum = 5;
TopW[0] = TopW[1] = 0;
for ( n = 0; n < 2; n++ )
{
Vec_IntClear( vUnateLitsW[n] );
Gia_ManComputeLitWeightsInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vUnateLitsW[n] );
ABC_SWAP( word *, pOffSet, pOnSet );
}
Gia_ManComputeLitWeightsInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n] );
for ( n = 0; n < 2; n++ )
{
int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnateLitsW[n]), Vec_IntSize(vUnateLitsW[n]) );
Abc_ReverseOrder( pPerm, Vec_IntSize(vUnateLitsW[n]) );
printf( "Top 10 %d-unate:\n", n );
for ( i = 0; i < 10 && i < Vec_IntSize(vUnateLits[n]); i++ )
if ( Vec_IntSize(vUnateLitsW[n]) )
{
printf( "%5d : ", i );
printf( "Obj = %5d ", Vec_IntEntry(vUnateLits[n], pPerm[i]) );
printf( "Cost = %5d\n", Vec_IntEntry(vUnateLitsW[n], pPerm[i]) );
int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnateLitsW[n]), Vec_IntSize(vUnateLitsW[n]) );
TopW[n] = -Vec_IntEntry(vUnateLitsW[n], pPerm[0]);
if ( fVerbose )
{
printf( "Top %d %d-unate divs:\n", TopNum, n );
for ( i = 0; i < TopNum && i < Vec_IntSize(vUnateLits[n]); i++ )
{
printf( "%5d : ", i );
printf( "Lit = %5d ", Vec_IntEntry(vUnateLits[n], pPerm[i]) );
printf( "Cost = %5d\n", -Vec_IntEntry(vUnateLitsW[n], pPerm[i]) );
}
}
for ( i = 0; i < Vec_IntSize(vUnateLits[n]); i++ )
pPerm[i] = Vec_IntEntry(vUnateLits[n], pPerm[i]);
for ( i = 0; i < Vec_IntSize(vUnateLits[n]); i++ )
vUnateLits[n]->pArray[i] = pPerm[i];
ABC_FREE( pPerm );
}
ABC_FREE( pPerm );
}
}
void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW )
@ -769,50 +835,59 @@ void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vD
Vec_IntClear( vUnatePairsW );
Vec_IntForEachEntry( vUnatePairs, iPair, i )
{
int fCompl = Abc_LitIsCompl(iPair);
int Pair = Abc_Lit2Var(iPair);
int iLit0 = Pair >> 16;
int iLit1 = Pair & 0xFFFF;
int fComp = Abc_LitIsCompl(iPair);
int iLit0 = Abc_Lit2Var(iPair) & 0x7FFF;
int iLit1 = Abc_Lit2Var(iPair) >> 15;
word * pDiv0 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit0) );
word * pDiv1 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit1) );
if ( iLit0 < iLit1 )
{
assert( !fCompl );
assert( !fComp );
assert( !Abc_TtIntersectTwo( pOffSet, 0, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ) );
Vec_IntPush( vUnatePairsW, Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOnSet, nWords) );
Vec_IntPush( vUnatePairsW, -Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOnSet, nWords) );
}
else
{
assert( !Abc_LitIsCompl(iLit0) );
assert( !Abc_LitIsCompl(iLit1) );
assert( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 0, nWords ) );
Vec_IntPush( vUnatePairsW, Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fCompl, pOnSet, nWords) );
assert( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, fComp, nWords ) );
Vec_IntPush( vUnatePairsW, -Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fComp, pOnSet, nWords) );
}
}
}
void Gia_ManComputePairWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2] )
void Gia_ManComputePairWeights( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2], int TopW[2], int fVerbose )
{
word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 );
word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 );
int n;
int n, TopNum = 5;
TopW[0] = TopW[1] = 0;
for ( n = 0; n < 2; n++ )
{
Gia_ManComputePairWeightsInt( pOffSet, pOnSet, vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] );
ABC_SWAP( word *, pOffSet, pOnSet );
}
Gia_ManComputePairWeightsInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] );
for ( n = 0; n < 2; n++ )
{
int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnatePairsW[n]), Vec_IntSize(vUnatePairsW[n]) );
Abc_ReverseOrder( pPerm, Vec_IntSize(vUnatePairsW[n]) );
printf( "Top 10 %d-unate:\n", n );
for ( i = 0; i < 10 && i < Vec_IntSize(vUnatePairs[n]); i++ )
if ( Vec_IntSize(vUnatePairsW[n]) )
{
printf( "%5d : ", i );
printf( "Obj = %5d ", Vec_IntEntry(vUnatePairs[n], pPerm[i]) );
printf( "Cost = %5d\n", Vec_IntEntry(vUnatePairsW[n], pPerm[i]) );
int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnatePairsW[n]), Vec_IntSize(vUnatePairsW[n]) );
TopW[n] = -Vec_IntEntry(vUnatePairsW[n], pPerm[0]);
if ( fVerbose )
{
printf( "Top %d %d-unate pairs:\n", TopNum, n );
for ( i = 0; i < TopNum && i < Vec_IntSize(vUnatePairs[n]); i++ )
{
int Pair = Vec_IntEntry(vUnatePairs[n], pPerm[i]);
int Div0 = Abc_Lit2Var(Pair) & 0x7FFF;
int Div1 = Abc_Lit2Var(Pair) >> 15;
printf( "%5d : ", i );
printf( "Compl = %5d ", Abc_LitIsCompl(Pair) );
printf( "Type = %s ", Div0 < Div1 ? "and" : "xor" );
printf( "Div0 = %5d ", Div0 );
printf( "Div1 = %5d ", Div1 );
printf( "Cost = %5d\n", -Vec_IntEntry(vUnatePairsW[n], pPerm[i]) );
}
}
for ( i = 0; i < Vec_IntSize(vUnatePairs[n]); i++ )
pPerm[i] = Vec_IntEntry(vUnatePairs[n], pPerm[i]);
for ( i = 0; i < Vec_IntSize(vUnatePairs[n]); i++ )
vUnatePairs[n]->pArray[i] = pPerm[i];
ABC_FREE( pPerm );
}
ABC_FREE( pPerm );
}
}
@ -827,28 +902,32 @@ void Gia_ManComputePairWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnat
SeeAlso []
***********************************************************************/
int Gia_ManResubInt2( Vec_Ptr_t * vDivs, int nWords, int NodeLimit, int ChoiceType, Vec_Int_t * vGates )
int Gia_ManResubPerformInt( Gia_ResbMan_t * p )
{
return 0;
}
int Gia_ManResubInt( Gia_ResbMan_t * p )
{
int nDivs = Vec_PtrSize(p->vDivs);
int iResLit = Gia_ManFindOneUnate( p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars );
if ( iResLit >= 0 ) // buffer
int TopOneW[2], TopTwoW[2], Max, iResLit, nVars = Vec_PtrSize(p->vDivs);
if ( p->fVerbose )
{
printf( "Creating %s (%d).\n", Abc_LitIsCompl(iResLit) ? "inverter" : "buffer", Abc_Lit2Var(iResLit) );
return iResLit;
printf( "\nCalling decomposition for ISF: " );
printf( "OFF = %5d (%6.2f %%) ", Abc_TtCountOnesVec(p->pSets[0], p->nWords), 100.0*Abc_TtCountOnesVec(p->pSets[0], p->nWords)/(64*p->nWords) );
printf( "ON = %5d (%6.2f %%)\n", Abc_TtCountOnesVec(p->pSets[1], p->nWords), 100.0*Abc_TtCountOnesVec(p->pSets[1], p->nWords)/(64*p->nWords) );
}
iResLit = Gia_ManFindTwoUnate( p->vDivs, p->nWords, p->vUnateLits );
if ( Abc_TtIsConst0( p->pSets[1], p->nWords ) )
return 0;
if ( Abc_TtIsConst0( p->pSets[0], p->nWords ) )
return 1;
iResLit = Gia_ManFindOneUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars, p->fVerbose );
if ( iResLit >= 0 ) // buffer
return iResLit;
iResLit = Gia_ManFindTwoUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->fVerbose );
if ( iResLit >= 0 ) // and
{
int fCompl = Abc_LitIsCompl(iResLit);
int iDiv0 = Abc_Lit2Var(iResLit) >> 16;
int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF;
int iNode = nVars + Vec_IntSize(p->vGates)/2;
int fComp = Abc_LitIsCompl(iResLit);
int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF;
int iDiv1 = Abc_Lit2Var(iResLit) >> 15;
assert( iDiv0 < iDiv1 );
Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 );
printf( "Creating one AND-gate.\n" );
return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, fCompl );
return Abc_Var2Lit( iNode, fComp );
}
Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars );
if ( Vec_IntSize(p->vBinateVars) > 1000 )
@ -856,43 +935,181 @@ int Gia_ManResubInt( Gia_ResbMan_t * p )
printf( "Reducing binate divs from %d to 1000.\n", Vec_IntSize(p->vBinateVars) );
Vec_IntShrink( p->vBinateVars, 1000 );
}
iResLit = Gia_ManFindXor( p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs );
iResLit = Gia_ManFindXor( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose );
if ( iResLit >= 0 ) // xor
{
int fCompl = Abc_LitIsCompl(iResLit);
int iDiv0 = Abc_Lit2Var(iResLit) >> 16;
int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF;
int iNode = nVars + Vec_IntSize(p->vGates)/2;
int fComp = Abc_LitIsCompl(iResLit);
int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF;
int iDiv1 = Abc_Lit2Var(iResLit) >> 15;
assert( !Abc_LitIsCompl(iDiv0) );
assert( !Abc_LitIsCompl(iDiv1) );
Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); // xor
printf( "Creating one XOR-gate.\n" );
return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, fCompl );
assert( iDiv0 > iDiv1 );
Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 );
return Abc_Var2Lit( iNode, fComp );
}
Gia_ManFindUnatePairs( p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs );
/*
iResLit = Gia_ManFindAndGate( p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->pDivA );
if ( iResLit >= 0 ) // and-gate
Gia_ManFindUnatePairs( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose );
iResLit = Gia_ManFindDivGate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->pDivA );
if ( iResLit >= 0 ) // and(div,pair)
{
int New = nDivs + Vec_IntSize(p->vGates)/2;
int fCompl = Abc_LitIsCompl(iResLit);
int iDiv0 = Abc_Lit2Var(iResLit) >> 16;
int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF;
Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv1), Abc_LitNot(iDiv0) );
Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv0), New );
printf( "Creating one two gates.\n" );
return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, 1 );
int iNode = nVars + Vec_IntSize(p->vGates)/2;
int fComp = Abc_LitIsCompl(iResLit);
int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // div
int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair
int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) );
int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1);
int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF;
int iDiv11 = Abc_Lit2Var(Div1) >> 15;
Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 );
Vec_IntPushTwo( p->vGates, iDiv0, Abc_Var2Lit(iNode, fComp1) );
return Abc_Var2Lit( iNode+1, fComp );
}
iResLit = Gia_ManFindGateGate( p->vDivs, p->nWords, p->vUnatePairs, p->pDivA, p->pDivB );
if ( iResLit >= 0 ) // and-(gate,gate)
iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->pDivA, p->pDivB );
if ( iResLit >= 0 ) // and(pair,pair)
{
printf( "Creating one three gates.\n" );
int iNode = nVars + Vec_IntSize(p->vGates)/2;
int fComp = Abc_LitIsCompl(iResLit);
int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // pair
int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair
int Div0 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv0) );
int fComp0 = Abc_LitIsCompl(Div0) ^ Abc_LitIsCompl(iDiv0);
int iDiv00 = Abc_Lit2Var(Div0) & 0x7FFF;
int iDiv01 = Abc_Lit2Var(Div0) >> 15;
int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) );
int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1);
int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF;
int iDiv11 = Abc_Lit2Var(Div1) >> 15;
Vec_IntPushTwo( p->vGates, iDiv00, iDiv01 );
Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 );
Vec_IntPushTwo( p->vGates, Abc_Var2Lit(iNode, fComp0), Abc_Var2Lit(iNode+1, fComp1) );
return Abc_Var2Lit( iNode+2, fComp );
}
if ( Vec_IntSize(p->vUnateLits[0]) + Vec_IntSize(p->vUnateLits[1]) + Vec_IntSize(p->vUnatePairs[0]) + Vec_IntSize(p->vUnatePairs[1]) == 0 )
return -1;
Gia_ManComputeLitWeights( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, TopOneW, p->fVerbose );
Gia_ManComputePairWeights( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, TopTwoW, p->fVerbose );
//Max = Abc_MaxInt( Abc_MaxInt(TopOneW[0], TopOneW[1]), Abc_MaxInt(TopTwoW[0], TopTwoW[1]) );
Max = Abc_MaxInt(TopOneW[0], TopOneW[1]);
if ( Max == 0 )
return -1;
if ( Max == TopOneW[0] || Max == TopOneW[1] )
{
int fUseOr = Max == TopOneW[0];
int iDiv = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 );
int fComp = Abc_LitIsCompl(iDiv);
word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) );
Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp );
iResLit = Gia_ManResubPerformInt( p );
if ( iResLit >= 0 )
{
int iNode = nVars + Vec_IntSize(p->vGates)/2;
Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) );
return Abc_Var2Lit( iNode, fUseOr );
}
}
if ( Max == TopTwoW[0] || Max == TopTwoW[1] )
{
int fUseOr = Max == TopTwoW[0];
int iDiv = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 );
int fComp = Abc_LitIsCompl(iDiv);
Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA );
Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp );
iResLit = Gia_ManResubPerformInt( p );
if ( iResLit >= 0 )
{
int iNode = nVars + Vec_IntSize(p->vGates)/2;
int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF;
int iDiv1 = Abc_Lit2Var(iDiv) >> 15;
Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 );
Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) );
return Abc_Var2Lit( iNode+1, fUseOr );
}
}
*/
Gia_ManComputeLitWeights( p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW );
Gia_ManComputePairWeights( p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW );
return -1;
}
void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vRes, int fVerbose )
{
int Res;
Vec_IntClear( vRes );
Gia_ResbInit( p, vDivs, nWords, vRes, fVerbose );
Res = Gia_ManResubPerformInt( p );
if ( Res == -1 )
{
printf( "\n" );
return;
}
Vec_IntPush( vRes, Res );
Gia_ManResubPrint( vRes, Vec_PtrSize(vDivs) );
printf( " Verification %s.\n", Gia_ManResubVerify(p) ? "succeeded" : "FAILED *******************************" );
}
void Gia_ManResubTest3()
{
int nVars = 3;
Gia_ResbMan_t * p = Gia_ResbAlloc( 1 );
word Divs[6] = { 0, 0,
ABC_CONST(0xAAAAAAAAAAAAAAAA),
ABC_CONST(0xCCCCCCCCCCCCCCCC),
ABC_CONST(0xF0F0F0F0F0F0F0F0),
ABC_CONST(0xFF00FF00FF00FF00)
};
Vec_Ptr_t * vDivs = Vec_PtrAlloc( 6 );
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
int i;
for ( i = 0; i < 6; i++ )
Vec_PtrPush( vDivs, Divs+i );
for ( i = 0; i < (1<<(1<<nVars)); i++ )
{
word Truth = Abc_Tt6Stretch( i, nVars );
Divs[0] = ~Truth;
Divs[1] = Truth;
printf( "%3d : ", i );
Extra_PrintHex( stdout, (unsigned*)&Truth, nVars );
printf( " " );
Dau_DsdPrintFromTruth2( (unsigned*)&Truth, nVars );
printf( " " );
Gia_ManResubPerform( p, vDivs, 1, vRes, 0 );
}
Gia_ResbFree( p );
Vec_IntFree( vRes );
Vec_PtrFree( vDivs );
}
void Gia_ManResubTest3_()
{
Gia_ResbMan_t * p = Gia_ResbAlloc( 1 );
word Divs[6] = { 0, 0,
ABC_CONST(0xAAAAAAAAAAAAAAAA),
ABC_CONST(0xCCCCCCCCCCCCCCCC),
ABC_CONST(0xF0F0F0F0F0F0F0F0),
ABC_CONST(0xFF00FF00FF00FF00)
};
Vec_Ptr_t * vDivs = Vec_PtrAlloc( 6 );
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
int i;
for ( i = 0; i < 6; i++ )
Vec_PtrPush( vDivs, Divs+i );
{
word Truth = (Divs[2] | Divs[3]) & (Divs[4] & Divs[5]);
// word Truth = (~Divs[2] | Divs[3]) | ~Divs[4];
Divs[0] = ~Truth;
Divs[1] = Truth;
Extra_PrintHex( stdout, (unsigned*)&Truth, 6 );
printf( " " );
Dau_DsdPrintFromTruth2( (unsigned*)&Truth, 6 );
printf( " " );
Gia_ManResubPerform( p, vDivs, 1, vRes, 0 );
}
Gia_ResbFree( p );
Vec_IntFree( vRes );
Vec_PtrFree( vDivs );
}
/**Function*************************************************************
@ -942,30 +1159,22 @@ Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, i
}
Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose )
{
int iTopLit, nWords = 0;
int nWords = 0;
Gia_Man_t * pMan = NULL;
Vec_Wrd_t * vSims = Gia_ManSimPatRead( pFileName, &nWords );
Vec_Ptr_t * vDivs = vSims ? Gia_ManDeriveDivs( vSims, nWords ) : NULL;
Vec_Int_t * vGates = vDivs ? Vec_IntAlloc( 100 ) : NULL;
Gia_ResbMan_t * p = vDivs ? Gia_ResbAlloc( vDivs, nWords, vGates ) : NULL;
if ( p == NULL )
return NULL;
assert( Vec_PtrSize(vDivs) < (1<<15) );
printf( "OFF = %5d (%6.2f %%) ", Abc_TtCountOnesVec((word *)Vec_PtrEntry(vDivs, 0), nWords), 100.0*Abc_TtCountOnesVec((word *)Vec_PtrEntry(vDivs, 0), nWords)/(64*nWords) );
printf( "ON = %5d (%6.2f %%)\n", Abc_TtCountOnesVec((word *)Vec_PtrEntry(vDivs, 1), nWords), 100.0*Abc_TtCountOnesVec((word *)Vec_PtrEntry(vDivs, 1), nWords)/(64*nWords) );
if ( Vec_PtrSize(vDivs) > 4000 )
{
printf( "Reducing all divs from %d to 4000.\n", Vec_PtrSize(vDivs) );
Vec_PtrShrink( vDivs, 4000 );
}
Gia_ResbReset( p );
Gia_ResbMan_t * p = Gia_ResbAlloc( nWords );
// Gia_ManCheckResub( vDivs, nWords );
iTopLit = Gia_ManResubInt( p );
if ( iTopLit >= 0 )
if ( Vec_PtrSize(vDivs) >= (1<<14) )
{
printf( "Verification %s.\n", Gia_ManResubVerify( vDivs, nWords, vGates, iTopLit ) ? "succeeded" : "FAILED" );
pMan = Gia_ManConstructFromGates( Vec_PtrSize(vDivs), vGates, iTopLit );
printf( "Reducing all divs from %d to %d.\n", Vec_PtrSize(vDivs), (1<<14)-1 );
Vec_PtrShrink( vDivs, (1<<14)-1 );
}
assert( Vec_PtrSize(vDivs) < (1<<14) );
Gia_ManResubPerform( p, vDivs, nWords, vGates, 1 );
if ( Vec_IntSize(vGates) )
pMan = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) );
else
printf( "Decomposition did not succeed.\n" );
Gia_ResbFree( p );

8
src/opt/dau/dauDsd.c
View File

@ -1973,6 +1973,14 @@ void Dau_DsdPrintFromTruth( word * pTruth, int nVarsInit )
Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
fprintf( stdout, "%s\n", pRes );
}
void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit )
{
char pRes[DAU_MAX_STR];
word pTemp[DAU_MAX_WORD];
Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
fprintf( stdout, "%s", pRes );
}
void Dau_DsdTest44()
{