From e9566a1e3db178a6111d227439354fcbb935ffa7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 29 Jan 2017 13:37:29 -0800 Subject: Updates to arithmetic verification. --- src/base/wlc/wlcReadVer.c | 1 + src/proof/acec/acecCore.c | 18 ++-- src/proof/acec/acecInt.h | 2 +- src/proof/acec/acecTree.c | 37 ++++++- src/proof/acec/acecXor.c | 238 ++++++++++++++++++++-------------------------- 5 files changed, 153 insertions(+), 143 deletions(-) diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index e4a65ecf..16de4943 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -429,6 +429,7 @@ char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p ) Vec_Str_t * vStr = Vec_StrAlloc( 1000 ); Vec_IntForEachEntry( p->vInits, Value, i ) { + char * pname = Wlc_ObjName( p, Value ); if ( Value < 0 ) { for ( k = 0; k < -Value; k++ ) diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c index a2341704..1a575fbe 100644 --- a/src/proof/acec/acecCore.c +++ b/src/proof/acec/acecCore.c @@ -319,7 +319,7 @@ void Vec_IntInsertOrder( Vec_Int_t * vLits, Vec_Int_t * vClasses, int Lit, int C void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses ) { Vec_Int_t * vLevel1, * vLevel2; - int i, k, Prev, This, Entry; + int i, k, Prev, This, Entry, Counter = 0; Vec_WecForEachLevel( vLits, vLevel1, i ) { if ( i == Vec_WecSize(vLits) - 1 ) @@ -347,8 +347,10 @@ void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses ) assert( Vec_IntSize(vLevel1) == Vec_IntSize(vLevel2) ); assert( Vec_IntSize(Vec_WecEntry(vLits, i+1)) == Vec_IntSize(Vec_WecEntry(vClasses, i+1)) ); + Counter++; } } + printf( "Moved %d pairs of PPs to normalize the matrix.\n", Counter ); } void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 ) @@ -490,12 +492,14 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars ) Gia_Man_t * pMiter; Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1; Cec_ParCec_t ParsCec, * pCecPars = &ParsCec; - 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, 0, 0, pPars->fVerbose ); - Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose ); - Vec_BitFreeP( &vIgnore0 ); - Vec_BitFreeP( &vIgnore1 ); +// 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, 0, 0, pPars->fVerbose ); +// Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose ); +// Vec_BitFreeP( &vIgnore0 ); +// Vec_BitFreeP( &vIgnore1 ); + Acec_Box_t * pBox0 = Acec_ProduceBox( pGia0, pPars->fVerbose ); + Acec_Box_t * pBox1 = Acec_ProduceBox( pGia1, pPars->fVerbose ); 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 diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index 47a32e78..381ab8d1 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -88,7 +88,7 @@ extern void Acec_BoxFreeP( Acec_Box_t ** ppBox ); extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ); extern Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose ); /*=== acecUtil.c ========================================================*/ -extern Acec_Box_t * Acec_DetectXorTrees( Gia_Man_t * p, int fVerbose ); +extern Acec_Box_t * Acec_ProduceBox( Gia_Man_t * p, int fVerbose ); diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c index 330a5d58..ab17d7b9 100644 --- a/src/proof/acec/acecTree.c +++ b/src/proof/acec/acecTree.c @@ -333,6 +333,37 @@ void Acec_TreeVerifyPhases2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxe Vec_BitFree( vPhase ); Vec_BitFree( vRoots ); } +void Acec_TreeVerifyConnections( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes ) +{ + Vec_Int_t * vCounts = Vec_IntStartFull( Gia_ManObjNum(p) ); + Vec_Int_t * vLevel; + int i, k, n, Box; + // mark outputs + Vec_WecForEachLevel( vBoxes, vLevel, i ) + Vec_IntForEachEntry( vLevel, Box, k ) + { + Vec_IntWriteEntry( vCounts, Vec_IntEntry( vAdds, 6*Box+3 ), 0 ); + Vec_IntWriteEntry( vCounts, Vec_IntEntry( vAdds, 6*Box+4 ), 0 ); + } + // count fanouts + Vec_WecForEachLevel( vBoxes, vLevel, i ) + Vec_IntForEachEntry( vLevel, Box, k ) + for ( n = 0; n < 3; n++ ) + if ( Vec_IntEntry( vCounts, Vec_IntEntry(vAdds, 6*Box+n) ) != -1 ) + Vec_IntAddToEntry( vCounts, Vec_IntEntry(vAdds, 6*Box+n), 1 ); + // print out + printf( "The adder tree has %d internal cut points. ", Vec_IntCountLarger(vCounts, -1) ); + if ( Vec_IntCountLarger(vCounts, 1) == 0 ) + printf( "There is no internal fanouts.\n" ); + else + { + printf( "These %d points have more than one fanout:\n", Vec_IntCountLarger(vCounts, 1) ); + Vec_IntForEachEntry( vCounts, Box, i ) + if ( Box > 1 ) + printf( "Node %d(lev %d) has fanout %d.\n", i, Gia_ObjLevelId(p, i), Box ); + } + Vec_IntFree( vCounts ); +} /**Function************************************************************* @@ -534,7 +565,7 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p ) SideEffects [] SeeAlso [] - +` ***********************************************************************/ void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds ) { @@ -560,6 +591,10 @@ void Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds ) Vec_WecPrintLits( pBox->vLeafLits ); printf( "Outputs:\n" ); Vec_WecPrintLits( pBox->vRootLits ); +// printf( "Node %d has level %d.\n", 3715, Gia_ObjLevelId(pBox->pGia, 3715) ); +// printf( "Node %d has level %d.\n", 167, Gia_ObjLevelId(pBox->pGia, 167) ); +// printf( "Node %d has level %d.\n", 278, Gia_ObjLevelId(pBox->pGia, 278) ); +// printf( "Node %d has level %d.\n", 597, Gia_ObjLevelId(pBox->pGia, 597) ); } int Acec_CreateBoxMaxRank( Vec_Int_t * vTree ) diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c index ae5aeff7..acbde1a0 100644 --- a/src/proof/acec/acecXor.c +++ b/src/proof/acec/acecXor.c @@ -44,43 +44,43 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Vec_Int_t * Acec_OrderXorRoots( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Wec_t * vXorTrees, Vec_Int_t * vMap ) +Vec_Int_t * Acec_OrderTreeRoots( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks ) { - Vec_Int_t * vOrder = Vec_IntAlloc( Vec_WecSize(vXorTrees) ); - Vec_Int_t * vReMap = Vec_IntStartFull( Vec_WecSize(vXorTrees) ); + Vec_Int_t * vOrder = Vec_IntAlloc( Vec_IntSize(vXorRoots) ); + Vec_Int_t * vMove = Vec_IntStartFull( Vec_IntSize(vXorRoots) ); int i, k, Entry, This; // iterate through adders and for each try mark the next one for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) { int Node = Vec_IntEntry(vAdds, 6*i+4); - if ( Vec_IntEntry(vMap, Node) == -1 ) + if ( Vec_IntEntry(vRanks, Node) == -1 ) continue; for ( k = 0; k < 3; k++ ) { int Fanin = Vec_IntEntry(vAdds, 6*i+k); - if ( Vec_IntEntry(vMap, Fanin) == -1 ) + if ( Vec_IntEntry(vRanks, Fanin) == -1 ) continue; - //printf( "%4d: %2d -> %2d\n", Node, Vec_IntEntry(vMap, Node), Vec_IntEntry(vMap, Fanin) ); - Vec_IntWriteEntry( vReMap, Vec_IntEntry(vMap, Node), Vec_IntEntry(vMap, Fanin) ); + //printf( "%4d: %2d -> %2d\n", Node, Vec_IntEntry(vRanks, Node), Vec_IntEntry(vRanks, Fanin) ); + Vec_IntWriteEntry( vMove, Vec_IntEntry(vRanks, Node), Vec_IntEntry(vRanks, Fanin) ); } } -//Vec_IntPrint( vReMap ); +//Vec_IntPrint( vMove ); // find reodering - Vec_IntForEachEntry( vReMap, Entry, i ) - if ( Entry == -1 && Vec_IntFind(vReMap, i) >= 0 ) + Vec_IntForEachEntry( vMove, Entry, i ) + if ( Entry == -1 && Vec_IntFind(vMove, i) >= 0 ) break; - assert( i < Vec_IntSize(vReMap) ); + assert( i < Vec_IntSize(vMove) ); while ( 1 ) { Vec_IntPush( vOrder, Vec_IntEntry(vXorRoots, i) ); Entry = i; - Vec_IntForEachEntry( vReMap, This, i ) + Vec_IntForEachEntry( vMove, This, i ) if ( This == Entry ) break; - if ( i == Vec_IntSize(vReMap) ) + if ( i == Vec_IntSize(vMove) ) break; } - Vec_IntFree( vReMap ); + Vec_IntFree( vMove ); //Vec_IntPrint( vOrder ); return vOrder; } @@ -96,27 +96,24 @@ Vec_Int_t * Acec_OrderXorRoots( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vX SeeAlso [] ***********************************************************************/ -// marks nodes appearing as fanins to XORs -Vec_Bit_t * Acec_MapXorIns( Gia_Man_t * p, Vec_Int_t * vXors ) +// marks XOR outputs +Vec_Bit_t * Acec_MapXorOuts( Gia_Man_t * p, Vec_Int_t * vXors ) { Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i; for ( i = 0; 4*i < Vec_IntSize(vXors); i++ ) - { - Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+1), 1 ); - Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+2), 1 ); - Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+3), 1 ); - } + Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i), 1 ); return vMap; } -// marks nodes having XOR cuts -Vec_Bit_t * Acec_MapXorOuts( Gia_Man_t * p, Vec_Int_t * vXors ) +// marks XOR outputs participating in trees +Vec_Bit_t * Acec_MapXorOuts2( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vRanks ) { Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i; for ( i = 0; 4*i < Vec_IntSize(vXors); i++ ) - Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i), 1 ); + if ( Vec_IntEntry(vRanks, Vec_IntEntry(vXors, 4*i)) != -1 ) + Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i), 1 ); return vMap; } -// marks nodes appearing as outputs of MAJs +// marks MAJ outputs Vec_Bit_t * Acec_MapMajOuts( Gia_Man_t * p, Vec_Int_t * vAdds ) { Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i; @@ -124,25 +121,24 @@ Vec_Bit_t * Acec_MapMajOuts( Gia_Man_t * p, Vec_Int_t * vAdds ) Vec_BitWriteEntry( vMap, Vec_IntEntry(vAdds, 6*i+4), 1 ); return vMap; } -// maps MAJ outputs into their FAs and HAs -Vec_Int_t * Acec_MapMajOutsToAdds( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vXorOuts, Vec_Int_t * vMapRank ) +// marks MAJ outputs participating in trees +Vec_Int_t * Acec_MapMajOuts2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vRanks ) { Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); int i; for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + if ( Vec_IntEntry(vRanks, Vec_IntEntry(vAdds, 6*i+4)) != -1 ) + Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*i+4), i ); + return vMap; +} +// marks nodes appearing as fanins to XORs +Vec_Bit_t * Acec_MapXorIns( Gia_Man_t * p, Vec_Int_t * vXors ) +{ + Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i; + for ( i = 0; 4*i < Vec_IntSize(vXors); i++ ) { - int Xor = Vec_IntEntry(vAdds, 6*i+3); - int Maj = Vec_IntEntry(vAdds, 6*i+4); - if ( Vec_IntEntry(vMap, Maj) >= 0 ) - { - int i2 = Vec_IntEntry(vMap, Maj); - int Xor2 = Vec_IntEntry(vAdds, 6*i2+3); - int Maj2 = Vec_IntEntry(vAdds, 6*i2+4); - printf( "*** Node %d has two MAJ adder drivers: %d%s (%d rank %d) and %d%s (%d rank %d).\n", - Maj, - i, Vec_IntEntry(vAdds, 6*i+2) ? "":"*", Vec_BitEntry(vXorOuts, Xor), Vec_IntEntry(vMapRank, Xor), - i2, Vec_IntEntry(vAdds, 6*i2+2) ? "":"*", Vec_BitEntry(vXorOuts, Xor2), Vec_IntEntry(vMapRank, Xor2) ); - } - Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*i+4), i ); + Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+1), 1 ); + Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+2), 1 ); + Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+3), 1 ); } return vMap; } @@ -159,103 +155,83 @@ Vec_Int_t * Acec_FindXorRoots( Gia_Man_t * p, Vec_Int_t * vXors ) return vXorRoots; } // collects XOR trees belonging to each of XOR roots -Vec_Wec_t * Acec_FindXorTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRoots, Vec_Int_t ** pvMap ) +Vec_Int_t * Acec_RankTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRoots ) { Vec_Int_t * vDoubles = Vec_IntAlloc( 100 ); - Vec_Wec_t * vXorTrees = Vec_WecStart( Vec_IntSize(vXorRoots) ); - Vec_Int_t * vLevel; int i, k, Entry; - // map roots into their classes - Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); + // map roots into their ranks + Vec_Int_t * vRanks = Vec_IntStartFull( Gia_ManObjNum(p) ); Vec_IntForEachEntry( vXorRoots, Entry, i ) - { - Vec_IntWriteEntry( vMap, Entry, i ); - Vec_WecPush( vXorTrees, i, Entry ); - } - // map nodes into their classes + Vec_IntWriteEntry( vRanks, Entry, i ); + // map nodes into their ranks for ( i = Vec_IntSize(vXors)/4 - 1; i >= 0; i-- ) { int Root = Vec_IntEntry( vXors, 4*i ); - int Repr = Vec_IntEntry( vMap, Root ); - //assert( Repr != -1 ); - if ( Repr == -1 ) + int Rank = Vec_IntEntry( vRanks, Root ); + // skip XORs that are not part of any tree + if ( Rank == -1 ) continue; + // iterate through XOR inputs for ( k = 1; k < 4; k++ ) { int Node = Vec_IntEntry( vXors, 4*i+k ); - if ( Node == 0 ) + if ( Node == 0 ) // HA continue; - Entry = Vec_IntEntry( vMap, Node ); - if ( Entry == Repr ) + Entry = Vec_IntEntry( vRanks, Node ); + if ( Entry == Rank ) // the same tree continue; if ( Entry == -1 ) - { - Vec_IntWriteEntry( vMap, Node, Repr ); - Vec_WecPush( vXorTrees, Repr, Node ); - continue; - } - //printf( "Node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Repr ); - Vec_IntPushUnique( Vec_WecEntry(vXorTrees, Entry), Node ); - Vec_IntPush( vDoubles, Node ); + Vec_IntWriteEntry( vRanks, Node, Rank ); + else + Vec_IntPush( vDoubles, Node ); + //if ( Entry != -1 ) + //printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank ); } } - // clean map + // remove duplicated entries Vec_IntForEachEntry( vDoubles, Entry, i ) - Vec_IntWriteEntry( vMap, Entry, -1 ); + Vec_IntWriteEntry( vRanks, Entry, -1 ); Vec_IntFree( vDoubles ); - // sort nodes - Vec_WecForEachLevel( vXorTrees, vLevel, i ) - Vec_IntSort( vLevel, 0 ); - if ( pvMap ) - *pvMap = vMap; - else - Vec_IntFree( vMap ); - return vXorTrees; + return vRanks; } // collects leaves of each XOR tree -Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vAdds, Vec_Wec_t * vXorTrees, Vec_Int_t * vMap, Vec_Wec_t ** pvAddBoxes ) +Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks, Vec_Wec_t ** pvAddBoxes ) { - Vec_Bit_t * vMapXorOuts = Acec_MapXorOuts( p, vXors ); - Vec_Int_t * vMapMajOuts = Acec_MapMajOutsToAdds( p, vAdds, vMapXorOuts, vMap ); - Vec_Wec_t * vXorLeaves = Vec_WecStart( Vec_WecSize(vXorTrees) ); + Vec_Bit_t * vMapXors = Acec_MapXorOuts2( p, vXors, vRanks ); + Vec_Int_t * vMapMajs = Acec_MapMajOuts2( p, vAdds, vRanks ); + Vec_Wec_t * vXorLeaves = Vec_WecStart( Vec_IntSize(vXorRoots) ); + Vec_Wec_t * vAddBoxes = Vec_WecStart( Vec_IntSize(vXorRoots) ); int i, k; - if ( pvAddBoxes ) - *pvAddBoxes = Vec_WecStart( Vec_WecSize(vXorTrees) ); - // collect leaves for ( i = 0; 4*i < Vec_IntSize(vXors); i++ ) { int Xor = Vec_IntEntry(vXors, 4*i); + int Rank = Vec_IntEntry(vRanks, Xor); + if ( Rank == -1 ) + continue; for ( k = 1; k < 4; k++ ) { - int Node = Vec_IntEntry(vXors, 4*i+k); - if ( Node == 0 ) + int Fanin = Vec_IntEntry(vXors, 4*i+k); + if ( Fanin == 0 ) continue; - if ( Vec_BitEntry(vMapXorOuts, Node) || Vec_IntEntry(vMap, Xor) == -1 ) + if ( Vec_BitEntry(vMapXors, Fanin) ) + { + assert( Rank == Vec_IntEntry(vRanks, Fanin) ); continue; - if ( Vec_IntEntry(vMapMajOuts, Node) == -1 ) // no maj driver - Vec_WecPush( vXorLeaves, Vec_IntEntry(vMap, Xor), Node ); - else if ( pvAddBoxes && Vec_IntEntry(vMap, Xor) > 0 ) // save adder box - Vec_WecPush( *pvAddBoxes, Vec_IntEntry(vMap, Xor)-1, Vec_IntEntry(vMapMajOuts, Node) ); + } + if ( Vec_IntEntry(vMapMajs, Fanin) == -1 ) // no adder driving this input + Vec_WecPush( vXorLeaves, Rank, Fanin ); + else if ( Vec_IntEntry(vRanks, Xor) > 0 ) // save adder box + Vec_WecPush( vAddBoxes, Rank-1, Vec_IntEntry(vMapMajs, Fanin) ); } } -/* + Vec_BitFree( vMapXors ); + Vec_IntFree( vMapMajs ); if ( pvAddBoxes ) - { - Vec_Int_t * vLevel; - //Vec_WecPrint( *pvAddBoxes, 0 ); - Vec_WecForEachLevelReverse( *pvAddBoxes, vLevel, i ) - if ( Vec_IntSize(vLevel) > 0 ) - break; - Vec_WecShrink( *pvAddBoxes, i+1 ); - //Vec_WecPrint( *pvAddBoxes, 0 ); - } -*/ - Vec_BitFree( vMapXorOuts ); - Vec_IntFree( vMapMajOuts ); + *pvAddBoxes = vAddBoxes; return vXorLeaves; } -Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBoxes, Vec_Wec_t * vXorTrees, Vec_Wec_t * vXorLeaves ) +Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBoxes, Vec_Wec_t * vXorLeaves, Vec_Int_t * vXorRoots ) { extern Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes ); extern void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase, Vec_Bit_t * vVisit ); @@ -275,8 +251,8 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox pBox->vLeafLits = Vec_WecStart( MaxRank + 0 ); pBox->vRootLits = Vec_WecStart( MaxRank + 0 ); - assert( Vec_WecSize(vAddBoxes) == Vec_WecSize(vXorTrees) ); assert( Vec_WecSize(vAddBoxes) == Vec_WecSize(vXorLeaves) ); + assert( Vec_WecSize(vAddBoxes) == Vec_IntSize(vXorRoots) ); // collect boxes; mark inputs/outputs Vec_WecForEachLevel( pBox->vAdds, vLevel, i ) @@ -332,12 +308,7 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox Vec_IntPush( vLevel, Abc_Var2Lit(Node, 0) ); } vLevel = Vec_WecEntry( pBox->vRootLits, Vec_WecSize(pBox->vRootLits)-1 ); - vLevel2 = Vec_WecEntry( vXorTrees, Vec_WecSize(vXorTrees)-1 ); - Vec_IntClear( vLevel ); - if ( Vec_IntSize(vLevel) == 0 && Vec_IntSize(vLevel2) > 0 ) - { - Vec_IntPush( vLevel, Abc_Var2Lit(Vec_IntEntryLast(vLevel2), 0) ); - } + Vec_IntFill( vLevel, 1, Abc_Var2Lit(Vec_IntEntryLast(vXorRoots), 0) ); // sort each level Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i ) @@ -347,50 +318,49 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox return pBox; } -Acec_Box_t * Acec_DetectXorTrees( Gia_Man_t * p, int fVerbose ) +Acec_Box_t * Acec_ProduceBox( Gia_Man_t * p, int fVerbose ) { + extern void Acec_TreeVerifyConnections( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes ); + abctime clk = Abc_Clock(); Acec_Box_t * pBox = NULL; Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, 0 ); - Vec_Int_t * vMap, * vXorRootsNew; - Vec_Int_t * vXorRoots = Acec_FindXorRoots( p, vXors ); - Vec_Wec_t * vXorTrees = Acec_FindXorTrees( p, vXors, vXorRoots, &vMap ); + Vec_Int_t * vTemp, * vXorRoots = Acec_FindXorRoots( p, vXors ); + Vec_Int_t * vRanks = Acec_RankTrees( p, vXors, vXorRoots ); Vec_Wec_t * vXorLeaves, * vAddBoxes = NULL; + Gia_ManLevelNum(p); + //Ree_ManPrintAdders( vAdds, 1 ); printf( "Detected %d full-adders and %d half-adders. Found %d XOR-cuts. ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); -// printf( "XOR roots: \n" ); -// Vec_IntPrint( vXorRoots ); -// Vec_WecPrint( vXorTrees, 0 ); + vXorRoots = Acec_OrderTreeRoots( p, vAdds, vTemp = vXorRoots, vRanks ); + Vec_IntFree( vTemp ); + Vec_IntFree( vRanks ); - vXorRootsNew = Acec_OrderXorRoots( p, vAdds, vXorRoots, vXorTrees, vMap ); - Vec_IntFree( vXorRoots ); - Vec_WecFree( vXorTrees ); - Vec_IntFree( vMap ); + vRanks = Acec_RankTrees( p, vXors, vXorRoots ); + vXorLeaves = Acec_FindXorLeaves( p, vXors, vAdds, vXorRoots, vRanks, &vAddBoxes ); + Vec_IntFree( vRanks ); - vXorRoots = vXorRootsNew; vXorRootsNew = NULL; - vXorTrees = Acec_FindXorTrees( p, vXors, vXorRoots, &vMap ); - vXorLeaves = Acec_FindXorLeaves( p, vXors, vAdds, vXorTrees, vMap, &vAddBoxes ); + //printf( "XOR roots after reordering: \n" ); + //Vec_IntPrint( vXorRoots ); + //printf( "XOR leaves: \n" ); + //Vec_WecPrint( vXorLeaves, 0 ); + //printf( "Adder boxes: \n" ); + //Vec_WecPrint( vAddBoxes, 0 ); - printf( "XOR roots: \n" ); - Vec_IntPrint( vXorRoots ); - printf( "XOR leaves: \n" ); - Vec_WecPrint( vXorLeaves, 0 ); - printf( "Adder boxes: \n" ); - Vec_WecPrint( vAddBoxes, 0 ); + Acec_TreeVerifyConnections( p, vAdds, vAddBoxes ); - pBox = Acec_FindBox( p, vAdds, vAddBoxes, vXorTrees, vXorLeaves ); + pBox = Acec_FindBox( p, vAdds, vAddBoxes, vXorLeaves, vXorRoots ); + //Vec_WecFree( vAddBoxes ); - Acec_TreePrintBox( pBox, vAdds ); + if ( fVerbose ) + Acec_TreePrintBox( pBox, vAdds ); Vec_IntFree( vXorRoots ); - Vec_WecFree( vXorTrees ); Vec_WecFree( vXorLeaves ); - //Vec_WecFree( vAddBoxes ); - Vec_IntFree( vMap ); Vec_IntFree( vXors ); Vec_IntFree( vAdds ); -- cgit v1.2.3