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

Updates to arithmetic verification.

This commit is contained in:
Alan Mishchenko 2017-01-14 16:11:59 +07:00
parent 6d606b51ab
commit 79701f8b46
10 changed files with 215 additions and 128 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1270,6 +1270,7 @@ extern void Gia_ManOrigIdsInit( Gia_Man_t * p );
extern void Gia_ManOrigIdsStart( Gia_Man_t * p );
extern void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew );
extern Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs );
extern Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose );
extern void Gia_ManEquivFixOutputPairs( Gia_Man_t * p );
extern int Gia_ManCheckTopoOrder( Gia_Man_t * p );
extern int * Gia_ManDeriveNexts( Gia_Man_t * p );

27
src/aig/gia/giaEquiv.c
View File

@ -129,7 +129,7 @@ Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs )
}
Gia_ManHashStop( pNew );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntFree( vMap );
// compute equivalences
assert( !p->pReprs && !p->pNexts );
@ -169,6 +169,31 @@ Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs )
return pNew;
}
/**Function*************************************************************
Synopsis [Compute equivalence classes of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
{
Gia_Man_t * pTemp;
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Cec_ManFraSetDefaultParams( pPars );
pPars->fUseOrigIds = 1;
pPars->fSatSweeping = 1;
pPars->nBTLimit = nConfs;
pPars->fVerbose = fVerbose;
pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
Gia_ManStop( pTemp );
return Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG is not in the required topo order.]

20
src/base/abci/abc.c
View File

@ -40543,7 +40543,7 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew;
Acec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdtvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdtbvh" ) ) != EOF )
{
switch ( c )
{
@ -40578,6 +40578,9 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
pPars->fTwoOutput ^= 1;
break;
case 'b':
pPars->fBooth ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -40720,13 +40723,14 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &acec [-CT num] [-mdtvh] <file1> <file2>\n" );
Abc_Print( -2, "usage: &acec [-CT num] [-mdtbvh] <file1> <file2>\n" );
Abc_Print( -2, "\t combinational equivalence checking for arithmetic circuits\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", pPars->fMiter? "miter":"two circuits");
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", pPars->fDualOutput? "yes":"no");
Abc_Print( -2, "\t-t : toggle using two-word miter [default = %s]\n", pPars->fTwoOutput? "yes":"no");
Abc_Print( -2, "\t-b : toggle working with Booth multipliers [default = %s]\n", pPars->fBooth? "yes":"no");
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\tfile1 : (optional) the file with the first network\n");
@ -40748,12 +40752,15 @@ usage:
int Abc_CommandAbc9Anorm( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c, fVerbose = 0;
int c, fBooth = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
{
switch ( c )
{
case 'b':
fBooth ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -40768,13 +40775,14 @@ int Abc_CommandAbc9Anorm( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Anorm(): There is no AIG.\n" );
return 0;
}
pTemp = Acec_Normalize( pAbc->pGia, fVerbose );
pTemp = Acec_Normalize( pAbc->pGia, fBooth, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &anorm [-vh]\n" );
Abc_Print( -2, "usage: &anorm [-bvh]\n" );
Abc_Print( -2, "\t normalize adder trees in the current AIG\n" );
Abc_Print( -2, "\t-b : toggles working with Booth multipliers [default = %s]\n", fBooth? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

30
src/base/abci/abcDress3.c
View File

@ -33,32 +33,6 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Compute equivalence classes of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
{
Gia_Man_t * pTemp;
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Cec_ManFraSetDefaultParams( pPars );
pPars->fUseOrigIds = 1;
pPars->fSatSweeping = 1;
pPars->nBTLimit = nConfs;
pPars->fVerbose = fVerbose;
pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
Gia_ManStop( pTemp );
pTemp = Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
Gia_ManStop( pTemp );
}
/**Function*************************************************************
Synopsis [Converts AIG from HOP to GIA.]
@ -315,13 +289,15 @@ void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * p
void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose )
{
//abctime clk = Abc_Clock();
Gia_Man_t * pTemp;
Vec_Int_t * vClasses;
// derive shared AIG for the two networks
Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1], fByName );
if ( fVerbose )
printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs );
// compute equivalences in this AIG
Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose );
pTemp = Gia_ManComputeGiaEquivs( pGia, nConfs, fVerbose );
Gia_ManStop( pTemp );
//if ( fVerbose )
// Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk );
if ( fVerbose )

3
src/proof/acec/acec.h
View File

@ -47,6 +47,7 @@ struct Acec_ParCec_t_
int fMiter; // input circuit is a miter
int fDualOutput; // dual-output miter
int fTwoOutput; // two-output miter
int fBooth; // expecting Booth multiplier
int fSilent; // print no messages
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
@ -81,7 +82,7 @@ extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int
extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
/*=== acecTree.c ========================================================*/
extern Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fVerbose );
extern Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose );
ABC_NAMESPACE_HEADER_END

