diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-11 20:56:05 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-11 20:56:05 -0800 |
commit | 3beb36778ec35702690833e6a5d01498d1113b28 (patch) | |
tree | bf9a89c9505ee2badb4eae7983cd2f2f03f90136 /src | |
parent | 9fe4c74952691c3a6cc87dc85edb43da11dd8c8e (diff) | |
download | abc-3beb36778ec35702690833e6a5d01498d1113b28.tar.gz abc-3beb36778ec35702690833e6a5d01498d1113b28.tar.bz2 abc-3beb36778ec35702690833e6a5d01498d1113b28.zip |
Enabled counter-example minimization in 'write_counter'.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigAbsCba.c | 12 | ||||
-rw-r--r-- | src/base/abci/abc.c | 2 | ||||
-rw-r--r-- | src/base/io/io.c | 36 | ||||
-rw-r--r-- | src/misc/util/utilCex.c | 20 | ||||
-rw-r--r-- | src/misc/util/utilCex.h | 1 |
6 files changed, 62 insertions, 11 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 96fdde5e..9f98a8f9 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -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 ==========================================================*/ diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index 32b9c129..15f2bdfd 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -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; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c412c42e..a1d32f5b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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 ); } diff --git a/src/base/io/io.c b/src/base/io/io.c index 1c82d91b..3d1a6ae3 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -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; diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 72989535..37205543 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -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************************************************************* @@ -244,6 +244,24 @@ void Abc_CexPrint( Abc_Cex_t * p ) SeeAlso [] ***********************************************************************/ +void Abc_CexFreeP( Abc_Cex_t ** p ) +{ + if ( *p == NULL ) + return; + ABC_FREE( *p ); +} + +/**Function************************************************************* + + Synopsis [Frees the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Abc_CexFree( Abc_Cex_t * p ) { ABC_FREE( p ); diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h index c52806fc..556f2268 100644 --- a/src/misc/util/utilCex.h +++ b/src/misc/util/utilCex.h @@ -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 |