From e21c7d72f3f43f38e5af10a38602de6f6ce9a20e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 30 Jan 2017 08:39:26 -0800 Subject: Updates to arithmetic verification. --- src/proof/acec/acecInt.h | 1 + src/proof/acec/acecMult.c | 66 +++++++++++ src/proof/acec/acecStruct.c | 271 ++++++++++++++++++++++++++++++++++++++++++++ src/proof/acec/acecXor.c | 67 ++++++++++- 4 files changed, 400 insertions(+), 5 deletions(-) create mode 100644 src/proof/acec/acecStruct.c (limited to 'src/proof/acec') diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index 381ab8d1..c4c8061e 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -76,6 +76,7 @@ extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdd /*=== acecMult.c ========================================================*/ extern Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits ); extern Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p ); +extern Vec_Bit_t * Acec_MultMarkPPs( Gia_Man_t * p ); /*=== acecNorm.c ========================================================*/ 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 ); diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c index ba9405ac..c63fdde2 100644 --- a/src/proof/acec/acecMult.c +++ b/src/proof/acec/acecMult.c @@ -433,6 +433,72 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec return vInputs; } +/**Function************************************************************* + + Synopsis [Mark nodes whose function is exactly that of a Booth PP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Bit_t * Acec_MultMarkPPs( Gia_Man_t * p ) +{ + word Saved[32] = { + ABC_CONST(0xF335ACC0F335ACC0), + ABC_CONST(0x35C035C035C035C0), + ABC_CONST(0xD728D728D728D728), + ABC_CONST(0xFD80FD80FD80FD80), + ABC_CONST(0xACC0ACC0ACC0ACC0), + ABC_CONST(0x7878787878787878), + ABC_CONST(0x2828282828282828), + ABC_CONST(0xD0D0D0D0D0D0D0D0), + ABC_CONST(0x8080808080808080), + ABC_CONST(0x8888888888888888), + ABC_CONST(0xAAAAAAAAAAAAAAAA), + ABC_CONST(0x5555555555555555), + + ABC_CONST(0xD5A8D5A8D5A8D5A8), + ABC_CONST(0x2A572A572A572A57), + ABC_CONST(0xF3C0F3C0F3C0F3C0), + ABC_CONST(0x5858585858585858), + ABC_CONST(0xA7A7A7A7A7A7A7A7), + ABC_CONST(0x2727272727272727), + ABC_CONST(0xD8D8D8D8D8D8D8D8) + }; + + Vec_Bit_t * vRes = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) ); + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + int i, iObj, nProds = 0; + Gia_ManCleanMark0(p); + Gia_ManForEachAndId( p, iObj ) + { + word Truth = Gia_ObjComputeTruth6Cis( p, Abc_Var2Lit(iObj, 0), vSupp, vTemp ); + if ( Vec_IntSize(vSupp) > 6 ) + continue; + vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize ); + if ( Vec_IntSize(vSupp) > 5 ) + continue; + for ( i = 0; i < 32 && Saved[i]; i++ ) + { + if ( Truth == Saved[i] || Truth == ~Saved[i] ) + { + Vec_BitWriteEntry( vRes, iObj, 1 ); + nProds++; + break; + } + } + } + Gia_ManCleanMark0(p); + printf( "Collected %d pps.\n", nProds ); + Vec_IntFree( vSupp ); + Vec_WrdFree( vTemp ); + return vRes; +} + /**Function************************************************************* Synopsis [] diff --git a/src/proof/acec/acecStruct.c b/src/proof/acec/acecStruct.c new file mode 100644 index 00000000..6702e13b --- /dev/null +++ b/src/proof/acec/acecStruct.c @@ -0,0 +1,271 @@ +/**CFile**************************************************************** + + FileName [acecStruct.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: acecStruct.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_StructDetectXorRoots( Gia_Man_t * p ) +{ + Vec_Int_t * vXors = Vec_IntAlloc( 100 ); + Vec_Bit_t * vXorIns = Vec_BitStart( Gia_ManObjNum(p) ); + Gia_Obj_t * pFan0, * pFan1, * pObj; + int i, k = 0, Entry; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + continue; + Vec_IntPush( vXors, i ); + Vec_BitWriteEntry( vXorIns, Gia_ObjId(p, Gia_Regular(pFan0)), 1 ); + Vec_BitWriteEntry( vXorIns, Gia_ObjId(p, Gia_Regular(pFan1)), 1 ); + } + // collect XORs that not inputs of other XORs + Vec_IntForEachEntry( vXors, Entry, i ) + if ( !Vec_BitEntry(vXorIns, Entry) ) + Vec_IntWriteEntry( vXors, k++, Entry ); + Vec_IntShrink( vXors, k ); + Vec_BitFree( vXorIns ); + return vXors; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acec_StructAssignRanks( Gia_Man_t * p, Vec_Int_t * vXorRoots ) +{ + Vec_Int_t * vDoubles = Vec_IntAlloc( 100 ); + Gia_Obj_t * pFan0, * pFan1, * pObj; + int i, k, Fanins[2], Entry, Rank; + // map roots into their ranks + Vec_Int_t * vRanks = Vec_IntStartFull( Gia_ManObjNum(p) ); + Vec_IntForEachEntry( vXorRoots, Entry, i ) + Vec_IntWriteEntry( vRanks, Entry, i ); + // map nodes into their ranks + Gia_ManForEachAndReverse( p, pObj, i ) + { + if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + continue; + Rank = Vec_IntEntry( vRanks, i ); + // skip XORs that are not part of any tree + if ( Rank == -1 ) + continue; + // iterate through XOR inputs + Fanins[0] = Gia_ObjId(p, Gia_Regular(pFan0)); + Fanins[1] = Gia_ObjId(p, Gia_Regular(pFan1)); + for ( k = 0; k < 2; k++ ) + { + Entry = Vec_IntEntry( vRanks, Fanins[k] ); + if ( Entry == Rank ) // the same tree -- allow fanout in this tree + continue; + if ( Entry == -1 ) + Vec_IntWriteEntry( vRanks, Fanins[k], Rank ); + else + Vec_IntPush( vDoubles, Fanins[k] ); + if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Fanins[k]))) + printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Fanins[k], Entry, Rank ); + } + } + // remove duplicated entries + Vec_IntForEachEntry( vDoubles, Entry, i ) + Vec_IntWriteEntry( vRanks, Entry, -1 ); + Vec_IntFree( vDoubles ); + return vRanks; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wec_t * Acec_FindTreeLeaves( Gia_Man_t * p, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks ) +{ + Vec_Bit_t * vMapXors = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Wec_t * vTreeLeaves = Vec_WecStart( Vec_IntSize(vXorRoots) ); + Gia_Obj_t * pFan0, * pFan1, * pObj; + int i, k, Fanins[2], Rank; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + continue; + Vec_BitWriteEntry( vMapXors, i, 1 ); + Rank = Vec_IntEntry( vRanks, i ); + // skip XORs that are not part of any tree + if ( Rank == -1 ) + continue; + // iterate through XOR inputs + Fanins[0] = Gia_ObjId(p, Gia_Regular(pFan0)); + Fanins[1] = Gia_ObjId(p, Gia_Regular(pFan1)); + for ( k = 0; k < 2; k++ ) + { + if ( Vec_BitEntry(vMapXors, Fanins[k]) ) + { + assert( Rank == Vec_IntEntry(vRanks, Fanins[k]) ); + continue; + } + Vec_WecPush( vTreeLeaves, Rank, Fanins[k] ); + } + } + Vec_BitFree( vMapXors ); + return vTreeLeaves; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acec_FindShadows( Gia_Man_t * p, Vec_Int_t * vRanks ) +{ + Vec_Int_t * vShadows = Vec_IntDup( vRanks ); + Gia_Obj_t * pObj; int i, Shad0, Shad1; + Gia_ManForEachCi( p, pObj, i ) + Vec_IntWriteEntry( vShadows, Gia_ObjId(p, pObj), -1 ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( Vec_IntEntry(vShadows, i) >= 0 ) + continue; + Shad0 = Vec_IntEntry(vShadows, Gia_ObjFaninId0(pObj, i)); + Shad1 = Vec_IntEntry(vShadows, Gia_ObjFaninId1(pObj, i)); + if ( Shad0 == Shad1 && Shad0 != -1 ) + Vec_IntWriteEntry(vShadows, i, Shad0); + } + return vShadows; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acec_CollectSupp_rec( Gia_Man_t * p, int iNode, int Rank, Vec_Int_t * vRanks ) +{ + Gia_Obj_t * pObj; + int nSize; + if ( Gia_ObjIsTravIdCurrentId(p, iNode) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iNode); + pObj = Gia_ManObj(p, iNode); + assert( Gia_ObjIsAnd(pObj) ); + if ( Vec_IntEntry(vRanks, iNode) == Rank ) + return 1; + nSize = Acec_CollectSupp_rec( p, Gia_ObjFaninId0(pObj, iNode), Rank, vRanks ); + nSize += Acec_CollectSupp_rec( p, Gia_ObjFaninId1(pObj, iNode), Rank, vRanks ); + return nSize; +} +Vec_Wec_t * Acec_FindNexts( Gia_Man_t * p, Vec_Int_t * vRanks, Vec_Int_t * vShadows, Vec_Wec_t * vTreeLeaves ) +{ + Vec_Wec_t * vNexts = Vec_WecStart( Vec_WecSize(vTreeLeaves) ); + Vec_Int_t * vTree; + int i, k, Node, Fanins[2], Shad0, Shad1, Rank, nSupp; + Vec_WecForEachLevel( vTreeLeaves, vTree, i ) + Vec_IntForEachEntry( vTree, Node, k ) + { + Gia_Obj_t * pObj = Gia_ManObj(p, Node); + if ( !Gia_ObjIsAnd(pObj) ) + continue; + Fanins[0] = Gia_ObjFaninId0(pObj, Node); + Fanins[1] = Gia_ObjFaninId1(pObj, Node); + Shad0 = Vec_IntEntry(vShadows, Fanins[0]); + Shad1 = Vec_IntEntry(vShadows, Fanins[1]); + if ( Shad0 != Shad1 || Shad0 == -1 ) + continue; + // check support size of Node in terms of the shadow of its fanins + Rank = Vec_IntEntry( vRanks, Node ); + assert( Rank != Shad0 ); + Gia_ManIncrementTravId( p ); + nSupp = Acec_CollectSupp_rec( p, Node, Shad0, vRanks ); + assert( nSupp > 1 ); + if ( nSupp > 3 ) + continue; + Vec_IntPushUniqueOrder( Vec_WecEntry(vNexts, Shad0), Rank ); + } + return vNexts; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acec_StructTest( Gia_Man_t * p ) +{ +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c index acbde1a0..71e0b7b3 100644 --- a/src/proof/acec/acecXor.c +++ b/src/proof/acec/acecXor.c @@ -33,6 +33,35 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acec_CheckXors( Gia_Man_t * p, Vec_Int_t * vXors ) +{ + Gia_Obj_t * pFan0, * pFan1; + Vec_Int_t * vCount2 = Vec_IntAlloc( Gia_ManObjNum(p) ); + int i, Entry, Count = 0; + for ( i = 0; 4*i < Vec_IntSize(vXors); i++ ) + if ( Vec_IntEntry(vXors, 4*i+3) == 0 ) + Vec_IntAddToEntry( vCount2, Vec_IntEntry(vXors, 4*i), 1 ); + Vec_IntForEachEntry( vCount2, Entry, i ) + if ( Entry > 1 ) + printf( "*** Obj %d has %d two-input XOR cuts.\n", i, Entry ), Count++; + else if ( Entry == 1 && Gia_ObjRecognizeExor(Gia_ManObj(p, i), &pFan0, &pFan1) ) + printf( "*** Obj %d cannot be recognized as XOR.\n", i ); + if ( Count == 0 ) + printf( "*** There no multiple two-input XOR cuts.\n" ); + Vec_IntFree( vCount2 ); +} + /**Function************************************************************* Synopsis [] @@ -151,7 +180,6 @@ Vec_Int_t * Acec_FindXorRoots( Gia_Man_t * p, Vec_Int_t * vXors ) 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 @@ -184,8 +212,9 @@ Vec_Int_t * Acec_RankTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRo 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 ); + + if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Node))) + printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank ); } } // remove duplicated entries @@ -211,6 +240,7 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA for ( k = 1; k < 4; k++ ) { int Fanin = Vec_IntEntry(vXors, 4*i+k); + //int RankFanin = Vec_IntEntry(vRanks, Fanin); if ( Fanin == 0 ) continue; if ( Vec_BitEntry(vMapXors, Fanin) ) @@ -218,6 +248,8 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA assert( Rank == Vec_IntEntry(vRanks, Fanin) ); continue; } +// if ( Vec_BitEntry(vMapXors, Fanin) && Rank == RankFanin ) +// continue; 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 @@ -230,7 +262,26 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA *pvAddBoxes = vAddBoxes; return vXorLeaves; } +void Acec_CheckBoothPPs( Gia_Man_t * p, Vec_Wec_t * vLitLeaves ) +{ + Vec_Bit_t * vMarked = Acec_MultMarkPPs( p ); + Vec_Int_t * vLevel; + int i, k, iLit; + Vec_WecForEachLevel( vLitLeaves, vLevel, i ) + { + int CountPI = 0, CountB = 0, CountNB = 0; + Vec_IntForEachEntry( vLevel, iLit, k ) + if ( !Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) ) + CountPI++; + else if ( Vec_BitEntry( vMarked, Abc_Lit2Var(iLit) ) ) + CountB++; + else + CountNB++; + printf( "Rank %2d : Lits = %5d PI = %d Booth = %5d Non-Booth = %5d\n", i, Vec_IntSize(vLevel), CountPI, CountB, CountNB ); + } + Vec_BitFree( vMarked ); +} 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 ); @@ -315,6 +366,8 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox Vec_IntSort( vLevel, 0 ); Vec_WecForEachLevel( pBox->vRootLits, vLevel, i ) Vec_IntSort( vLevel, 1 ); + + //Acec_CheckBoothPPs( p, pBox->vLeafLits ); return pBox; } @@ -331,9 +384,13 @@ Acec_Box_t * Acec_ProduceBox( Gia_Man_t * p, int fVerbose ) Gia_ManLevelNum(p); + //Acec_CheckXors( p, vXors ); + //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 ); + if ( fVerbose ) + 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 ); + if ( fVerbose ) + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); vXorRoots = Acec_OrderTreeRoots( p, vAdds, vTemp = vXorRoots, vRanks ); Vec_IntFree( vTemp ); -- cgit v1.2.3