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-13 21:17:00 +07:00
parent 1a39fb3946
commit 6d606b51ab
5 changed files with 326 additions and 278 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
src/aig/gia/giaShow.c
View File

@ -52,7 +52,7 @@ void Gia_ShowPath( Gia_Man_t * p, char * pFileName )
Gia_Obj_t * pNode;
Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) );
int i, k, iFan, LevelMax, nLevels, * pLevels, Level, Prev;
int nLuts = 0, nNodes = 0, nEdges = 0, nEdgesAll = 0;
int nLuts = 0, nNodes = 0, nEdges = 0;
assert( Gia_ManHasMapping(p) );
// set critical CO drivers
@ -670,7 +670,7 @@ int Gia_ShowAddOut( Vec_Int_t * vAdds, Vec_Int_t * vMapAdds, int Node )
return Vec_IntEntry( vAdds, 6*iBox+4 );
return Node;
}
void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors, Vec_Int_t * vOrder )
void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors, Vec_Int_t * vOrder )
{
FILE * pFile;
Gia_Obj_t * pNode;//, * pTemp, * pPrev;
@ -689,6 +689,11 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
return;
}
// mark the nodes
if ( vBold )
Gia_ManForEachObjVec( vBold, p, pNode, i )
pNode->fMark0 = 1;
// compute levels
LevelMax = 1 + p->nLevels;
Gia_ManForEachCo( p, pNode, i )
@ -819,7 +824,7 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
else
fprintf( pFile, ", shape = ellipse" );
*/
if ( Vec_IntEntry(vMapAdds, iNode) >= 0 )
if ( !pNode->fMark0 && Vec_IntEntry(vMapAdds, iNode) >= 0 )
{
int iBox = Vec_IntEntry(vMapAdds, iNode);
fprintf( pFile, " Node%d [label = \"%d_%d\"", Gia_ShowAddOut(vAdds, vMapAdds, iNode), Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
@ -848,8 +853,8 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
fprintf( pFile, " Node%d [label = \"%d\"", iNode, iNode );
fprintf( pFile, ", shape = ellipse" );
}
// if ( pNode->fMark0 )
// fprintf( pFile, ", style = filled" );
if ( pNode->fMark0 )
fprintf( pFile, ", style = filled" );
fprintf( pFile, "];\n" );
}
fprintf( pFile, "}" );
@ -920,8 +925,6 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
Gia_ManForEachObjVec( vOrder, p, pNode, i )
{
int iNode = Gia_ObjId( p, pNode );
// if ( !Gia_ObjIsAnd(pNode) && !Gia_ObjIsCo(pNode) && !Gia_ObjIsBuf(pNode) )
// continue;
if ( Vec_IntEntry(vMapAdds, Gia_ObjId(p, pNode)) >= 0 )
{
int k, iBox = Vec_IntEntry(vMapAdds, iNode);
@ -990,6 +993,11 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
fprintf( pFile, "\n" );
fclose( pFile );
// unmark nodes
if ( vBold )
Gia_ManForEachObjVec( vBold, p, pNode, i )
pNode->fMark0 = 0;
Vec_IntFreeP( &p->vLevels );
}
@ -1093,12 +1101,12 @@ Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * v
SeeAlso []
***********************************************************************/
void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
{
Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds );
Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors );
Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors );
Gia_WriteDotAig( p, pFileName, vAdds, vXors, vMapAdds, vMapXors, vOrder );
Gia_WriteDotAig( p, pFileName, vBold, vAdds, vXors, vMapAdds, vMapXors, vOrder );
Vec_IntFree( vMapAdds );
Vec_IntFree( vMapXors );
Vec_IntFree( vOrder );
@ -1121,7 +1129,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds,
if ( fPath )
Gia_ShowPath( pMan, FileNameDot );
else if ( fAdders )
Gia_ShowProcess( pMan, FileNameDot, vAdds, vXors, fFadds );
Gia_ShowProcess( pMan, FileNameDot, vBold, vAdds, vXors, fFadds );
else
Gia_WriteDotAigSimple( pMan, FileNameDot, vBold );
// visualize the file

10
src/base/wlc/wlcBlast.c
View File

