From 9171bb32ad332d2b76e3c85ff64308065b89367d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 28 Jan 2017 17:04:22 -0800 Subject: Updates to arithmetic verification. --- abclib.dsp | 8 + src/proof/acec/acecInt.h | 9 + src/proof/acec/acecMult.c | 1 + src/proof/acec/acecTree.c | 12 +- src/proof/acec/acecXor.c | 407 +++++++++++++++++++++++++++++++++++++++++++++ src/proof/acec/module.make | 3 +- 6 files changed, 430 insertions(+), 10 deletions(-) create mode 100644 src/proof/acec/acecXor.c diff --git a/abclib.dsp b/abclib.dsp index 6da7e2a2..cbed067a 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -1963,6 +1963,10 @@ SOURCE=.\src\sat\xsat\xsatCnfReader.c # End Source File # Begin Source File +SOURCE=.\src\sat\xsat\xsatFloat.h +# End Source File +# Begin Source File + SOURCE=.\src\sat\xsat\xsatHeap.h # End Source File # Begin Source File @@ -5553,6 +5557,10 @@ SOURCE=.\src\proof\acec\acecTree.c SOURCE=.\src\proof\acec\acecUtil.c # End Source File +# Begin Source File + +SOURCE=.\src\proof\acec\acecXor.c +# End Source File # End Group # End Group # End Group diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index b8ec2455..47a32e78 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -56,6 +56,12 @@ struct Acec_Box_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +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)); } + //////////////////////////////////////////////////////////////////////// /// ITERATORS /// //////////////////////////////////////////////////////////////////////// @@ -75,11 +81,14 @@ extern void Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] ); extern Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll ); /*=== acecTree.c ========================================================*/ extern void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds ); +extern void Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds ); extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose ); extern void Acec_BoxFreeP( Acec_Box_t ** ppBox ); /*=== acecUtil.c ========================================================*/ 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 ); diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c index d868c399..ba9405ac 100644 --- a/src/proof/acec/acecMult.c +++ b/src/proof/acec/acecMult.c @@ -499,6 +499,7 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p ) { if ( Truth == Saved[i] || Truth == ~Saved[i] ) { + //printf( "*** Node %d is PP with support %d.\n", iObj, Vec_IntSize(vSupp) ); Acec_MultFindPPs_rec( p, iObj, vBold ); nProds++; break; diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c index 2461c89b..330a5d58 100644 --- a/src/proof/acec/acecTree.c +++ b/src/proof/acec/acecTree.c @@ -27,12 +27,6 @@ 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 /// //////////////////////////////////////////////////////////////////////// @@ -558,7 +552,7 @@ void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds ) printf( " }\n" ); } } -void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds ) +void Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds ) { printf( "Adders:\n" ); Acec_PrintAdders( pBox->vAdds, vAdds ); @@ -703,7 +697,7 @@ void Acec_CreateBoxTest( Gia_Man_t * p ) printf( "Processing tree %d: Ranks = %d. Adders = %d. Leaves = %d. Roots = %d.\n", i, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) ); - Acec_PrintBox( pBox, vAdds ); + Acec_TreePrintBox( pBox, vAdds ); Acec_BoxFreeP( &pBox ); } @@ -737,7 +731,7 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, 0, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) ); if ( pBox && fVerbose ) - Acec_PrintBox( pBox, vAdds ); + Acec_TreePrintBox( pBox, vAdds ); //Acec_PrintAdders( pBox0->vAdds, vAdds ); //Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits ); Vec_WecFreeP( &vTrees ); diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c new file mode 100644 index 00000000..ae5aeff7 --- /dev/null +++ b/src/proof/acec/acecXor.c @@ -0,0 +1,407 @@ +/**CFile**************************************************************** + + FileName [acecXor.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Detection of XOR trees.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecXor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" +#include "misc/vec/vecWec.h" +#include "misc/extra/extra.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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 * vOrder = Vec_IntAlloc( Vec_WecSize(vXorTrees) ); + Vec_Int_t * vReMap = Vec_IntStartFull( Vec_WecSize(vXorTrees) ); + 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 ) + continue; + for ( k = 0; k < 3; k++ ) + { + int Fanin = Vec_IntEntry(vAdds, 6*i+k); + if ( Vec_IntEntry(vMap, 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) ); + } + } +//Vec_IntPrint( vReMap ); + // find reodering + Vec_IntForEachEntry( vReMap, Entry, i ) + if ( Entry == -1 && Vec_IntFind(vReMap, i) >= 0 ) + break; + assert( i < Vec_IntSize(vReMap) ); + while ( 1 ) + { + Vec_IntPush( vOrder, Vec_IntEntry(vXorRoots, i) ); + Entry = i; + Vec_IntForEachEntry( vReMap, This, i ) + if ( This == Entry ) + break; + if ( i == Vec_IntSize(vReMap) ) + break; + } + Vec_IntFree( vReMap ); +//Vec_IntPrint( vOrder ); + return vOrder; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +// 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++ ) + { + 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; +} +// marks nodes having XOR cuts +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 ); + return vMap; +} +// marks nodes appearing as outputs of MAJs +Vec_Bit_t * Acec_MapMajOuts( Gia_Man_t * p, Vec_Int_t * vAdds ) +{ + Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i; + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + 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 ) +{ + Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); int i; + for ( i = 0; 6*i < Vec_IntSize(vAdds); 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 ); + } + return vMap; +} +// collects XOR roots (XOR nodes not appearing as fanins of other XORs) +Vec_Int_t * Acec_FindXorRoots( Gia_Man_t * p, Vec_Int_t * vXors ) +{ + Vec_Bit_t * vMapXorIns = Acec_MapXorIns( p, vXors ); + Vec_Int_t * vXorRoots = Vec_IntAlloc( 100 ); int i; + for ( i = 0; 4*i < Vec_IntSize(vXors); i++ ) + if ( !Vec_BitEntry(vMapXorIns, Vec_IntEntry(vXors, 4*i)) ) + Vec_IntPushUniqueOrder( vXorRoots, Vec_IntEntry(vXors, 4*i) ); + Vec_BitFree( vMapXorIns ); +//Vec_IntRemove( vXorRoots, 54 ); + 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 * 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) ); + Vec_IntForEachEntry( vXorRoots, Entry, i ) + { + Vec_IntWriteEntry( vMap, Entry, i ); + Vec_WecPush( vXorTrees, i, Entry ); + } + // map nodes into their classes + 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 ) + continue; + for ( k = 1; k < 4; k++ ) + { + int Node = Vec_IntEntry( vXors, 4*i+k ); + if ( Node == 0 ) + continue; + Entry = Vec_IntEntry( vMap, Node ); + if ( Entry == Repr ) + 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 ); + } + } + // clean map + Vec_IntForEachEntry( vDoubles, Entry, i ) + Vec_IntWriteEntry( vMap, 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; +} +// 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_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) ); + 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); + for ( k = 1; k < 4; k++ ) + { + int Node = Vec_IntEntry(vXors, 4*i+k); + if ( Node == 0 ) + continue; + if ( Vec_BitEntry(vMapXorOuts, Node) || Vec_IntEntry(vMap, Xor) == -1 ) + 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 ( 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 ); + 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 ) +{ + 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 ); + extern void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes ); + extern void Acec_TreeVerifyPhases2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes ); + + int MaxRank = Vec_WecSize( vAddBoxes ); + 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, * vLevel2, * vMap; + int i, j, k, Box, Node; + + Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 ); + pBox->pGia = p; + pBox->vAdds = vAddBoxes; // Vec_WecDup( vAddBoxes ); + 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) ); + + // collect boxes; mark inputs/outputs + Vec_WecForEachLevel( pBox->vAdds, vLevel, i ) + Vec_IntForEachEntry( vLevel, Box, k ) + { + 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 ); + + // set phases starting from roots + vMap = Acec_TreeCarryMap( p, vAdds, pBox->vAdds ); + Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i ) + Vec_IntForEachEntry( vLevel, Box, k ) + if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) ) + { + //printf( "Pushing phase of output %d of box %d\n", Vec_IntEntry(vAdds, 6*Box+4), Box ); + 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( 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 ); + + // collect last bit + vLevel = Vec_WecEntry( pBox->vLeafLits, Vec_WecSize(pBox->vLeafLits)-1 ); + vLevel2 = Vec_WecEntry( vXorLeaves, Vec_WecSize(vXorLeaves)-1 ); + if ( Vec_IntSize(vLevel) == 0 && Vec_IntSize(vLevel2) > 0 ) + { + Vec_IntForEachEntry( vLevel2, Node, k ) + 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) ); + } + + // sort each level + Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i ) + Vec_IntSort( vLevel, 0 ); + Vec_WecForEachLevel( pBox->vRootLits, vLevel, i ) + Vec_IntSort( vLevel, 1 ); + return pBox; +} + +Acec_Box_t * Acec_DetectXorTrees( Gia_Man_t * p, int fVerbose ) +{ + 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_Wec_t * vXorLeaves, * vAddBoxes = NULL; + + //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 ); + + vXorRootsNew = Acec_OrderXorRoots( p, vAdds, vXorRoots, vXorTrees, vMap ); + Vec_IntFree( vXorRoots ); + Vec_WecFree( vXorTrees ); + Vec_IntFree( vMap ); + + vXorRoots = vXorRootsNew; vXorRootsNew = NULL; + vXorTrees = Acec_FindXorTrees( p, vXors, vXorRoots, &vMap ); + vXorLeaves = Acec_FindXorLeaves( p, vXors, vAdds, vXorTrees, vMap, &vAddBoxes ); + + printf( "XOR roots: \n" ); + Vec_IntPrint( vXorRoots ); + printf( "XOR leaves: \n" ); + Vec_WecPrint( vXorLeaves, 0 ); + printf( "Adder boxes: \n" ); + Vec_WecPrint( vAddBoxes, 0 ); + + pBox = Acec_FindBox( p, vAdds, vAddBoxes, vXorTrees, vXorLeaves ); + + 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 ); + + return pBox; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make index dbf86ac2..f4c69892 100644 --- a/src/proof/acec/module.make +++ b/src/proof/acec/module.make @@ -14,4 +14,5 @@ SRC += src/proof/acec/acecCl.c \ src/proof/acec/acecPolyn.c \ src/proof/acec/acecSt.c \ src/proof/acec/acecTree.c \ - src/proof/acec/acecUtil.c + src/proof/acec/acecUtil.c \ + src/proof/acec/acecXor.c -- cgit v1.2.3