diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-10 16:58:24 +0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-10 16:58:24 +0700 |
commit | 5fbc0cd7f09a382241266404d78c18c5443d2b9d (patch) | |
tree | cb6bdfcceb7414b8d2637724dfeac0ffc152eeff | |
parent | fbdf28e4c937067737d84db37ff6e1a65348df5f (diff) | |
download | abc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.tar.gz abc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.tar.bz2 abc-5fbc0cd7f09a382241266404d78c18c5443d2b9d.zip |
Updates to arithmetic verification.
-rw-r--r-- | abclib.dsp | 4 | ||||
-rw-r--r-- | src/aig/gia/giaShow.c | 6 | ||||
-rw-r--r-- | src/proof/acec/acec.h | 4 | ||||
-rw-r--r-- | src/proof/acec/acecCl.c | 8 | ||||
-rw-r--r-- | src/proof/acec/acecInt.h | 7 | ||||
-rw-r--r-- | src/proof/acec/acecPa.c | 21 | ||||
-rw-r--r-- | src/proof/acec/acecPool.c | 17 | ||||
-rw-r--r-- | src/proof/acec/acecRe.c | 4 | ||||
-rw-r--r-- | src/proof/acec/acecTree.c | 56 | ||||
-rw-r--r-- | src/proof/acec/module.make | 1 |
10 files changed, 75 insertions, 53 deletions
@@ -5535,6 +5535,10 @@ SOURCE=.\src\proof\acec\acecSt.c # End Source File # Begin Source File +SOURCE=.\src\proof\acec\acecTree.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\acec\acecUtil.c # End Source File # End Group diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index afd36fff..986d5624 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -814,18 +814,12 @@ void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In } void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds ) { - extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, 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 ); - extern void Abc_ShowFile( char * FileNameDot ); static int Counter = 0; char FileNameDot[200]; FILE * pFile; Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( pMan, &vXors, 0 ); - Ree_ManRemoveTrivial( pMan, vAdds ); - Ree_ManRemoveContained( pMan, vAdds ); // create the file name // Gia_ShowGetFileName( pMan->pName, FileNameDot ); diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h index 058e0f56..918119f8 100644 --- a/src/proof/acec/acec.h +++ b/src/proof/acec/acec.h @@ -76,6 +76,10 @@ extern Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVery extern Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose ); /*=== acecPolyn.c ========================================================*/ extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose ); +/*=== acecRe.c ========================================================*/ +extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose ); +extern int Ree_ManCountFadds( Vec_Int_t * vAdds ); +extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose ); ABC_NAMESPACE_HEADER_END diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c index 63483d57..145f2e0b 100644 --- a/src/proof/acec/acecCl.c +++ b/src/proof/acec/acecCl.c @@ -306,18 +306,10 @@ Gia_Man_t * Acec_DetectXorBuildNew( Gia_Man_t * p, Vec_Int_t * vRootXorSet ) ***********************************************************************/ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose ) { - extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, 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 ); - extern int Ree_ManCountFadds( Vec_Int_t * vAdds ); - extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose ); - abctime clk = Abc_Clock(); Gia_Man_t * pNew; Vec_Int_t * vRootXorSet; // Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, 0 ); -// Ree_ManRemoveTrivial( p, vAdds ); -// Ree_ManRemoveContained( p, vAdds ); //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 ); diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index d53b61c7..065f6300 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -63,12 +63,17 @@ struct Acec_Box_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== acecPa.c ========================================================*/ +/*=== acecCo.c ========================================================*/ +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 Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes ); +/*=== acecTree.c ========================================================*/ extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p ); /*=== acecUtil.c ========================================================*/ extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ); extern Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose ); + + ABC_NAMESPACE_HEADER_END diff --git a/src/proof/acec/acecPa.c b/src/proof/acec/acecPa.c index b59cdbef..6b382d91 100644 --- a/src/proof/acec/acecPa.c +++ b/src/proof/acec/acecPa.c @@ -248,11 +248,6 @@ int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Ve ***********************************************************************/ void Pas_ManComputeCutsTest( Gia_Man_t * p ) { - extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, 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, NULL, 1 ); Vec_Int_t * vIns, * vOuts; @@ -273,22 +268,6 @@ void Pas_ManComputeCutsTest( Gia_Man_t * p ) Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p ) -{ - return NULL; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/acec/acecPool.c b/src/proof/acec/acecPool.c index 08ee37f2..0868545e 100644 --- a/src/proof/acec/acecPool.c +++ b/src/proof/acec/acecPool.c @@ -303,17 +303,9 @@ void Acec_ManPrintRanks( Vec_Int_t * vPairs ) ***********************************************************************/ void Acec_ManProfile( Gia_Man_t * p, int fVerbose ) { - extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, 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 ); - extern int Ree_ManCountFadds( Vec_Int_t * vAdds ); - extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose ); - abctime clk = Abc_Clock(); Vec_Wec_t * vBoxes; int i; Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, fVerbose ); - Ree_ManRemoveTrivial( p, vAdds ); - Ree_ManRemoveContained( p, vAdds ); //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 ); @@ -396,13 +388,6 @@ Vec_Int_t * Acec_ManPoolTopMost( Gia_Man_t * p, Vec_Int_t * vAdds ) } void Acec_ManPool( Gia_Man_t * p ) { - extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, 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; @@ -413,8 +398,6 @@ void Acec_ManPool( Gia_Man_t * p ) 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 ); diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c index 26faad00..60b894c8 100644 --- a/src/proof/acec/acecRe.c +++ b/src/proof/acec/acecRe.c @@ -392,6 +392,8 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos } Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, 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 ); Gia_Obj_t * pObj; int * pList0, * pList1, i, nCuts = 0; Hash_IntMan_t * pHash = Hash_IntManStart( 1000 ); @@ -430,6 +432,8 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose 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 ); + Ree_ManRemoveTrivial( p, vAdds ); + Ree_ManRemoveContained( p, vAdds ); return vAdds; } diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c new file mode 100644 index 00000000..c2d89a1c --- /dev/null +++ b/src/proof/acec/acecTree.c @@ -0,0 +1,56 @@ +/**CFile**************************************************************** + + FileName [acecTree.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Adder tree construction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecTree.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p ) +{ + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make index 4003695e..4db695c5 100644 --- a/src/proof/acec/module.make +++ b/src/proof/acec/module.make @@ -11,4 +11,5 @@ SRC += src/proof/acec/acecCl.c \ src/proof/acec/acecOrder.c \ src/proof/acec/acecPolyn.c \ src/proof/acec/acecSt.c \ + src/proof/acec/acecTree.c \ src/proof/acec/acecUtil.c |