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

Changes to enable decomposition of non-DSD functions.

This commit is contained in:
Alan Mishchenko 2013-09-25 13:18:21 -07:00
parent cab8301065
commit ee11ee1833
6 changed files with 179 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/gia/gia.h
View File

@ -1227,6 +1227,7 @@ extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManPrint( Gia_Man_t * p );
extern void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeaves, Vec_Int_t * vNodes );
extern void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj );
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
extern void Gia_ManInvertPos( Gia_Man_t * pAig );
extern int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );

23
src/aig/gia/giaUtil.c
View File

@ -1194,6 +1194,7 @@ void Gia_ManPrintCo( Gia_Man_t * p, Gia_Obj_t * pObj )
Gia_ManPrintCo_rec( p, Gia_ObjFanin0(pObj) );
Gia_ObjPrint( p, pObj );
}
void Gia_ManPrintCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
{
if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
@ -1215,6 +1216,28 @@ void Gia_ManPrintCone( Gia_Man_t * p, Gia_Obj_t * pObj, int * pLeaves, int nLeav
Gia_ObjPrint( p, pObj );
}
void Gia_ManPrintCollect2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
{
if ( Vec_IntFind(vNodes, Gia_ObjId(p, pObj)) >= 0 )
return;
if ( Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj) )
Gia_ManPrintCollect2_rec( p, Gia_ObjFanin0(pObj), vNodes );
if ( Gia_ObjIsAnd(pObj) )
Gia_ManPrintCollect2_rec( p, Gia_ObjFanin1(pObj), vNodes );
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
}
void Gia_ManPrintCone2( Gia_Man_t * p, Gia_Obj_t * pObj )
{
Vec_Int_t * vNodes;
int i;
vNodes = Vec_IntAlloc( 100 );
Gia_ManPrintCollect2_rec( p, pObj, vNodes );
printf( "GIA logic cone for node %d:\n", Gia_ObjId(p, pObj) );
Gia_ManForEachObjVec( vNodes, p, pObj, i )
Gia_ObjPrint( p, pObj );
Vec_IntFree( vNodes );
}
/**Function*************************************************************
Synopsis [Complements the constraint outputs.]

10
src/base/abci/abcRec3.c
View File

@ -1035,7 +1035,15 @@ Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, &BestPo );
assert( BestPo >= 0 );
pGiaPo = Gia_ManCo( pGia, BestPo );
/*
if ( If_CutLeaveNum(pCut) == 6 )
{
printf( "\n" );
Kit_DsdPrintFromTruth( If_CutTruth(pCut), If_CutLeaveNum(pCut) ); printf( "\n" );
//Gia_ManPrintCo( pGia, pGiaPo );
Gia_ManPrintCone2( pGia, pGiaPo );
}
*/
// collect internal nodes into pGia->vTtNodes
if ( pGia->vTtNodes == NULL )
pGia->vTtNodes = Vec_IntAlloc( 256 );

57
src/bool/rsb/rsbDec6.c
View File

@ -334,7 +334,7 @@ int Rsb_DecInitCexes( int nVars, word * f, word ** g, int nGs, int nGsAll, word
SeeAlso []
***********************************************************************/
unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll )
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);
@ -365,7 +365,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n
pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
if ( uTruth )
return 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 );
@ -388,7 +398,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n
pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
if ( uTruth )
return 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 );
@ -414,7 +434,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n
pDivs[2] = g[j]; p->vFanins->pArray[2] = j;
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
if ( uTruth )
return 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 );
@ -443,7 +473,17 @@ unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int n
pDivs[3] = g[n]; p->vFanins->pArray[3] = n;
uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
if ( uTruth )
return 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 );
@ -611,7 +651,7 @@ unsigned Rsb_ManPerform( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs,
if ( fVerbose )
vTries = Vec_IntAlloc( 100 );
assert( nGs < nGsAll );
uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll );
uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll, 0 );
if ( uTruth )
{
@ -653,12 +693,13 @@ Vec_IntFree( vTries );
***********************************************************************/
int Rsb_ManPerformResub6( Rsb_Man_t * p, int nVarsAll, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose )
{
word * pGs[64];
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 );
uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs, 0 );
if ( uTruthRes == 0 )
return 0;

