luke/abc
1
0
Fork 0
mirror of https://github.com/YosysHQ/abc.git synced 2026-09-03 03:43:02 +02:00
Code Issues Packages Projects Releases Wiki Activity

Adding new command line options for &verify and &synch2.

Browse Source
This commit is contained in:
Alan Mishchenko
2017-07-06 21:13:53 -07:00
parent 4712edc097
commit 1676df19e7
3 changed files with 28 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/aig/gia/gia.h
+1 -1
View File
@@ -1533,7 +1533,7 @@ extern void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBox
extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres );
extern Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft );
extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq );
extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fVerbose, char * pFileSpec );
extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec );
/*=== giaTruth.c ===========================================================*/
extern word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths );
extern word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp );
src/aig/gia/giaTim.c
+13 -1
View File
@@ -21,6 +21,7 @@
#include "gia.h"
#include "giaAig.h"
#include "misc/tim/tim.h"
#include "misc/extra/extra.h"
#include "proof/cec/cec.h"
#include "proof/fra/fra.h"
@@ -892,7 +893,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
SeeAlso []
***********************************************************************/
int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fVerbose, char * pFileSpec )
int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec )
{
int Status = -1;
Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
@@ -955,6 +956,17 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
pGia1 = Gia_ManDup( pGia );
Vec_IntFreeP( &vBoxPres );
}
if ( fDumpFiles )
{
char pFileName0[1000], pFileName1[1000];
char * pNameGeneric = Extra_FileNameGeneric( pFileSpec ? pFileSpec : pGia->pSpec );
sprintf( pFileName0, "%s_spec.aig", pNameGeneric );
sprintf( pFileName1, "%s_impl.aig", pNameGeneric );
Gia_AigerWrite( pGia0, pFileName0, 0, 0 );
Gia_AigerWrite( pGia1, pFileName1, 0, 0 );
ABC_FREE( pNameGeneric );
printf( "Dumped two parts of the miter into files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
}
// compute the miter
if ( fSeq )
{