summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaAiger.c2
-rw-r--r--src/aig/gia/giaDup.c7
-rw-r--r--src/aig/gia/giaRex.c2
-rw-r--r--src/aig/gia/giaTim.c2
-rw-r--r--src/base/abci/abc.c2
-rw-r--r--src/base/cba/cbaBlast.c2
-rw-r--r--src/base/io/io.c56
-rw-r--r--src/base/wlc/wlc.h1
-rw-r--r--src/base/wlc/wlcBlast.c26
-rw-r--r--src/base/wlc/wlcCom.c8
-rw-r--r--src/base/wlc/wlcReadVer.c4
12 files changed, 96 insertions, 18 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index e7e64302..2e888130 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1313,7 +1313,7 @@ extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl );
-extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose );
+extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int nNewPis, int fGiaSimple, int fVerbose );
extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManTransformMiter2( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 03929aff..47986faa 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -848,7 +848,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
}
}
pInit[i] = 0;
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, fGiaSimple, 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, fGiaSimple, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
ABC_FREE( pInit );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index e868e3ae..ae38a95a 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -3047,7 +3047,7 @@ Gia_Man_t * Gia_ManTransformDualOutput( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose )
+Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int nNewPis, int fGiaSimple, int fVerbose )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@@ -3072,6 +3072,9 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int
// create additional primary inputs
for ( i = Gia_ManPiNum(p); i < CountPis; i++ )
Gia_ManAppendCi( pNew );
+ // create additional primary inputs
+ for ( i = 0; i < nNewPis; i++ )
+ Gia_ManAppendCi( pNew );
// create flop outputs
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
@@ -3137,7 +3140,7 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose )
for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
assert( pInit[i] == 'x' || pInit[i] == 'X' );
// normalize the manager
- pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, fVerbose );
+ pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, 0, fVerbose );
// create new init string
pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc)+1 );
for ( i = 0; i < Gia_ManPiNum(pStart); i++ )
diff --git a/src/aig/gia/giaRex.c b/src/aig/gia/giaRex.c
index ebfc9401..7f8d365e 100644
--- a/src/aig/gia/giaRex.c
+++ b/src/aig/gia/giaRex.c
@@ -309,7 +309,7 @@ Gia_Man_t * Gia_ManRex2Gia( char * pStrInit, int fOrder, int fVerbose )
Gia_ManStop( pTemp );
// add initial state
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0, 0 );
Gia_ManStop( pTemp );
Vec_StrFree( vInit );
/*
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index e136f68f..3f65d65f 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -874,7 +874,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
pInit[i] = 'X';
}
pInit[i] = 0;
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 0, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
ABC_FREE( pInit );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bcd876a3..974cf0f4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29478,7 +29478,7 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
Aig_ManStop( pAig );
// perform undc/zero
pInits = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur );
- pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, 0, fVerbose );
+ pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, 0, 0, fVerbose );
Gia_ManStop( pTemp );
ABC_FREE( pInits );
}
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
index 490a36eb..937b9b69 100644
--- a/src/base/cba/cbaBlast.c
+++ b/src/base/cba/cbaBlast.c
@@ -1013,7 +1013,7 @@ Gia_Man_t * Cba_NtkBlast( Cba_Ntk_t * p, int fSeq )
{
Gia_ManSetRegNum( pNew, Vec_StrSize(vInit) );
Vec_StrPush( vInit, '\0' );
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0, 1 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
Vec_StrFreeP( &vInit );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index a85d64ef..ea46ac66 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2317,10 +2317,11 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
int forceSeq = 0;
int fAiger = 0;
int fPrintFull = 0;
+ int fUseFfNames = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvh" ) ) != EOF )
{
switch ( c )
{
@@ -2351,6 +2352,9 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
case 'f':
fPrintFull ^= 1;
break;
+ case 'z':
+ fUseFfNames ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -2444,6 +2448,46 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
}
fprintf( pFile, "\n");
fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
+ if ( fUseFfNames )
+ {
+ int * pValues;
+ int nXValues = 0, iFlop = 0, iPivotPi = -1;
+ Abc_NtkForEachPi( pNtk, pObj, iPivotPi )
+ if ( !strcmp(Abc_ObjName(pObj), "_abc_190121_abc_") )
+ break;
+ if ( iPivotPi == Abc_NtkPiNum(pNtk) )
+ {
+ fprintf( stdout, "IoCommandWriteCex(): Cannot find special PI required by switch \"-z\".\n" );
+ return 1;
+ }
+ // count X-valued flops
+ for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
+ if ( Abc_ObjName(Abc_NtkPi(pNtk, i))[0] == 'x' )
+ nXValues++;
+ // map X-valued flops into auxiliary PIs
+ pValues = ABC_FALLOC( int, Abc_NtkPiNum(pNtk) );
+ for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
+ if ( Abc_ObjName(Abc_NtkPi(pNtk, i))[0] == 'x' )
+ pValues[i] = iPivotPi - nXValues + iFlop++;
+ assert( iFlop == nXValues );
+ // write flop values
+ for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
+ if ( pValues[i] == -1 )
+ fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_NtkPi(pNtk, i))+1, Abc_ObjName(Abc_NtkPi(pNtk, i))[0] );
+ else if ( Abc_InfoHasBit(pCare->pData, pCare->nRegs + pValues[i]) )
+ fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_NtkPi(pNtk, i))+1, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs + pValues[i]) );
+ ABC_FREE( pValues );
+ // output PI values (while skipping the minimized ones)
+ for ( f = 0; f <= pCex->iFrame; f++ )
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ {
+ if ( i == iPivotPi - nXValues ) break;
+ if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
+ fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+ }
+ }
+ else
+ {
// output flop values (unaffected by the minimization)
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
@@ -2452,6 +2496,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
Abc_NtkForEachPi( pNtk, pObj, i )
if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+ }
Abc_CexFreeP( &pCare );
}
else
@@ -2498,7 +2543,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
- fprintf( pAbc->Err, "usage: write_cex [-snmueocfvh] <file>\n" );
+ fprintf( pAbc->Err, "usage: write_cex [-snmueocfzvh] <file>\n" );
fprintf( pAbc->Err, "\t saves counter-example (CEX) derived by \"sat\", \"iprove\", \"dprove\", etc\n" );
fprintf( pAbc->Err, "\t the output file <file> contains values for each PI in natural order\n" );
fprintf( pAbc->Err, "\t-s : always report a sequential CEX (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
@@ -2508,9 +2553,10 @@ usage:
fprintf( pAbc->Err, "\t-e : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" );
fprintf( pAbc->Err, "\t-o : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
- fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s].\n", fAiger? "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-a : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
+ fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" );
+ fprintf( pAbc->Err, "\t-z : toggle using saved flop names [default = %s]\n", fUseFfNames? "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, "\t<file> : the name of the file to write\n" );
return 1;
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 6547da13..a04e19e8 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -214,6 +214,7 @@ struct Wlc_BstPar_t_
int fNoCleanup;
int fCreateMiter;
int fDecMuxes;
+ int fSaveFfNames;
int fVerbose;
Vec_Int_t * vBoxIds;
};
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 01b6e64c..9b55c008 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -2055,7 +2055,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
}
else
{
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, pPar->fGiaSimple, 0 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, pPar->fSaveFfNames ? 1+Gia_ManRegNum(pNew) : 0, pPar->fGiaSimple, 0 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
}
@@ -2121,10 +2121,13 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
if ( p->pInits[i] == 'x' || p->pInits[i] == 'X' )
{
char Buffer[100];
- sprintf( Buffer, "%s%d", "init", i );
+ sprintf( Buffer, "_%s_abc_%d_", "init", i );
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
fAdded = 1;
}
+ if ( pPar->fSaveFfNames )
+ for ( i = 0; i < 1+Length; i++ )
+ Vec_PtrPush( pNew->vNamesIn, NULL );
}
Wlc_NtkForEachCi( p, pObj, i )
if ( !Wlc_ObjIsPi(pObj) )
@@ -2173,6 +2176,25 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
}
}
+ if ( p->pInits && pPar->fSaveFfNames )
+ {
+ char * pName;
+ int Length = (int)strlen(p->pInits);
+ int NameStart = Vec_PtrSize(pNew->vNamesIn)-Length;
+ int NullStart = Vec_PtrSize(pNew->vNamesIn)-2*Length;
+ int SepStart = Vec_PtrSize(pNew->vNamesIn)-2*Length-1;
+ assert( Vec_PtrEntry(pNew->vNamesIn, SepStart) == NULL );
+ Vec_PtrWriteEntry( pNew->vNamesIn, SepStart, Abc_UtilStrsav("_abc_190121_abc_") );
+ for ( i = 0; i < Length; i++ )
+ {
+ char Buffer[100];
+ sprintf( Buffer, "%c%s", p->pInits[i], Vec_PtrEntry(pNew->vNamesIn, NameStart+i) );
+ assert( Vec_PtrEntry(pNew->vNamesIn, NullStart+i) == NULL );
+ Vec_PtrWriteEntry( pNew->vNamesIn, NullStart+i, Abc_UtilStrsav(Buffer) );
+ }
+ Vec_PtrForEachEntry( char *, pNew->vNamesIn, pName, i )
+ assert( pName != NULL );
+ }
if ( p->pInits && fAdded )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav("abc_reset_flop") );
if ( pPar->vBoxIds )
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 5e69000f..3031f331 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -978,7 +978,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_BstParDefault( pPar );
pPar->nOutputRange = 2;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombadstnivh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombadstnizvh" ) ) != EOF )
{
switch ( c )
{
@@ -1057,6 +1057,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'i':
fPrintInputInfo ^= 1;
break;
+ case 'z':
+ pPar->fSaveFfNames ^= 1;
+ break;
case 'v':
pPar->fVerbose ^= 1;
break;
@@ -1125,7 +1128,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameUpdateGia( pAbc, pNew );
return 0;
usage:
- Abc_Print( -2, "usage: %%blast [-ORAM num] [-combadstnivh]\n" );
+ Abc_Print( -2, "usage: %%blast [-ORAM num] [-combadstnizvh]\n" );
Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", pPar->iOutput );
Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n", pPar->nOutputRange );
@@ -1141,6 +1144,7 @@ usage:
Abc_Print( -2, "\t-t : toggle creating regular multi-output miter [default = %s]\n", fMiter? "yes": "no" );
Abc_Print( -2, "\t-n : toggle dumping signal names into a text file [default = %s]\n", fDumpNames? "yes": "no" );
Abc_Print( -2, "\t-i : toggle to print input names after blasting [default = %s]\n", fPrintInputInfo ? "yes": "no" );
+ Abc_Print( -2, "\t-z : toggle saving flop names after blasting [default = %s]\n", pPar->fSaveFfNames ? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPar->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index db2cf3b2..9c40e71e 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -457,7 +457,7 @@ char * Wlc_PrsConvertInitValues( Wlc_Ntk_t * p )
pObj = Wlc_NtkObj( p, Wlc_ObjFaninId0(pObj) );
pInits = (pObj->Type == WLC_OBJ_CONST && !pObj->fXConst) ? Wlc_ObjConstValue(pObj) : NULL;
for ( k = 0; k < Abc_MinInt(Value, Wlc_ObjRange(pObj)); k++ )
- Vec_StrPush( vStr, (char)(pInits ? '0' + Abc_InfoHasBit((unsigned *)pInits, k) : 'X') );
+ Vec_StrPush( vStr, (char)(pInits ? '0' + Abc_InfoHasBit((unsigned *)pInits, k) : 'x') );
// extend values with zero, in case the init value signal has different range compared to constant used
for ( ; k < Value; k++ )
Vec_StrPush( vStr, '0' );
@@ -588,6 +588,8 @@ static inline char * Wlc_PrsReadConstant( Wlc_Prs_t * p, char * pStr, Vec_Int_t
if ( pStr[1] != 'h' )
return (char *)(ABC_PTRINT_T)Wlc_PrsWriteErrorMessage( p, pStr, "Expecting hexadecimal constant and not \"%c\".", pStr[1] );
*pXValue = (pStr[2] == 'x' || pStr[2] == 'X');
+ if ( *pXValue == 'X' )
+ *pXValue = 'x';
Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 );
if ( nDigits != (nBits + 3)/4 )
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 11:15:42 +0000