79
src/misc/extra/extraUtilDsd.c
View File

@ -27,6 +27,7 @@
#include "misc/vec/vec.h"
#include "misc/vec/vecHsh.h"
#include "misc/util/utilTruth.h"
#include "bool/rsb/rsb.h"
ABC_NAMESPACE_IMPL_START
@ -1151,6 +1152,84 @@ void Sdm_ManCompareCnfSizes()
}
*/
/**Function*************************************************************
Synopsis [Collect DSD divisors of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Sdm_ManDivCollect_rec( word t, Vec_Wrd_t ** pvDivs )
{
int i, Config, Counter = 0;
// check if function is decomposable
Config = Sdm_ManCheckDsd6( s_SdmMan, t );
if ( Config != -1 && (Config >> 17) < 2 )
return;
for ( i = 0; i < 6; i++ )
{
if ( !Abc_Tt6HasVar( t, i ) )
continue;
Sdm_ManDivCollect_rec( Abc_Tt6Cofactor0(t, i), pvDivs );
Sdm_ManDivCollect_rec( Abc_Tt6Cofactor1(t, i), pvDivs );
Counter++;
}
if ( Config != -1 && Counter >= 2 && Counter <= 4 )
{
Vec_WrdPush( pvDivs[Counter], (t & 1) ? ~t : t );
// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" );
}
}
void Sdm_ManDivTest()
{
// word u, t0, t1, t = ABC_CONST(0xB0F0BBFFB0F0BAFE);
// word u, t0, t1, t = ABC_CONST(0x3F1F3F13FFDFFFD3);
word u, t0, t1, t = ABC_CONST(0x3F3FFFFF37003700);
Rsb_Man_t * pManRsb = Rsb_ManAlloc( 6, 200, 3, 1 );
Vec_Wrd_t * pvDivs[7] = { NULL };
Vec_Wrd_t * vDivs = Vec_WrdAlloc( 100 );
int i, RetValue;
// collect divisors
for ( i = 2; i <= 4; i++ )
pvDivs[i] = Vec_WrdAlloc( 100 );
Sdm_ManDivCollect_rec( t, pvDivs );
for ( i = 2; i <= 4; i++ )
Vec_WrdUniqify( pvDivs[i] );
// prepare the set
vDivs = Vec_WrdAlloc( 100 );
for ( i = 0; i < 6; i++ )
Vec_WrdPush( vDivs, s_Truths6[i] );
for ( i = 2; i <= 4; i++ )
Vec_WrdAppend( vDivs, pvDivs[i] );
for ( i = 2; i <= 4; i++ )
Vec_WrdFree( pvDivs[i] );
Vec_WrdForEachEntry( vDivs, u, i )
{
printf( "%2d : ", i );
Kit_DsdPrintFromTruth( (unsigned *)&u, 6 ); printf( "\n" );
}
RetValue = Rsb_ManPerformResub6( pManRsb, 6, t, vDivs, &t0, &t1, 1 );
if ( RetValue )
{
Kit_DsdPrintFromTruth( (unsigned *)&t0, 6 ); printf( "\n" );
Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ); printf( "\n" );
printf( "Decomposition exits.\n" );
}
Vec_WrdFree( vDivs );
Rsb_ManFree( pManRsb );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

18
src/misc/vec/vecWrd.h
View File

@ -1120,6 +1120,24 @@ static inline void Vec_WrdSortUnsigned( Vec_Wrd_t * p )
}
/**Function*************************************************************
Synopsis [Appends the contents of the second vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_WrdAppend( Vec_Wrd_t * vVec1, Vec_Wrd_t * vVec2 )
{
word Entry; int i;
Vec_WrdForEachEntry( vVec2, Entry, i )
Vec_WrdPush( vVec1, Entry );
}
ABC_NAMESPACE_HEADER_END