73
src/proof/acec/acecCore.c
View File

@ -68,7 +68,7 @@ void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
SeeAlso []
***********************************************************************/
Gia_Man_t * Acec_FindEquivs( Gia_Man_t * pBase, Gia_Man_t * pAdd )
Gia_Man_t * Acec_CommonStart( Gia_Man_t * pBase, Gia_Man_t * pAdd )
{
Gia_Obj_t * pObj;
int i;
@ -93,35 +93,69 @@ Gia_Man_t * Acec_FindEquivs( Gia_Man_t * pBase, Gia_Man_t * pAdd )
pObj->Value = Gia_ManHashAnd( pBase, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
return pBase;
}
Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd )
void Acec_CommonFinish( Gia_Man_t * pBase )
{
int Id;
Gia_ManCreateRefs( pBase );
Gia_ManForEachAndId( pBase, Id )
if ( Gia_ObjRefNumId(pBase, Id) == 0 )
Gia_ManAppendCo( pBase, Abc_Var2Lit(Id,0) );
}
Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd, Gia_Man_t * pBase )
{
Gia_Obj_t * pObj; int i;
Vec_Int_t * vMapNew = Vec_IntStartFull( Gia_ManObjNum(pAdd) );
Gia_ManSetPhase( pAdd );
Vec_IntWriteEntry( vMapNew, 0, 0 );
Gia_ManForEachCand( pAdd, pObj, i )
Vec_IntWriteEntry( vMapNew, i, Abc_Lit2Var(pObj->Value) );
{
int iObjBase = Abc_Lit2Var(pObj->Value);
Gia_Obj_t * pObjBase = Gia_ManObj( pBase, iObjBase );
int iObjRepr = Abc_Lit2Var(pObjBase->Value);
Vec_IntWriteEntry( vMapNew, i, Abc_Var2Lit(iObjRepr, Gia_ObjPhase(pObj)) );
}
return vMapNew;
}
void Acec_ComputeEquivClasses( Gia_Man_t * pOne, Gia_Man_t * pTwo, Vec_Int_t ** pvMap1, Vec_Int_t ** pvMap2 )
{
Gia_Man_t * pBase;
pBase = Acec_FindEquivs( NULL, pOne );
pBase = Acec_FindEquivs( pBase, pTwo );
*pvMap1 = Acec_CountRemap( pOne );
*pvMap2 = Acec_CountRemap( pTwo );
Gia_Man_t * pBase, * pRepr;
pBase = Acec_CommonStart( NULL, pOne );
pBase = Acec_CommonStart( pBase, pTwo );
Acec_CommonFinish( pBase );
//Gia_ManShow( pBase, NULL, 0, 0, 0 );
pRepr = Gia_ManComputeGiaEquivs( pBase, 100, 0 );
*pvMap1 = Acec_CountRemap( pOne, pBase );
*pvMap2 = Acec_CountRemap( pTwo, pBase );
Gia_ManStop( pBase );
Gia_ManStop( pRepr );
}
static inline void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCosts )
void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
{
int i, j, best_i;
for ( i = 0; i < nSize-1; i++ )
{
best_i = i;
for ( j = i+1; j < nSize; j++ )
if ( pCosts[Abc_Lit2Var(pArray[j])] > pCosts[Abc_Lit2Var(pArray[best_i])] )
if ( Abc_Lit2LitL(pCostLits, pArray[j]) > Abc_Lit2LitL(pCostLits, pArray[best_i]) )
best_i = j;
ABC_SWAP( int, pArray[i], pArray[best_i] );
}
}
void Acec_MatchPrintEquivLits( Vec_Wec_t * vLits, int * pCostLits )
{
Vec_Int_t * vLevel;
int i, k, Entry;
printf( "Leaf literals and their classes:\n" );
Vec_WecForEachLevel( vLits, vLevel, i )
{
printf( "Rank %2d : %2d ", i, Vec_IntSize(vLevel) );
Vec_IntForEachEntry( vLevel, Entry, k )
printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) );
printf( "\n" );
}
}
int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
{
Vec_Int_t * vMap0, * vMap1, * vLevel;
@ -132,6 +166,8 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap0) );
Vec_WecForEachLevel( pBox1->vLeafLits, vLevel, i )
Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap1) );
//Acec_MatchPrintEquivLits( pBox0->vLeafLits, Vec_IntArray(vMap0) );
//Acec_MatchPrintEquivLits( pBox1->vLeafLits, Vec_IntArray(vMap1) );
// reorder nodes to have the same order
assert( pBox0->vShared == NULL );
assert( pBox1->vShared == NULL );
@ -159,8 +195,9 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
int * pEnd1 = Vec_IntLimit(vLevel1);
while ( pBeg0 < pEnd0 && pBeg1 < pEnd1 )
{
int Entry0 = Abc_Lit2LitV( Vec_IntArray(vMap0), *pBeg0 );
int Entry1 = Abc_Lit2LitV( Vec_IntArray(vMap1), *pBeg1 );
int Entry0 = Abc_Lit2LitL( Vec_IntArray(vMap0), *pBeg0 );
int Entry1 = Abc_Lit2LitL( Vec_IntArray(vMap1), *pBeg1 );
assert( *pBeg0 && *pBeg1 );
if ( Entry0 == Entry1 )
{
Vec_IntPush( vShared0, *pBeg0++ );
@ -201,11 +238,16 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
{
int status = -1;
abctime clk = Abc_Clock();
Gia_Man_t * pMiter;
Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, pPars->fVerbose );
Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, pPars->fVerbose );
Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, pPars->fVerbose );
Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, pPars->fVerbose );
Vec_BitFreeP( &vIgnore0 );
Vec_BitFreeP( &vIgnore1 );
if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
printf( "Cannot find arithmetic boxes in both LHS and RHS. Trying regular CEC.\n" );
else if ( !Acec_MatchBoxes( pBox0, pBox1 ) ) // cannot find matching
@ -214,7 +256,8 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
{
pGia0n = Acec_InsertBox( pBox0, 1 );
pGia1n = Acec_InsertBox( pBox1, 1 );
printf( "Found, matched, and normalized arithmetic boxes in LHS and RHS. Solving resulting CEC.\n" );
printf( "Matching of adder trees in LHS and RHS succeeded. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
// solve regular CEC problem
Cec_ManCecSetDefaultParams( pCecPars );

3
src/proof/acec/acecInt.h
View File

@ -69,10 +69,11 @@ extern Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Ve
extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes );
/*=== acecMult.c ========================================================*/
extern Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits );
extern Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p );
/*=== acecNorm.c ========================================================*/
extern Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll );
/*=== acecTree.c ========================================================*/
extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose );
extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose );
extern void Acec_BoxFreeP( Acec_Box_t ** ppBox );
/*=== acecUtil.c ========================================================*/
extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );

