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

Changes to arithmetic logic detection.

This commit is contained in:
Alan Mishchenko 2016-12-02 21:12:57 -08:00
parent 2ff522df45
commit 1bf289c774
7 changed files with 740 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
abclib.dsp
View File

@ -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

55
src/proof/acec/acecCl.c Normal file
View File

@ -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

146
src/proof/acec/acecCo.c
View File

@ -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 );
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 );
}
// collect additional outputs
Vec_IntForEachEntry( vAddCos, Driver, i )
{
Vec_IntPush( vRoots, Driver );
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 );

282
src/proof/acec/acecPa.c Normal file
View File

@ -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

132
src/proof/acec/acecPool.c Normal file
View File

@ -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

171
src/proof/acec/acecRe.c
View File

@ -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 []
***********************************************************************/
// 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 )
{
int i, Count = 0;
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, 6*i+2) == 0 )
// continue;
if ( !fVerbose )
continue;
printf( "%6d : ", i );
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, 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 i, Count = 0;
for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
{
if ( Vec_IntEntry(vAdds, 5*i+2) == 0 )
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( " -> " );
printf( "%6d ", Vec_IntEntry(vAdds, 5*i+3) );
printf( "%6d ", Vec_IntEntry(vAdds, 5*i+4) );
printf( "\n" );
}
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 );
}

5
src/proof/acec/module.make
View File

@ -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 \