diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-11 10:49:36 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-11 10:49:36 +0700 |
| commit | af84c0d2056ecd11e057990c7d717c0a2e984941 (patch) | |
| tree | 0ca43e9d5c5a5ea00a34a9374823caf32a51b071 /src/sat/pdr | |
| parent | 3a6c8f1c429e556332fcc8544ca06cc58270bd7e (diff) | |
| download | abc-af84c0d2056ecd11e057990c7d717c0a2e984941.tar.gz abc-af84c0d2056ecd11e057990c7d717c0a2e984941.tar.bz2 abc-af84c0d2056ecd11e057990c7d717c0a2e984941.zip | |
Added printout of flop names in the PLA file representing the invariant.
Diffstat (limited to 'src/sat/pdr')
| -rw-r--r-- | src/sat/pdr/pdrInv.c | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c index a60732cb..e2e3cdb7 100644 --- a/src/sat/pdr/pdrInv.c +++ b/src/sat/pdr/pdrInv.c @@ -18,6 +18,9 @@ ***********************************************************************/ +#include "abc.h" // for Abc_NtkCollectCioNames() +#include "main.h" // for Abc_FrameReadGlobalFrame() + #include "pdrInt.h" #include "extra.h" @@ -231,6 +234,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName ) Vec_Int_t * vFlopCounts; Vec_Ptr_t * vCubes; Pdr_Set_t * pCube; + char ** pNamesCi; int i, kStart; // create file pFile = fopen( pFileName, "w" ); @@ -251,6 +255,18 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName ) fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) ); fprintf( pFile, ".o 1\n" ); fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) ); + // output flop names + pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 ); + if ( pNamesCi ) + { + fprintf( pFile, ".ilb" ); + for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) + if ( !fUseSupp || Vec_IntEntry( vFlopCounts, i ) ) + fprintf( pFile, " %s", pNamesCi[Saig_ManPiNum(p->pAig) + i] ); + fprintf( pFile, "\n" ); + ABC_FREE( pNamesCi ); + fprintf( pFile, ".ob inv\n" ); + } // output cubes Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i ) { |