19
src/proof/acec/acecMult.c
View File

@ -490,18 +490,16 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
Gia_ManForEachAndId( p, iObj )
{
word Truth = Gia_ObjComputeTruth6Cis( p, Abc_Var2Lit(iObj, 0), vSupp, vTemp );
if ( Vec_IntSize(vSupp) > 6 )
continue;
vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
if ( Vec_IntSize(vSupp) > 5 )
continue;
for ( i = 0; i < 32; i++ )
for ( i = 0; i < 32 && Saved[i]; i++ )
{
if ( Saved[i] == 0 )
break;
if ( Truth == Saved[i] || Truth == ~Saved[i] )
{
//Vec_IntPush( vBold, iObj );
Acec_MultFindPPs_rec( p, iObj, vBold );
printf( "%d ", iObj );
nProds++;
break;
}
@ -515,7 +513,6 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
Vec_IntPrint( vSupp );
*/
}
printf( "\n" );
Gia_ManCleanMark0(p);
printf( "Collected %d pps and %d nodes.\n", nProds, Vec_IntSize(vBold) );
@ -523,6 +520,16 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
Vec_WrdFree( vTemp );
return vBold;
}
Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p )
{
Vec_Bit_t * vIgnore = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vMap = Acec_MultFindPPs( p );
int i, Entry;
Vec_IntForEachEntry( vMap, Entry, i )
Vec_BitWriteEntry( vIgnore, Entry, 1 );
Vec_IntFree( vMap );
return vIgnore;
}
void Acec_MultFindPPsTest( Gia_Man_t * p )
{
Vec_Int_t * vBold = Acec_MultFindPPs( p );

6
src/proof/acec/acecNorm.c
View File

@ -198,11 +198,13 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
SeeAlso []
***********************************************************************/
Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fVerbose )
Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose )
{
Acec_Box_t * pBox = Acec_DeriveBox( pGia, fVerbose );
Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL;
Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose );
Gia_Man_t * pNew = Acec_InsertBox( pBox, 1 );
Acec_BoxFreeP( &pBox );
Vec_BitFreeP( &vIgnore );
return pNew;
}

