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

Enabled counter-example minimization in 'write_counter'.

This commit is contained in:
Alan Mishchenko 2011-11-11 20:56:05 -08:00
parent 9fe4c74952
commit 3beb36778e
6 changed files with 62 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/saig/saig.h
View File

@ -136,7 +136,7 @@ extern Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops );
extern Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs );
/*=== sswAbsCba.c ==========================================================*/
extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );
/*=== sswAbsPba.c ==========================================================*/

12
src/aig/saig/saigAbsCba.c
View File

@ -593,7 +593,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p )
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose )
Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
{
Saig_ManCba_t * p;
Vec_Int_t * vReasons;
@ -611,8 +611,8 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int
Saig_ManCbaShrink( p );
if ( fVerbose )
Aig_ManPrintStats( p->pFrames );
//if ( fVerbose )
//Aig_ManPrintStats( p->pFrames );
if ( fVerbose )
{
@ -629,9 +629,15 @@ ABC_PRT( "Time", clock() - clk );
Saig_ManCbaStop( p );
if ( fVerbose )
{
printf( "Real " );
Abc_CexPrintStats( pCex );
}
if ( fVerbose )
{
printf( "Care " );
Abc_CexPrintStats( pCare );
}
return pCare;
}

2
src/base/abci/abc.c
View File

@ -8881,7 +8881,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Cex_t * pNew;
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
pNew = Saig_ManCbaFindCexCareBits( pAig, pAbc->pCex, 0, fNewOrder, fVerbose );
pNew = Saig_ManCbaFindCexCareBits( pAig, pAbc->pCex, 0, fVerbose );
Aig_ManStop( pAig );
Abc_FrameReplaceCex( pAbc, &pNew );
}

36
src/base/io/io.c
View File

@ -20,6 +20,7 @@
#include "ioAbc.h"
#include "mainInt.h"
#include "saig.h"
ABC_NAMESPACE_IMPL_START
@ -2012,14 +2013,17 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
char * pFileName;
int c;
int fNames;
int c, fNames;
int fMinimize;
int forceSeq;
int fVerbose;
fNames = 0;
fMinimize = 0;
forceSeq = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "snh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "snmvh" ) ) != EOF )
{
switch ( c )
{
@ -2029,6 +2033,12 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
case 'n':
fNames ^= 1;
break;
case 'm':
fMinimize ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
@ -2080,11 +2090,25 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
}
if ( fNames )
{
Abc_Cex_t * pCare = NULL;
if ( fMinimize )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
if ( pCare == NULL )
printf( "Counter-example minimization has failed.\n" );
Aig_ManStop( pAig );
}
// output flop values (unaffected by the minimization)
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "%s@0=%c ", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
// output PI values (while skipping the minimized ones)
for ( f = 0; f <= pCex->iFrame; f++ )
Abc_NtkForEachPi( pNtk, pObj, i )
fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
Abc_CexFreeP( &pCare );
}
else
{
@ -2125,11 +2149,13 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: write_counter [-snh] <file>\n" );
fprintf( pAbc->Err, "usage: write_counter [-snmvh] <file>\n" );
fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" );
fprintf( pAbc->Err, "\t-s : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
fprintf( pAbc->Err, "\t-m : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
return 1;

20
src/misc/util/utilCex.c
View File

@ -196,7 +196,7 @@ void Abc_CexPrintStats( Abc_Cex_t * p )
for ( k = 0; k < p->nBits; k++ )
Counter += Abc_InfoHasBit(p->pData, k);
printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d nOnes = %5d (%5.2f %%)\n",
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / p->nBits );
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
}
/**Function*************************************************************
@ -233,6 +233,24 @@ void Abc_CexPrint( Abc_Cex_t * p )
assert( k == p->nBits );
}
/**Function*************************************************************
Synopsis [Frees the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_CexFreeP( Abc_Cex_t ** p )
{
if ( *p == NULL )
return;
ABC_FREE( *p );
}
/**Function*************************************************************
Synopsis [Frees the counter-example.]

1
src/misc/util/utilCex.h
View File

@ -63,6 +63,7 @@ extern Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew );
extern Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo );
extern void Abc_CexPrintStats( Abc_Cex_t * p );
extern void Abc_CexPrint( Abc_Cex_t * p );
extern void Abc_CexFreeP( Abc_Cex_t ** p );
extern void Abc_CexFree( Abc_Cex_t * p );
ABC_NAMESPACE_HEADER_END