@ -645,10 +645,20 @@ void Wlc_IntInsert( Vec_Int_t * vProd, Vec_Int_t * vLevel, int Node, int Level )
}
void Wlc_BlastPrintMatrix( Gia_Man_t * p, Vec_Wec_t * vProds )
{
int fVerbose = 0;
Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
Vec_Int_t * vLevel; word Truth;
int i, k, iLit;
Vec_WecForEachLevel( vProds, vLevel, i )
Vec_IntForEachEntry( vLevel, iLit, k )
if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
Vec_IntPushUnique( vSupp, Abc_Lit2Var(iLit) );
printf( "Booth partial products: %d pps, %d unique, %d nodes.\n",
Vec_WecSizeSize(vProds), Vec_IntSize(vSupp), Gia_ManAndNum(p) );
Vec_IntPrint( vSupp );
if ( fVerbose )
Vec_WecForEachLevel( vProds, vLevel, i )
Vec_IntForEachEntry( vLevel, iLit, k )
{

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

@ -42,13 +42,10 @@ struct Acec_Box_t_
{
Gia_Man_t * pGia; // AIG manager
Vec_Wec_t * vAdds; // adders by rank
Vec_Wec_t * vLeafs; // leaf literals by rank
Vec_Wec_t * vRoots; // root literals by rank
Vec_Wec_t * vLeafLits; // leaf literals by rank
Vec_Wec_t * vRootLits; // root literals by rank
Vec_Wec_t * vShared; // shared leaves
Vec_Wec_t * vUnique; // unique leaves
Vec_Bit_t * vInvHadds; // complemented half adders
};
////////////////////////////////////////////////////////////////////////

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

@ -20,6 +20,7 @@
#include "acecInt.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@ -400,6 +401,15 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec
if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
printf( " " );
Vec_IntPrint( vSupp );
/*
if ( Truth == 0xF335ACC0F335ACC0 )
{
int iObj = Abc_Lit2Var(iLit);
Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 );
Gia_ManShow( pGia0, NULL, 0, 0, 0 );
Gia_ManStop( pGia0 );
}
*/
}
// support rank counts
Vec_IntForEachEntry( vSupp, Entry, j )
@ -423,6 +433,103 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec
return vInputs;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_MultFindPPs_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vBold )
{
Gia_Obj_t * pObj;
pObj = Gia_ManObj( p, iObj );
if ( pObj->fMark0 )
return;
pObj->fMark0 = 1;
if ( !Gia_ObjIsAnd(pObj) )
return;
Acec_MultFindPPs_rec( p, Gia_ObjFaninId0(pObj, iObj), vBold );
Acec_MultFindPPs_rec( p, Gia_ObjFaninId1(pObj, iObj), vBold );
Vec_IntPush( vBold, iObj );
}
Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
{
word Saved[32] = {
ABC_CONST(0xF335ACC0F335ACC0),
ABC_CONST(0x35C035C035C035C0),
ABC_CONST(0xD728D728D728D728),
ABC_CONST(0xFD80FD80FD80FD80),
ABC_CONST(0xACC0ACC0ACC0ACC0),
ABC_CONST(0x7878787878787878),
ABC_CONST(0x2828282828282828),
ABC_CONST(0xD0D0D0D0D0D0D0D0),
ABC_CONST(0x8080808080808080),
ABC_CONST(0x8888888888888888),
ABC_CONST(0xAAAAAAAAAAAAAAAA),
ABC_CONST(0x5555555555555555),
ABC_CONST(0xD5A8D5A8D5A8D5A8),
ABC_CONST(0x2A572A572A572A57),
ABC_CONST(0xF3C0F3C0F3C0F3C0),
ABC_CONST(0x5858585858585858),
ABC_CONST(0xA7A7A7A7A7A7A7A7),
ABC_CONST(0x2727272727272727),
ABC_CONST(0xD8D8D8D8D8D8D8D8)
};
Vec_Int_t * vBold = Vec_IntAlloc( 100 );
Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
int i, iObj, nProds = 0;
Gia_ManCleanMark0(p);
Gia_ManForEachAndId( p, iObj )
{
word Truth = Gia_ObjComputeTruth6Cis( p, Abc_Var2Lit(iObj, 0), vSupp, vTemp );
vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
if ( Vec_IntSize(vSupp) > 5 )
continue;
for ( i = 0; i < 32; 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;
}
}
/*
Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
if ( Vec_IntSize(vSupp) == 4 ) printf( " " );
if ( Vec_IntSize(vSupp) == 3 ) printf( " " );
if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
printf( " " );
Vec_IntPrint( vSupp );
*/
}
printf( "\n" );
Gia_ManCleanMark0(p);
printf( "Collected %d pps and %d nodes.\n", nProds, Vec_IntSize(vBold) );
Vec_IntFree( vSupp );
Vec_WrdFree( vTemp );
return vBold;
}
void Acec_MultFindPPsTest( Gia_Man_t * p )
{
Vec_Int_t * vBold = Acec_MultFindPPs( p );
Gia_ManShow( p, vBold, 1, 0, 0 );
Vec_IntFree( vBold );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -45,13 +45,10 @@ ABC_NAMESPACE_IMPL_START
void Acec_BoxFree( Acec_Box_t * pBox )
{
Vec_WecFreeP( &pBox->vAdds );
Vec_WecFreeP( &pBox->vLeafs );
Vec_WecFreeP( &pBox->vRoots );
Vec_WecFreeP( &pBox->vLeafLits );
Vec_WecFreeP( &pBox->vRootLits );
Vec_WecFreeP( &pBox->vUnique );
Vec_WecFreeP( &pBox->vShared );
Vec_BitFreeP( &pBox->vInvHadds );
ABC_FREE( pBox );
}
void Acec_BoxFreeP( Acec_Box_t ** ppBox )
@ -120,6 +117,141 @@ void Acec_TreeFilterTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees
Acec_TreeFilterOne( p, vAdds, vLevel );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acec_TreeVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
int Truth0, Truth1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return pObj->Value;
Gia_ObjSetTravIdCurrent(p, pObj);
assert( Gia_ObjIsAnd(pObj) );
assert( !Gia_ObjIsXor(pObj) );
Truth0 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
Truth1 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
return (pObj->Value = Truth0 & Truth1);
}
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;
Gia_ManIncrementTravId( p );
for ( k = 0; k < 3; k++ )
{
iObj = Vec_IntEntry( vAdds, 6*iBox+k );
if ( iObj == 0 )
continue;
pObj = Gia_ManObj( p, iObj );
pObj->Value = Phase[k] ? 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;
iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
TruthMaj = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
TruthMaj = Phase[4] ? 0xFF & ~TruthMaj : TruthMaj;
if ( fFadd ) // FADD
{
if ( TruthXor != 0x96 )
printf( "Fadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
if ( TruthMaj != 0xE8 )
printf( "Fadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
}
else
{
if ( TruthXor != 0x66 )
printf( "Hadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
if ( TruthMaj != 0x88 )
printf( "Hadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
}
}
void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
{
Vec_Int_t * vLevel;
int i, k, Box;
Vec_WecForEachLevel( vBoxes, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, k )
Acec_TreeVerifyPhaseOne( p, vAdds, Box );
}
/**Function*************************************************************
Synopsis [Creates polarity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
{
Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
Vec_Int_t * vLevel;
int i, k, Box;
Vec_WecForEachLevel( vBoxes, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, k )
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 )
{
int k, iBox, iXor, Sign, fXorPhase, fPhaseThis;
assert( Node != 0 );
iBox = Vec_IntEntry( vMap, Node );
if ( iBox == -1 )
return;
assert( Node == Vec_IntEntry( vAdds, 6*iBox+4 ) );
iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
Sign = Vec_IntEntry( vAdds, 6*iBox+5 ) & 0xFFFFFFF0;
fXorPhase = ((Sign >> 3) & 1);
if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
{
fPhase ^= ((Sign >> 2) & 1);
if ( fPhase ) // complemented HADD
Sign |= (1 << 6);
}
for ( k = 0; k < 3; k++ )
{
int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
if ( iObj == 0 )
continue;
fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
fXorPhase ^= fPhaseThis;
Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis );
if ( fPhaseThis )
Sign |= (1 << (4+k));
}
if ( fXorPhase )
Sign |= (1 << 7);
if ( fPhase )
Sign |= (1 << 8);
// save updated signature
Vec_IntWriteEntry( vAdds, 6*iBox+5, Sign );
}
/**Function*************************************************************
Synopsis [Find internal cut points with exactly one adder fanin/fanout.]
@ -249,256 +381,6 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
}
/**Function*************************************************************
Synopsis [Creates leaves and roots.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
{
int k, Box, Rank, MaxRank = 0;
Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
MaxRank = Abc_MaxInt( MaxRank, Rank );
return MaxRank;
}
void Acec_TreeInsOuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree, Vec_Wec_t * vBoxes, Vec_Wec_t * vLeaves, Vec_Wec_t * vRoots )
{
Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vLevel;
int i, k, Box, Rank;
Vec_BitWriteEntry( vIsLeaf, 0, 1 );
Vec_BitWriteEntry( vIsRoot, 0, 1 );
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
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_IntForEachEntryDouble( vTree, Box, Rank, i )
{
Vec_WecPush( vBoxes, Rank, Box );
for ( k = 0; k < 3; k++ )
{
if ( Vec_BitEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k) ) )
continue;
Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k), 1 );
Vec_WecPush( vLeaves, Rank, Vec_IntEntry(vAdds, 6*Box+k) );
}
for ( k = 3; k < 5; k++ )
{
if ( Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
continue;
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k), 1 );
Vec_WecPush( vRoots, k == 4 ? Rank + 1 : Rank, Abc_Var2Lit(Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), k==4), Vec_IntEntry(vAdds, 6*Box+2)!=0) );
}
}
Vec_BitFree( vIsLeaf );
Vec_BitFree( vIsRoot );
// sort each level
Vec_WecForEachLevel( vBoxes, vLevel, i )
Vec_IntSort( vLevel, 0 );
Vec_WecForEachLevel( vLeaves, vLevel, i )
Vec_IntSort( vLevel, 0 );
Vec_WecForEachLevel( vRoots, vLevel, i )
Vec_IntSort( vLevel, 0 );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acec_TreeVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
int Truth0, Truth1;
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return pObj->Value;
Gia_ObjSetTravIdCurrent(p, pObj);
assert( Gia_ObjIsAnd(pObj) );
assert( !Gia_ObjIsXor(pObj) );
Truth0 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
Truth1 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
return (pObj->Value = Truth0 & Truth1);
}
void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bit_t * vPhase )
{
Gia_Obj_t * pObj;
unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
//if ( !fFadd )
// return;
Gia_ManIncrementTravId( p );
for ( k = 0; k < 3; k++ )
{
iObj = Vec_IntEntry( vAdds, 6*iBox+k );
if ( iObj == 0 )
continue;
pObj = Gia_ManObj( p, iObj );
pObj->Value = Vec_BitEntry(vPhase, iObj) ? 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 = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthXor : TruthXor;
iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
TruthMaj = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj;
if ( fFadd ) // FADD
{
if ( TruthXor != 0x96 )
printf( "Fadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
if ( TruthMaj != 0xE8 )
printf( "Fadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
}
else
{
if ( TruthXor != 0x66 )
printf( "Hadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
if ( TruthMaj != 0x88 )
printf( "Hadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
}
}
void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes, Vec_Bit_t * vPhase )
{
Vec_Int_t * vLevel;
int i, k, Box;
Vec_WecForEachLevel( vBoxes, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, k )
Acec_TreeVerifyPhaseOne( p, vAdds, Box, vPhase );
}
/**Function*************************************************************
Synopsis [Creates polarity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
{
Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
Vec_Int_t * vLevel;
int i, k, Box;
Vec_WecForEachLevel( vBoxes, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, k )
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,
Vec_Bit_t * vPhase, Vec_Bit_t * vInvHadds, Vec_Bit_t * vVisit )
{
int k, iBox, iXor, Sign, fXorPhase, fPhaseThis;
assert( Node != 0 );
if ( Vec_BitEntry(vVisit, Node) )
{
//assert( Vec_BitEntry(vPhase, Node) == fPhase );
if ( Vec_BitEntry(vPhase, Node) != fPhase )
printf( "Phase check failed for node %d.\n", Node );
return;
}
Vec_BitWriteEntry( vVisit, Node, 1 );
if ( fPhase )
Vec_BitWriteEntry( vPhase, Node, fPhase );
iBox = Vec_IntEntry( vMap, Node );
if ( iBox == -1 )
return;
assert( Node == Vec_IntEntry( vAdds, 6*iBox+4 ) );
iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
Sign = Vec_IntEntry( vAdds, 6*iBox+5 );
fXorPhase = ((Sign >> 3) & 1);
if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
{
fPhase ^= ((Sign >> 2) & 1);
// remember complemented HADD
if ( fPhase )
Vec_BitWriteEntry( vInvHadds, iBox, 1 );
}
for ( k = 0; k < 3; k++ )
{
int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
if ( iObj == 0 )
continue;
fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
fXorPhase ^= fPhaseThis;
Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis, vPhase, vInvHadds, vVisit );
}
if ( Vec_BitEntry(vVisit, iXor) )
{
//assert( Vec_BitEntry(vPhase, iXor) == fXorPhase );
if ( Vec_BitEntry(vPhase, iXor) != fXorPhase )
printf( "Phase check failed for XOR %d.\n", iXor );
return;
}
if ( fXorPhase )
Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
}
void Acec_TreePhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes,
Vec_Wec_t * vLeaves, Vec_Wec_t * vRoots,
Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits, Vec_Bit_t * vInvHadds )
{
Vec_Int_t * vMap = Acec_TreeCarryMap( p, vAdds, vBoxes );
Vec_Bit_t * vPhase = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vVisit = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vLevel;
int i, k, iObj;
Vec_WecForEachLevelReverse( vRoots, vLevel, i )
{
Vec_IntForEachEntry( vLevel, iObj, k )
{
int fFadd = Abc_LitIsCompl(iObj);
int fCout = Abc_LitIsCompl(Abc_Lit2Var(iObj));
int Node = Abc_Lit2Var(Abc_Lit2Var(iObj));
if ( !fCout )
continue;
Acec_TreePhases_rec( p, vAdds, vMap, Node, fFadd, vPhase, vInvHadds, vVisit );
}
}
Vec_IntFree( vMap );
Vec_BitFree( vVisit );
Acec_TreeVerifyPhases( p, vAdds, vBoxes, vPhase );
// create leaves
Vec_WecForEachLevel( vLeaves, vLevel, i )
Vec_IntForEachEntry( vLevel, iObj, k )
Vec_WecPush( vLeafLits, i, Abc_Var2Lit(iObj, Vec_BitEntry(vPhase, iObj)) );
// add constants
Vec_WecForEachLevel( vBoxes, vLevel, i )
Vec_IntForEachEntry( vLevel, iObj, k )
if ( Vec_BitEntry(vInvHadds, iObj) )
Vec_WecPush( vLeafLits, i, 1 );
// create roots
Vec_WecForEachLevel( vRoots, vLevel, i )
Vec_IntForEachEntry( vLevel, iObj, k )
iObj >>= 2, Vec_WecPush( vRootLits, i, Abc_Var2Lit(iObj, Vec_BitEntry(vPhase, iObj)) );
// cleanup
Vec_BitFree( vPhase );
}
/**Function*************************************************************
Synopsis [Derives one adder tree.]
@ -564,25 +446,69 @@ void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
//Acec_PrintRootLits( pBox->vRoots );
}
int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
{
int k, Box, Rank, MaxRank = 0;
Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
MaxRank = Abc_MaxInt( MaxRank, Rank );
return MaxRank;
}
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 * 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;
Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
pBox->pGia = p;
pBox->pGia = p;
pBox->vAdds = Vec_WecStart( MaxRank + 1 );
pBox->vLeafLits = Vec_WecStart( MaxRank + 1 );
pBox->vRootLits = Vec_WecStart( MaxRank + 2 );
pBox->vAdds = Vec_WecStart( MaxRank + 1 );
pBox->vLeafs = Vec_WecStart( MaxRank + 1 );
pBox->vRoots = Vec_WecStart( MaxRank + 2 );
// 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 );
}
// sort each level
Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
Vec_IntSort( vLevel, 0 );
Acec_TreeInsOuts( p, vAdds, vTree, pBox->vAdds, pBox->vLeafs, pBox->vRoots );
pBox->vLeafLits = Vec_WecStart( Vec_WecSize(pBox->vLeafs) );
pBox->vRootLits = Vec_WecStart( Vec_WecSize(pBox->vRoots) );
pBox->vInvHadds = Vec_BitStart( Vec_IntSize(vAdds)/6 );
Acec_TreePhases( p, vAdds, pBox->vAdds, pBox->vLeafs, pBox->vRoots, pBox->vLeafLits, pBox->vRootLits, pBox->vInvHadds );
// set phases
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 );
Acec_TreeVerifyPhases( p, vAdds, pBox->vAdds );
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_BitFree( vIsLeaf );
Vec_BitFree( vIsRoot );
// sort each level
Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
Vec_IntSort( vLevel, 0 );
Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
Vec_IntSort( vLevel, 0 );
return pBox;
}
void Acec_CreateBoxTest( Gia_Man_t * p )
@ -641,7 +567,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;