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

Updates to arithmetic verification.

This commit is contained in:
Alan Mishchenko 2017-01-10 16:58:24 +07:00
parent fbdf28e4c9
commit 5fbc0cd7f0
10 changed files with 75 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

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

6
src/aig/gia/giaShow.c
View File

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

4
src/proof/acec/acec.h
View File

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

8
src/proof/acec/acecCl.c
View File

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

7
src/proof/acec/acecInt.h
View File

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

21
src/proof/acec/acecPa.c
View File

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

17
src/proof/acec/acecPool.c
View File

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

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

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

56
src/proof/acec/acecTree.c Normal file
View File

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

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

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