161
src/proof/acec/acecTree.c
View File

@ -27,6 +27,12 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Acec_SignBit( Vec_Int_t * vAdds, int iBox, int b ) { return (Vec_IntEntry(vAdds, 6*iBox+5) >> b) & 1; }
static inline int Acec_SignBit2( Vec_Int_t * vAdds, int iBox, int b ) { return (Vec_IntEntry(vAdds, 6*iBox+5) >> (16+b)) & 1; }
static inline void Acec_SignSetBit( Vec_Int_t * vAdds, int iBox, int b, int v ) { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << b); }
static inline void Acec_SignSetBit2( Vec_Int_t * vAdds, int iBox, int b, int v ) { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << (16+b)); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -147,10 +153,7 @@ void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox )
Gia_Obj_t * pObj;
unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
int Sign = Vec_IntEntry( vAdds, 6*iBox+5 ), Phase[5];
for ( k = 0; k < 5; k++ )
Phase[k] = (Sign >> (4+k)) & 1;
int fFlip = !fFadd && Acec_SignBit2(vAdds, iBox, 2);
Gia_ManIncrementTravId( p );
for ( k = 0; k < 3; k++ )
@ -159,17 +162,17 @@ void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox )
if ( iObj == 0 )
continue;
pObj = Gia_ManObj( p, iObj );
pObj->Value = Phase[k] ? 0xFF & ~Truths[k] : Truths[k];
pObj->Value = (Acec_SignBit2(vAdds, iBox, k) ^ fFlip) ? 0xFF & ~Truths[k] : Truths[k];
Gia_ObjSetTravIdCurrent( p, pObj );
}
iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
TruthXor = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
TruthXor = Phase[3] ? 0xFF & ~TruthXor : TruthXor;
TruthXor = (Acec_SignBit2(vAdds, iBox, 3) ^ fFlip) ? 0xFF & ~TruthXor : TruthXor;
iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
TruthMaj = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
TruthMaj = Phase[4] ? 0xFF & ~TruthMaj : TruthMaj;
TruthMaj = (Acec_SignBit2(vAdds, iBox, 4) ^ fFlip) ? 0xFF & ~TruthMaj : TruthMaj;
if ( fFadd ) // FADD
{
@ -180,6 +183,8 @@ void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox )
}
else
{
//printf( "Sign1 = %d%d%d %d\n", Acec_SignBit(vAdds, iBox, 0), Acec_SignBit(vAdds, iBox, 1), Acec_SignBit(vAdds, iBox, 2), Acec_SignBit(vAdds, iBox, 3) );
//printf( "Sign2 = %d%d%d %d%d\n", Acec_SignBit2(vAdds, iBox, 0), Acec_SignBit2(vAdds, iBox, 1), Acec_SignBit2(vAdds, iBox, 2), Acec_SignBit2(vAdds, iBox, 3), Acec_SignBit2(vAdds, iBox, 4) );
if ( TruthXor != 0x66 )
printf( "Hadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
if ( TruthMaj != 0x88 )
@ -194,6 +199,36 @@ void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes
Vec_IntForEachEntry( vLevel, Box, k )
Acec_TreeVerifyPhaseOne( p, vAdds, Box );
}
void Acec_TreeVerifyPhases2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
{
Vec_Bit_t * vPhase = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vRoots = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vLevel;
int i, k, n, Box;
// mark all output points and their values
Vec_WecForEachLevel( vBoxes, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, k )
{
Vec_BitWriteEntry( vRoots, Vec_IntEntry( vAdds, 6*Box+3 ), 1 );
Vec_BitWriteEntry( vRoots, Vec_IntEntry( vAdds, 6*Box+4 ), 1 );
Vec_BitWriteEntry( vPhase, Vec_IntEntry( vAdds, 6*Box+3 ), Acec_SignBit2(vAdds, Box, 3) );
Vec_BitWriteEntry( vPhase, Vec_IntEntry( vAdds, 6*Box+4 ), Acec_SignBit2(vAdds, Box, 4) );
}
// compare with input points
Vec_WecForEachLevel( vBoxes, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, k )
for ( n = 0; n < 3; n++ )
{
if ( !Vec_BitEntry(vRoots, Vec_IntEntry(vAdds, 6*Box+n)) )
continue;
if ( Vec_BitEntry(vPhase, Vec_IntEntry(vAdds, 6*Box+n)) == Acec_SignBit2(vAdds, Box, n) )
continue;
printf( "Phase of input %d=%d is mismatched in box %d=(%d,%d).\n",
n, Vec_IntEntry(vAdds, 6*Box+n), Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4) );
}
Vec_BitFree( vPhase );
Vec_BitFree( vRoots );
}
/**Function*************************************************************
@ -216,40 +251,40 @@ Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBo
Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*Box+4), Box );
return vMap;
}
void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase )
void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase, Vec_Bit_t * vVisit )
{
int k, iBox, iXor, Sign, fXorPhase, fPhaseThis;
int k, iBox, iXor, fXorPhase, fPhaseThis;
assert( Node != 0 );
iBox = Vec_IntEntry( vMap, Node );
if ( iBox == -1 )
return;
assert( Node == Vec_IntEntry( vAdds, 6*iBox+4 ) );
if ( Vec_BitEntry(vVisit, iBox) )
return;
Vec_BitWriteEntry( vVisit, iBox, 1 );
iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
Sign = Vec_IntEntry( vAdds, 6*iBox+5 ) & 0xFFFFFFF0;
fXorPhase = ((Sign >> 3) & 1);
fXorPhase = Acec_SignBit(vAdds, iBox, 3);
if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
{
fPhase ^= ((Sign >> 2) & 1);
if ( fPhase ) // complemented HADD
Sign |= (1 << 6);
//fPhaseThis = Acec_SignBit( vAdds, iBox, 2 ) ^ fPhase;
//fXorPhase ^= fPhaseThis;
//Acec_SignSetBit2( vAdds, iBox, 2, fPhaseThis ); // complemented HADD -- create const1 input
fPhase ^= Acec_SignBit( vAdds, iBox, 2 );
fXorPhase ^= fPhase;
Acec_SignSetBit2( vAdds, iBox, 2, fPhase ); // complemented HADD -- create const1 input
}
for ( k = 0; k < 3; k++ )
{
int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
if ( iObj == 0 )
continue;
fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
fPhaseThis = Acec_SignBit(vAdds, iBox, k) ^ fPhase;
fXorPhase ^= fPhaseThis;
Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis );
if ( fPhaseThis )
Sign |= (1 << (4+k));
Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis, vVisit );
Acec_SignSetBit2( vAdds, iBox, k, fPhaseThis );
}
if ( fXorPhase )
Sign |= (1 << 7);
if ( fPhase )
Sign |= (1 << 8);
// save updated signature
Vec_IntWriteEntry( vAdds, 6*iBox+5, Sign );
Acec_SignSetBit2( vAdds, iBox, 3, fXorPhase );
Acec_SignSetBit2( vAdds, iBox, 4, fPhase );
}
/**Function*************************************************************
@ -271,12 +306,14 @@ void Acec_TreeAddInOutPoint( Vec_Int_t * vMap, int iObj, int iAdd, int fOut )
else if ( *pPlace >= 0 )
*pPlace = -2;
}
Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds )
Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore )
{
Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(p) );
int i;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
continue;
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 );
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 );
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+2), i, 0 );
@ -328,10 +365,10 @@ void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int
Acec_TreeFindTrees2_rec( vAdds, vMap, In, Acec_TreeWhichPoint(vAdds, In, iObj) == 4 ? Rank-1 : Rank, vTree, vFound );
Acec_TreeFindTrees2_rec( vAdds, vMap, Out, Rank, vTree, vFound );
}
Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds )
Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore )
{
Vec_Wec_t * vTrees = Vec_WecAlloc( 10 );
Vec_Int_t * vMap = Acec_TreeFindPoints( p, vAdds );
Vec_Int_t * vMap = Acec_TreeFindPoints( p, vAdds, vIgnore );
Vec_Bit_t * vFound = Vec_BitStart( Vec_IntSize(vAdds)/6 );
Vec_Int_t * vTree;
int i, k, In, Out, Box, Rank, MinRank;
@ -371,7 +408,7 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
vTrees = Acec_TreeFindTrees( p, vAdds );
vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
printf( "Collected %d trees with %d adders in them. ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Vec_WecPrint( vTrees, 0 );
@ -417,23 +454,6 @@ void Vec_WecPrintLits( Vec_Wec_t * p )
printf( " }\n" );
}
}
void Acec_PrintRootLits( Vec_Wec_t * vRoots )
{
Vec_Int_t * vLevel;
int i, k, iObj;
Vec_WecForEachLevel( vRoots, vLevel, i )
{
printf( "Rank %d : %2d ", i, Vec_IntSize(vLevel) );
Vec_IntForEachEntry( vLevel, iObj, k )
{
int fFadd = Abc_LitIsCompl(iObj);
int fCout = Abc_LitIsCompl(Abc_Lit2Var(iObj));
int Node = Abc_Lit2Var(Abc_Lit2Var(iObj));
printf( "%d%s%s ", Node, fCout ? "*" : "", (fCout && fFadd) ? "*" : "" );
}
printf( "\n" );
}
}
void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
{
printf( "Adders:\n" );
@ -442,8 +462,6 @@ void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
Vec_WecPrintLits( pBox->vLeafLits );
printf( "Outputs:\n" );
Vec_WecPrintLits( pBox->vRootLits );
//printf( "Raw outputs:\n" );
//Acec_PrintRootLits( pBox->vRoots );
}
int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
@ -456,10 +474,11 @@ int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
{
int MaxRank = Acec_CreateBoxMaxRank(vTree);
Vec_Bit_t * vVisit = Vec_BitStart( Vec_IntSize(vAdds)/6 );
Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vLevel, * vMap;
int i, k, Box, Rank;
int i, j, k, Box, Rank;
Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
pBox->pGia = p;
@ -470,38 +489,42 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
// collect boxes; mark inputs/outputs
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
Vec_WecPush( pBox->vAdds, Rank, Box );
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 );
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 );
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 );
Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+3), 1 );
Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+4), 1 );
Vec_WecPush( pBox->vAdds, Rank, Box );
}
// sort each level
Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
Vec_IntSort( vLevel, 0 );
// set phases
// set phases starting from roots
vMap = Acec_TreeCarryMap( p, vAdds, pBox->vAdds );
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) )
Acec_TreePhases_rec( p, vAdds, vMap, Vec_IntEntry(vAdds, 6*Box+4), Vec_IntEntry(vAdds, 6*Box+2) != 0 );
Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, k )
if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) )
Acec_TreePhases_rec( p, vAdds, vMap, Vec_IntEntry(vAdds, 6*Box+4), Vec_IntEntry(vAdds, 6*Box+2) != 0, vVisit );
Acec_TreeVerifyPhases( p, vAdds, pBox->vAdds );
Acec_TreeVerifyPhases2( p, vAdds, pBox->vAdds );
Vec_BitFree( vVisit );
Vec_IntFree( vMap );
// collect inputs/outputs
Vec_BitWriteEntry( vIsLeaf, 0, 0 );
Vec_BitWriteEntry( vIsRoot, 0, 0 );
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
int Sign = Vec_IntEntry( vAdds, 6*Box+5 );
for ( k = 0; k < 3; k++ )
if ( !Vec_BitEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k) ) )
Vec_WecPush( pBox->vLeafLits, Rank, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), (Sign >> (4+k)) & 1) );
for ( k = 3; k < 5; k++ )
if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
Vec_WecPush( pBox->vRootLits, k == 4 ? Rank + 1 : Rank, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), (Sign >> (7+k)) & 1) );
}
Vec_BitWriteEntry( vIsRoot, 0, 1 );
Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, j )
{
for ( k = 0; k < 3; k++ )
if ( !Vec_BitEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k) ) )
Vec_WecPush( pBox->vLeafLits, i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
for ( k = 3; k < 5; k++ )
if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
Vec_WecPush( pBox->vRootLits, k == 4 ? i + 1 : i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
if ( Vec_IntEntry(vAdds, 6*Box+2) == 0 && Acec_SignBit2(vAdds, Box, 2) )
Vec_WecPush( pBox->vLeafLits, i, 1 );
}
Vec_BitFree( vIsLeaf );
Vec_BitFree( vIsRoot );
// sort each level
@ -524,7 +547,7 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
vTrees = Acec_TreeFindTrees( p, vAdds );
vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
printf( "Collected %d trees with %d adders in them. ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//Vec_WecPrint( vTrees, 0 );
@ -554,11 +577,11 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose )
Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose )
{
Acec_Box_t * pBox = NULL;
Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds );
Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore );
if ( vTrees && Vec_WecSize(vTrees) > 0 )
pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
if ( pBox )//&& fVerbose )
@ -567,7 +590,7 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose )
Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) );
if ( pBox && fVerbose )
Acec_PrintBox( pBox, vAdds );
Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
//Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
Vec_WecFreeP( &vTrees );
Vec_IntFree( vAdds );
return pBox;