From 1bf289c774eca7ead1edfba51c0e86255e2730e7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 2 Dec 2016 21:12:57 -0800 Subject: Changes to arithmetic logic detection. --- abclib.dsp | 12 ++ src/proof/acec/acecCl.c | 55 +++++++++ src/proof/acec/acecCo.c | 146 +++++++++++++++++------ src/proof/acec/acecPa.c | 282 +++++++++++++++++++++++++++++++++++++++++++++ src/proof/acec/acecPool.c | 132 +++++++++++++++++++++ src/proof/acec/acecRe.c | 163 ++++++++++++++++++++++---- src/proof/acec/module.make | 5 +- 7 files changed, 736 insertions(+), 59 deletions(-) create mode 100644 src/proof/acec/acecCl.c create mode 100644 src/proof/acec/acecPa.c create mode 100644 src/proof/acec/acecPool.c diff --git a/abclib.dsp b/abclib.dsp index a098dfc2..8d33b15b 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -5411,6 +5411,10 @@ SOURCE=.\src\proof\acec\acec.h # End Source File # Begin Source File +SOURCE=.\src\proof\acec\acecCl.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\acec\acecCo.c # End Source File # Begin Source File @@ -5435,6 +5439,10 @@ SOURCE=.\src\proof\acec\acecOrder.c # End Source File # Begin Source File +SOURCE=.\src\proof\acec\acecPa.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\acec\acecPo.c # End Source File # Begin Source File @@ -5443,6 +5451,10 @@ SOURCE=.\src\proof\acec\acecPolyn.c # End Source File # Begin Source File +SOURCE=.\src\proof\acec\acecPool.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\acec\acecRe.c # End Source File # Begin Source File diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c new file mode 100644 index 00000000..32be3b30 --- /dev/null +++ b/src/proof/acec/acecCl.c @@ -0,0 +1,55 @@ +/**CFile**************************************************************** + + FileName [acecCl.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecCl.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 [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c index 1b73c36f..39f092b2 100644 --- a/src/proof/acec/acecCo.c +++ b/src/proof/acec/acecCo.c @@ -90,38 +90,30 @@ Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts ) +Vec_Wec_t * Gia_PolynComputeMap( Vec_Int_t * vAdds, int nObjs ) { - Vec_Int_t * vOrder = Vec_IntAlloc( 1000 ); - Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) ); - Vec_Int_t * vRoots = Vec_IntAlloc( 5 * Gia_ManCoNum(pGia) ); - Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) ); - Vec_Wec_t * vMap = Vec_WecStart( Gia_ManObjNum(pGia) ); - int i, k, Index, Driver, Entry1, Entry2 = -1; // map nodes driven by adders into adder indexes - for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ ) + Vec_Wec_t * vMap = Vec_WecStart( nObjs ); int i; + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) { - Entry1 = Vec_IntEntry( vAdds, 5*i + 3 ); - Entry2 = Vec_IntEntry( vAdds, 5*i + 4 ); + int Entry1 = Vec_IntEntry( vAdds, 6*i + 3 ); + int Entry2 = Vec_IntEntry( vAdds, 6*i + 4 ); Vec_WecPush( vMap, Entry1, i ); Vec_WecPush( vMap, Entry1, Entry2 ); Vec_WecPush( vMap, Entry2, i ); Vec_WecPush( vMap, Entry2, Entry1 ); } - // collect roots - Gia_ManForEachCoDriverId( pGia, Driver, i ) - { - Vec_IntPush( vRoots, Driver ); - Vec_BitWriteEntry( vIsRoot, Driver, 1 ); - } - // collect additional outputs - Vec_IntForEachEntry( vAddCos, Driver, i ) - { - Vec_IntPush( vRoots, Driver ); + return vMap; +} +Vec_Int_t * Gia_PolynCoreOrder_int( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Int_t * vRoots, Vec_Int_t ** pvIns ) +{ + Vec_Int_t * vOrder = Vec_IntAlloc( 1000 ); + Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) ); + int i, k, Index, Driver, Entry1, Entry2 = -1; + // mark roots + Vec_IntForEachEntry( vRoots, Driver, i ) Vec_BitWriteEntry( vIsRoot, Driver, 1 ); - } - // detect full adder tree - *pvOuts = Vec_IntDup( vRoots ); + // collect boxes while ( 1 ) { // iterate through boxes driving this one @@ -143,9 +135,9 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * Vec_IntRemove( vRoots, Entry1 ); Vec_IntRemove( vRoots, Entry2 ); // set new marks - Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 ); - Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 ); - Driver = Vec_IntEntry( vAdds, 5*Index + 2 ); + Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 ); + Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 ); + Driver = Vec_IntEntry( vAdds, 6*Index + 2 ); Vec_BitWriteEntry( vIsRoot, Entry1, 1 ); Vec_BitWriteEntry( vIsRoot, Entry2, 1 ); Vec_BitWriteEntry( vIsRoot, Driver, 1 ); @@ -158,17 +150,97 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * break; } // collect remaining leaves - Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 ) - if ( Driver ) - Vec_IntPush( vLeaves, i ); - *pvIns = vLeaves; - // cleanup + if ( pvIns ) + { + *pvIns = Vec_IntAlloc( Vec_BitSize(vIsRoot) ); + Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 ) + if ( Driver ) + Vec_IntPush( *pvIns, i ); + } Vec_BitFree( vIsRoot ); + return vOrder; +} +Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts ) +{ + Vec_Int_t * vOrder; + Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) ); + Vec_Int_t * vRoots = Vec_IntAlloc( Gia_ManCoNum(pGia) ); + int i, Driver; + // collect roots + Gia_ManForEachCoDriverId( pGia, Driver, i ) + Vec_IntPush( vRoots, Driver ); + // collect additional outputs + if ( vAddCos ) + Vec_IntForEachEntry( vAddCos, Driver, i ) + Vec_IntPush( vRoots, Driver ); + // remember roots + if ( pvOuts ) + *pvOuts = Vec_IntDup( vRoots ); + // create order + vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, pvIns ); Vec_IntFree( vRoots ); Vec_WecFree( vMap ); + printf( "Collected %d boxes.\n", Vec_IntSize(vOrder) ); return vOrder; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_PolyCollectRoots_rec( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots ) +{ + int k; + for ( k = 0; k < 3; k++ ) + { + int i, Index, Sum, Carry = Vec_IntEntry( vAdds, 6*iBox+k ); + Vec_Int_t * vLevel = Vec_WecEntry( vMap, Carry ); + if ( Carry == 0 ) + continue; + Vec_IntForEachEntryDouble( vLevel, Index, Sum, i ) + if ( Vec_IntEntry(vAdds, 6*Index+4) == Carry && !Vec_BitEntry(vMarks, Sum) ) + { + Vec_IntPush( vRoots, Sum ); + Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, Index, vRoots ); + } + } +} +void Gia_PolyCollectRoots( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots ) +{ + Vec_IntClear( vRoots ); + Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+3) ); + Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+4) ); + Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, iBox, vRoots ); +} +Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes ) +{ + extern Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds ); + Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( pGia, vAdds ); + Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) ); + Vec_Wec_t * vRes = Vec_WecStart( Vec_IntSize(vRootBoxes) ); + Vec_Int_t * vRoots = Vec_IntAlloc( 64 ); + Vec_Int_t * vOrder; + int i, iBox; + Vec_IntForEachEntry( vRootBoxes, iBox, i ) + { + Gia_PolyCollectRoots( vAdds, vMap, vMarks, iBox, vRoots ); + vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, NULL ); + Vec_IntAppend( Vec_WecEntry(vRes, i), vOrder ); + Vec_IntFree( vOrder ); + } + Vec_BitFree( vMarks ); + Vec_IntFree( vRoots ); + Vec_WecFree( vMap ); + return vRes; +} + /**Function************************************************************* Synopsis [Collect internal node order.] @@ -197,15 +269,15 @@ Vec_Int_t * Gia_PolynCoreCollect( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t Vec_IntForEachEntryReverse( vOrder, Index, i ) { // mark inputs - Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 ); - Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 ); - Entry3 = Vec_IntEntry( vAdds, 5*Index + 2 ); + Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 ); + Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 ); + Entry3 = Vec_IntEntry( vAdds, 6*Index + 2 ); Vec_BitWriteEntry( vVisited, Entry1, 1 ); Vec_BitWriteEntry( vVisited, Entry2, 1 ); Vec_BitWriteEntry( vVisited, Entry3, 1 ); // traverse from outputs - Entry1 = Vec_IntEntry( vAdds, 5*Index + 3 ); - Entry2 = Vec_IntEntry( vAdds, 5*Index + 4 ); + Entry1 = Vec_IntEntry( vAdds, 6*Index + 3 ); + Entry2 = Vec_IntEntry( vAdds, 6*Index + 4 ); Gia_PolynCoreCollect_rec( pGia, Entry1, vNodes, vVisited ); Gia_PolynCoreCollect_rec( pGia, Entry2, vNodes, vVisited ); } @@ -325,7 +397,7 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos, //Gia_ManShow( pGia, vNodes, 0 ); printf( "Detected %d FAs/HAs. Roots = %d. Leaves = %d. Nodes = %d. Adds = %d. ", - Vec_IntSize(vAdds)/5, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) ); + Vec_IntSize(vAdds)/6, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose ); diff --git a/src/proof/acec/acecPa.c b/src/proof/acec/acecPa.c new file mode 100644 index 00000000..11d68d37 --- /dev/null +++ b/src/proof/acec/acecPa.c @@ -0,0 +1,282 @@ +/**CFile**************************************************************** + + FileName [acecPa.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecPa.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 [] + +***********************************************************************/ +int Pas_ManVerifyPhaseOne_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 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) ); + Truth1 = Pas_ManVerifyPhaseOne_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 Pas_ManVerifyPhaseOne( 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 = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) ); + TruthXor = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthXor : TruthXor; + + iObj = Vec_IntEntry( vAdds, 6*iBox+4 ); + TruthMaj = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) ); + TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj; + + if ( fFadd ) // FADD + { + if ( TruthXor != 0x96 ) + printf( "Fadd %d sum is wrong.\n", iBox ); + if ( TruthMaj != 0xE8 ) + printf( "Fadd %d carry is wrong.\n", iBox ); + } + else + { + if ( TruthXor != 0x66 ) + printf( "Hadd %d sum is wrong.\n", iBox ); + if ( TruthMaj != 0x88 ) + printf( "Hadd %d carry is wrong.\n", iBox ); + } +} +void Pas_ManVerifyPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Bit_t * vPhase ) +{ + int k, iBox; + Vec_IntForEachEntry( vOrder, iBox, k ) + Pas_ManVerifyPhaseOne( p, vAdds, iBox, vPhase ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pas_ManPhase_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Gia_Obj_t * pObj, int fPhase, Vec_Bit_t * vPhase, Vec_Bit_t * vConstPhase ) +{ + int k, iBox, iXor, Sign, fXorPhase; + assert( pObj != Gia_ManConst0(p) ); + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( fPhase ) + Vec_BitWriteEntry( vPhase, Gia_ObjId(p, pObj), fPhase ); + if ( !Gia_ObjIsAnd(pObj) ) + return; + iBox = Vec_IntEntry( vMap, Gia_ObjId(p, pObj) ); + if ( iBox == -1 ) + return; + iXor = Vec_IntEntry( vAdds, 6*iBox+3 ); + Sign = Vec_IntEntry( vAdds, 6*iBox+5 ); + fXorPhase = ((Sign >> 3) & 1); + // remember complemented HADD + if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 && fPhase ) + Vec_BitWriteEntry( vConstPhase, iBox, 1 ); + for ( k = 0; k < 3; k++ ) + { + int iObj = Vec_IntEntry( vAdds, 6*iBox+k ); + int fPhaseThis = ((Sign >> k) & 1) ^ fPhase; + fXorPhase ^= fPhaseThis; + if ( iObj == 0 ) + continue; + Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iObj), fPhaseThis, vPhase, vConstPhase ); + } + Vec_BitWriteEntry( vPhase, iXor, fXorPhase ); +} +Vec_Bit_t * Pas_ManPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Vec_Int_t * vRoots, Vec_Bit_t ** pvConstPhase ) +{ + Vec_Bit_t * vPhase = Vec_BitStart( Vec_IntSize(vMap) ); + Vec_Bit_t * vConstPhase = Vec_BitStart( Vec_IntSize(vAdds)/6 ); + int i, iRoot; + Gia_ManIncrementTravId( p ); + Vec_IntForEachEntry( vRoots, iRoot, i ) + Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iRoot), 1, vPhase, vConstPhase ); + *pvConstPhase = vConstPhase; + return vPhase; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Int_t * vIns, Vec_Int_t * vOuts ) +{ + Vec_Bit_t * vUnique = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Bit_t * vUsed = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); + Vec_Int_t * vRoots = Vec_IntAlloc( 100 ); + Vec_Bit_t * vPhase, * vConstPhase; + int i, k, Entry, nTrees; + + // map carries into adder indexes and mark driven nodes + Vec_IntForEachEntry( vOrder, i, k ) + { + int Carry = Vec_IntEntry(vAdds, 6*i+4); + if ( Vec_BitEntry(vUnique, Carry) ) + printf( "Carry %d participates more than once.\n", Carry ); + Vec_BitWriteEntry( vUnique, Carry, 1 ); + Vec_IntWriteEntry( vMap, Carry, i ); + // mark driven + Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+0), 1 ); + Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+1), 1 ); + Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+2), 1 ); + } + // collect carries that do not drive other adders + for ( i = 0; i < Gia_ManObjNum(p); i++ ) + if ( Vec_BitEntry(vUnique, i) && !Vec_BitEntry(vUsed, i) ) + Vec_IntPush( vRoots, i ); + nTrees = Vec_IntSize( vRoots ); + + Vec_IntPrint( vRoots ); + + // compute phases + if ( Vec_IntSize(vRoots) > 0 ) + { + int nCompls = 0; + + vPhase = Pas_ManPhase( p, vAdds, vMap, vRoots, &vConstPhase ); + Pas_ManVerifyPhase( p, vAdds, vOrder, vPhase ); + + printf( "Outputs: " ); + Vec_IntForEachEntry( vOuts, Entry, i ) + printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) ); + printf( "\n" ); + + printf( "Inputs: " ); + Vec_IntForEachEntry( vIns, Entry, i ) + { + printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) ); + nCompls += Vec_BitEntry(vPhase, Entry); + } + printf( " Compl = %d\n", nCompls ); + + Vec_BitFreeP( &vPhase ); + Vec_BitFreeP( &vConstPhase ); + } + + Vec_IntFree( vRoots ); + Vec_IntFree( vMap ); + Vec_BitFree( vUnique ); + Vec_BitFree( vUsed ); + return nTrees; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pas_ManComputeCutsTest( Gia_Man_t * p ) +{ + extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose ); + extern Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts ); + + extern int Ree_ManCountFadds( Vec_Int_t * vAdds ); + extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose ); + abctime clk = Abc_Clock(); + Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 ); + Vec_Int_t * vIns, * vOuts; + Vec_Int_t * vOrder = Gia_PolynCoreOrder( p, vAdds, NULL, &vIns, &vOuts ); + int nTrees, nFadds = Ree_ManCountFadds( vAdds ); + //Ree_ManPrintAdders( vAdds, 1 ); + printf( "Detected %d FAs and %d HAs. Collected %d adders. ", nFadds, Vec_IntSize(vAdds)/6-nFadds, Vec_IntSize(vOrder) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + // detect trees + clk = Abc_Clock(); + nTrees = Pas_ManComputeCuts( p, vAdds, vOrder, vIns, vOuts ); + Vec_IntFree( vAdds ); + Vec_IntFree( vOrder ); + Vec_IntFree( vIns ); + Vec_IntFree( vOuts ); + + printf( "Detected %d adder trees. ", nTrees ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecPool.c b/src/proof/acec/acecPool.c new file mode 100644 index 00000000..294066fa --- /dev/null +++ b/src/proof/acec/acecPool.c @@ -0,0 +1,132 @@ +/**CFile**************************************************************** + + FileName [acecPool.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecPool.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_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds ) +{ + Vec_Bit_t * vMarks = Vec_BitStart( Gia_ManObjNum(p) ); + int i, k; + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + for ( k = 0; k < 3; k++ ) + Vec_BitWriteEntry( vMarks, Vec_IntEntry(vAdds, 6*i+k), 1 ); + return vMarks; +} + +Vec_Int_t * Acec_ManPoolTopMost( Gia_Man_t * p, Vec_Int_t * vAdds ) +{ + int i, k, iTop, fVerbose = 0; + Vec_Int_t * vTops = Vec_IntAlloc( 1000 ); + Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( p, vAdds ); + + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + if ( !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+3)) && + !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+4)) ) + Vec_IntPush( vTops, i ); + + if ( fVerbose ) + Vec_IntForEachEntry( vTops, iTop, i ) + { + printf( "%4d : ", iTop ); + for ( k = 0; k < 3; k++ ) + printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) ); + printf( " -> " ); + for ( k = 3; k < 5; k++ ) + printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) ); + printf( "\n" ); + } + + Vec_BitFree( vMarks ); + return vTops; +} +void Acec_ManPool( Gia_Man_t * p ) +{ + extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose ); + extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes ); + + extern int Ree_ManCountFadds( Vec_Int_t * vAdds ); + extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose ); + extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds ); + extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds ); + Vec_Int_t * vTops, * vTree; + Vec_Wec_t * vTrees; + + abctime clk = Abc_Clock(); + Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 ); + int i, nFadds = Ree_ManCountFadds( vAdds ); + printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + clk = Abc_Clock(); + Ree_ManRemoveTrivial( p, vAdds ); + Ree_ManRemoveContained( p, vAdds ); + nFadds = Ree_ManCountFadds( vAdds ); + printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + //Ree_ManPrintAdders( vAdds, 1 ); + + // detect topmost nodes + vTops = Acec_ManPoolTopMost( p, vAdds ); + printf( "Detected %d topmost adder%s.\n", Vec_IntSize(vTops), Vec_IntSize(vTops) > 1 ? "s":"" ); + + // collect adder trees + vTrees = Gia_PolynCoreOrderArray( p, vAdds, vTops ); + Vec_WecForEachLevel( vTrees, vTree, i ) + printf( "Adder %5d : Tree with %5d nodes.\n", Vec_IntEntry(vTops, i), Vec_IntSize(vTree) ); + + Vec_WecFree( vTrees ); + Vec_IntFree( vAdds ); + Vec_IntFree( vTops ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c index 1f10d249..e2340dba 100644 --- a/src/proof/acec/acecRe.c +++ b/src/proof/acec/acecRe.c @@ -69,6 +69,18 @@ void Ree_TruthPrecompute() } printf( "\n" ); } +void Ree_TruthPrecompute2() +{ + int i, b; + for ( i = 0; i < 8; i++ ) + { + word Truth = 0xE8; + for ( b = 0; b < 3; b++ ) + if ( (i >> b) & 1 ) + Truth = Abc_Tt6Flip( Truth, b ); + printf( "%d = %X\n", i, 0xFF & (int)Truth ); + } +} /**Function************************************************************* @@ -239,7 +251,7 @@ void Ree_ManCutPrint( int * pCut, int Count, word Truth ) void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Hash_IntMan_t * pHash, Vec_Int_t * vData ) { int fVerbose = 0; - int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[5], Count = 0; + int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[6], Count = 0; if ( fVerbose ) printf( "Object %d\n", iObj ); Vec_IntFill( vCuts, 2, 1 ); @@ -290,7 +302,7 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I ***********************************************************************/ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData ) { - int i, j, k, iObj, iObj2, Value, Truth, CountX, CountM, Index = 0; + int i, j, k, iObj, iObj2, Value, Truth, Truth2, CountX, CountM, Index = 0; int nEntries = Hash_IntManEntryNum(p); Vec_Int_t * vAdds = Vec_IntAlloc( 1000 ); Vec_Int_t * vXors = Vec_IntStart( nEntries + 1 ); @@ -325,9 +337,9 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData ) if ( Index == -1 ) continue; if ( Truth == 0x66 || Truth == 0x99 || Truth == 0x69 || Truth == 0x96 ) - Vec_WecPush( vXorMap, Index, iObj ); + Vec_IntPushTwo( Vec_WecEntry(vXorMap, Index), iObj, Truth ); else - Vec_WecPush( vMajMap, Index, iObj ); + Vec_IntPushTwo( Vec_WecEntry(vMajMap, Index), iObj, Truth ); } Vec_IntFree( vIndex ); // create pairs @@ -336,11 +348,22 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData ) Vec_Int_t * vXorOne = Vec_WecEntry( vXorMap, i ); Vec_Int_t * vMajOne = Vec_WecEntry( vMajMap, i ); Hash_IntObj_t * pObj = Hash_IntObj( p, Value ); - Vec_IntForEachEntry( vXorOne, iObj, j ) - Vec_IntForEachEntry( vMajOne, iObj2, k ) + Vec_IntForEachEntryDouble( vXorOne, iObj, Truth, j ) + Vec_IntForEachEntryDouble( vMajOne, iObj2, Truth2, k ) { + int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0xEE, 0xDD, 0xBB, 0x77}; + int SignMaj[8] = {0xE8, 0xD4, 0xB2, 0x71, 0x8E, 0x4D, 0x2B, 0x17}; + int n, SignXor = (Truth == 0x99 || Truth == 0x69) << 3; + for ( n = 0; n < 8; n++ ) + if ( Truth2 == SignMaj[n] ) + break; + if ( n == 8 ) + for ( n = 0; n < 8; n++ ) + if ( Truth2 == SignAnd[n] ) + break; + assert( n < 8 ); Vec_IntPushThree( vAdds, pObj->iData0, pObj->iData1, pObj->iData2 ); - Vec_IntPushTwo( vAdds, iObj, iObj2 ); + Vec_IntPushThree( vAdds, iObj, iObj2, SignXor | n ); } } Vec_IntFree( vIndexRev ); @@ -384,12 +407,58 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose ) vAdds = Ree_ManDeriveAdds( pHash, vData ); if ( fVerbose ) printf( "Adds = %d. Total = %d. Hashed = %d. Hashed/Adds = %.2f.\n", - Vec_IntSize(vAdds)/5, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 5.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) ); + Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) ); Vec_IntFree( vData ); Hash_IntManStop( pHash ); return vAdds; } +/**Function************************************************************* + + Synopsis [Highlight nodes inside FAs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ree_CollectInsiders_rec( Gia_Man_t * pGia, int iObj, Vec_Bit_t * vVisited, Vec_Bit_t * vInsiders ) +{ + if ( Vec_BitEntry(vVisited, iObj) ) + return; + Vec_BitSetEntry( vVisited, iObj, 1 ); + Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId0p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders ); + Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId1p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders ); + Vec_BitSetEntry( vInsiders, iObj, 1 ); +} +Vec_Bit_t * Ree_CollectInsiders( Gia_Man_t * pGia, Vec_Int_t * vAdds ) +{ + Vec_Bit_t * vVisited = Vec_BitStart( Gia_ManObjNum(pGia) ); + Vec_Bit_t * vInsiders = Vec_BitStart( Gia_ManObjNum(pGia) ); + int i, Entry1, Entry2, Entry3; + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + { + if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD + continue; + // mark inputs + Entry1 = Vec_IntEntry( vAdds, 6*i + 0 ); + Entry2 = Vec_IntEntry( vAdds, 6*i + 1 ); + Entry3 = Vec_IntEntry( vAdds, 6*i + 2 ); + Vec_BitWriteEntry( vVisited, Entry1, 1 ); + Vec_BitWriteEntry( vVisited, Entry2, 1 ); + Vec_BitWriteEntry( vVisited, Entry3, 1 ); + // traverse from outputs + Entry1 = Vec_IntEntry( vAdds, 6*i + 3 ); + Entry2 = Vec_IntEntry( vAdds, 6*i + 4 ); + Ree_CollectInsiders_rec( pGia, Entry1, vVisited, vInsiders ); + Ree_CollectInsiders_rec( pGia, Entry2, vVisited, vInsiders ); + } + Vec_BitFree( vVisited ); + return vInsiders; +} + /**Function************************************************************* Synopsis [] @@ -401,28 +470,80 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -void Ree_ManComputeCutsTest( Gia_Man_t * p ) +// removes HAs whose AND2 is part of XOR2 without additional fanout +void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds ) +{ + Gia_Obj_t * pObjX, * pObjM; + int i, k = 0; + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + { + if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD + { + pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) ); + pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) ); + if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 ) + continue; + } + memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) ); + } + assert( k <= i ); + Vec_IntShrink( vAdds, 6*k ); +} +// removes HAs fully contained inside FAs +void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds ) +{ + Vec_Bit_t * vInsiders = Ree_CollectInsiders( p, vAdds ); + int i, k = 0; + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + { + if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD + if ( Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+4)) ) + continue; + memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) ); + } + assert( k <= i ); + Vec_IntShrink( vAdds, 6*k ); + Vec_BitFree( vInsiders ); +} + +int Ree_ManCountFadds( Vec_Int_t * vAdds ) { - abctime clk = Abc_Clock(); - Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 ); int i, Count = 0; - for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ ) + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + if ( Vec_IntEntry(vAdds, 6*i+2) != 0 ) + Count++; + return Count; +} +void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose ) +{ + int i; + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) { - if ( Vec_IntEntry(vAdds, 5*i+2) == 0 ) + //if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) + // continue; + if ( !fVerbose ) continue; - Count++; - continue; printf( "%6d : ", i ); - printf( "%6d ", Vec_IntEntry(vAdds, 5*i+0) ); - printf( "%6d ", Vec_IntEntry(vAdds, 5*i+1) ); - printf( "%6d ", Vec_IntEntry(vAdds, 5*i+2) ); + printf( "%6d ", Vec_IntEntry(vAdds, 6*i+0) ); + printf( "%6d ", Vec_IntEntry(vAdds, 6*i+1) ); + printf( "%6d ", Vec_IntEntry(vAdds, 6*i+2) ); printf( " -> " ); - printf( "%6d ", Vec_IntEntry(vAdds, 5*i+3) ); - printf( "%6d ", Vec_IntEntry(vAdds, 5*i+4) ); + printf( "%6d ", Vec_IntEntry(vAdds, 6*i+3) ); + printf( "%6d ", Vec_IntEntry(vAdds, 6*i+4) ); + printf( " (%d)", Vec_IntEntry(vAdds, 6*i+5) ); printf( "\n" ); } +} +void Ree_ManComputeCutsTest( Gia_Man_t * p ) +{ + abctime clk = Abc_Clock(); + Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 ); + int nFadds = Ree_ManCountFadds( vAdds ); + Ree_ManPrintAdders( vAdds, 1 ); + printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds ); Vec_IntFree( vAdds ); - printf( "Detected %d FAs and %d HAs. ", Count, Vec_IntSize(vAdds)/5-Count ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make index e66bf6e8..df6db695 100644 --- a/src/proof/acec/module.make +++ b/src/proof/acec/module.make @@ -1,7 +1,10 @@ -SRC += src/proof/acec/acecCore.c \ +SRC += src/proof/acec/acecCl.c \ + src/proof/acec/acecCore.c \ src/proof/acec/acecCo.c \ src/proof/acec/acecRe.c \ + src/proof/acec/acecPa.c \ src/proof/acec/acecPo.c \ + src/proof/acec/acecPool.c \ src/proof/acec/acecCover.c \ src/proof/acec/acecFadds.c \ src/proof/acec/acecOrder.c \ -- cgit v1.2.3