summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/saig/saig.h1
-rw-r--r--src/aig/saig/saigDup.c52
-rw-r--r--src/base/io/io.c51
3 files changed, 84 insertions, 20 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 99928a66..64bb3b02 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -168,6 +168,7 @@ extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
extern Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
+extern Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
extern Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit );
/*=== saigHaig.c ==========================================================*/
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 45c37c3b..ca06398c 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -315,6 +315,58 @@ int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
SeeAlso []
***********************************************************************/
+Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p )
+{
+ Abc_Cex_t * pNew;
+ Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+ int RetValue, i, k, iBit = 0;
+ // create new counter-example
+ pNew = Abc_CexAlloc( 0, Aig_ManPiNum(pAig), p->iFrame + 1 );
+ pNew->iPo = p->iPo;
+ pNew->iFrame = p->iFrame;
+ // simulate the AIG
+ Aig_ManCleanMarkB(pAig);
+ Aig_ManConst1(pAig)->fMarkB = 1;
+ Saig_ManForEachLo( pAig, pObj, i )
+ pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+ for ( i = 0; i <= p->iFrame; i++ )
+ {
+ Saig_ManForEachPi( pAig, pObj, k )
+ pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+ ///////// write PI+LO values ////////////
+ Aig_ManForEachPi( pAig, pObj, k )
+ if ( pObj->fMarkB )
+ Aig_InfoSetBit(pNew->pData, Aig_ManPiNum(pAig)*i + k);
+ /////////////////////////////////////////
+ Aig_ManForEachNode( pAig, pObj, k )
+ pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
+ (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+ Aig_ManForEachPo( pAig, pObj, k )
+ pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+ if ( i == p->iFrame )
+ break;
+ Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+ pObjRo->fMarkB = pObjRi->fMarkB;
+ }
+ assert( iBit == p->nBits );
+ RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB;
+ Aig_ManCleanMarkB(pAig);
+ if ( RetValue == 0 )
+ printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 2ed4b3b2..1cea2e37 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2018,17 +2018,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
{
Abc_Ntk_t * pNtk;
char * pFileName;
- int c, fNames;
- int fMinimize;
- int forceSeq;
- int fVerbose;
+ int c, fNames = 0;
+ int fMinimize = 0;
+ int forceSeq = 0;
+ int fPrintFull = 0;
+ int fVerbose = 0;
- fNames = 0;
- fMinimize = 0;
- forceSeq = 0;
- fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "snmvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "snmfvh" ) ) != EOF )
{
switch ( c )
{
@@ -2041,6 +2038,9 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
case 'm':
fMinimize ^= 1;
break;
+ case 'f':
+ fPrintFull ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -2050,28 +2050,25 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
goto usage;
}
}
-
pNtk = pAbc->pNtkCur;
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
-
+ if ( pNtk->pModel == NULL && pAbc->pCex == NULL )
+ {
+ fprintf( pAbc->Out, "Counter-example is not available.\n" );
+ return 0;
+ }
if ( argc != globalUtilOptind + 1 )
{
printf( "File name is missing on the command line.\n" );
goto usage;
}
+
// get the input file name
pFileName = argv[globalUtilOptind];
-
- if ( pNtk->pModel == NULL && pAbc->pCex == NULL )
- {
- fprintf( pAbc->Out, "Counter-example is not available.\n" );
- return 0;
- }
-
// write the counter-example into the file
if ( pAbc->pCex )
{
@@ -2093,7 +2090,20 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
return 1;
}
- if ( fNames )
+ if ( fPrintFull )
+ {
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+ Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+ Abc_Cex_t * pCexFull = Saig_ManExtendCex( pAig, pCex );
+ Aig_ManStop( pAig );
+ // output PI values (while skipping the minimized ones)
+ assert( pCexFull->nBits == Abc_NtkCiNum(pNtk) * (pCex->iFrame + 1) );
+ for ( f = 0; f <= pCex->iFrame; f++ )
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) );
+ Abc_CexFreeP( &pCexFull );
+ }
+ else if ( fNames )
{
Abc_Cex_t * pCare = NULL;
if ( fMinimize )
@@ -2154,12 +2164,13 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
- fprintf( pAbc->Err, "usage: write_counter [-snmvh] <file>\n" );
+ fprintf( pAbc->Err, "usage: write_counter [-snmfvh] <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-f : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "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" );
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-01 05:21:38 +0000