summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c152
-rw-r--r--src/base/abci/abcBmc.c2
-rw-r--r--src/base/abci/abcDar.c17
-rw-r--r--src/base/abci/abcFxu.c4
-rw-r--r--src/base/abci/abcHaig.c2
-rw-r--r--src/base/abci/abcMv.c2
-rw-r--r--src/base/abci/abcPrint.c2
-rw-r--r--src/base/abci/abcReach.c2
-rw-r--r--src/base/abci/abcSat.c2
-rw-r--r--src/base/abci/abcSweep.c2
-rw-r--r--src/base/abci/abcUnreach.c2
-rw-r--r--src/base/abci/abcVerify.c2
12 files changed, 152 insertions, 39 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ef7969be..c48b7e95 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27,7 +27,7 @@
#include "if.h"
#include "res.h"
#include "lpk.h"
-#include "aig.h"
+#include "giaAig.h"
#include "dar.h"
#include "mfs.h"
#include "mfx.h"
@@ -39,7 +39,6 @@
#include "ssw.h"
#include "cgt.h"
#include "amap.h"
-#include "gia.h"
#include "cec.h"
////////////////////////////////////////////////////////////////////////
@@ -194,6 +193,7 @@ static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneHot ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -513,6 +513,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "onehot", Abc_CommandOneHot, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "dretime", Abc_CommandDRetime, 1 );
@@ -598,7 +599,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "AIG", "&psig", Abc_CommandAbc9PSig, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&status", Abc_CommandAbc9Status, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&show", Abc_CommandAbc9Show, 0 );
- Cmd_CommandAdd( pAbc, "AIG", "&hash", Abc_CommandAbc9Hash, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&st", Abc_CommandAbc9Hash, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&topand", Abc_CommandAbc9Topand, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&cof", Abc_CommandAbc9Cof, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&trim", Abc_CommandAbc9Trim, 0 );
@@ -11945,7 +11946,7 @@ usage:
fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->fEpsilon );
fprintf( pErr, "\t-m : toggles using MUX matching [default = %s]\n", pPars->fUseMuxes? "yes": "no" );
fprintf( pErr, "\t-x : toggles using XOR matching [default = %s]\n", pPars->fUseXors? "yes": "no" );
- fprintf( pErr, "\t-i : toggles assuming inverters are ABC_FREE [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
+ fprintf( pErr, "\t-i : toggles assuming inverters are free [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -13094,7 +13095,74 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: undc [-h]\n" );
- fprintf( pErr, "\t converts latches with DC init values into ABC_FREE PIs\n" );
+ fprintf( pErr, "\t converts latches with DC init values into free PIs\n" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandOneHot( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c;
+ extern Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsComb(pNtk) )
+ {
+ fprintf( pErr, "The current network is combinational.\n" );
+ return 0;
+ }
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( pErr, "This command works only for logic networks.\n" );
+ return 0;
+ }
+ // get the new network
+ pNtkRes = Abc_NtkConvertOnehot( pNtk );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Converting to one-hot encoding has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: onehot [-h]\n" );
+ fprintf( pErr, "\t converts natural encoding into one-hot encoding\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -15030,7 +15098,7 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fNew = 1;
+ fNew = 0;
fComb = 0;
nFrames = 32;
nWords = 8;
@@ -18381,22 +18449,28 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConfMax;
int fDynamic;
int fExtend;
+ int fSkipProof;
+ int nFramesBmc;
+ int nConfMaxBmc;
int fVerbose;
int c;
- extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFramesMax = 10;
- nConfMax = 10000;
- fDynamic = 1;
- fExtend = 0;
- fVerbose = 0;
+ nFramesMax = 10;
+ nConfMax = 10000;
+ fDynamic = 1;
+ fExtend = 0;
+ fSkipProof = 0;
+ nFramesBmc = 2000;
+ nConfMaxBmc = 5000;
+ fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF )
{
switch ( c )
{
@@ -18422,12 +18496,37 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMax < 0 )
goto usage;
break;
+ case 'G':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFramesBmc = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFramesBmc < 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfMaxBmc = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfMaxBmc < 0 )
+ goto usage;
+ break;
case 'd':
fDynamic ^= 1;
break;
case 'e':
fExtend ^= 1;
break;
+ case 's':
+ fSkipProof ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -18454,7 +18553,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
- pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
+ pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pNtkRes == NULL )
{
if ( pNtk->pSeqModel == NULL )
@@ -18465,12 +18564,16 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
- fprintf( pErr, "usage: abs [-FC num] [-devh]\n" );
- fprintf( pErr, "\t proof-based abstraction from UNSAT core of the BMC instance\n" );
- fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
- fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
+ fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" );
+ fprintf( pErr, "\t proof-based abstraction (PBA) using UNSAT core of BMC\n" );
+ fprintf( pErr, "\t followed by counter-example-based abstraction\n" );
+ fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax );
+ fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax );
+ fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc );
+ fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc );
fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
+ fprintf( pErr, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -22128,11 +22231,15 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c;
+ int fAddStrash = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
{
switch ( c )
{
+ case 'a':
+ fAddStrash ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -22144,13 +22251,14 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
return 1;
}
- pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig );
+ pAbc->pAig = Gia_ManRehash( pTemp = pAbc->pAig, fAddStrash );
Gia_ManStop( pTemp );
return 0;
usage:
- fprintf( stdout, "usage: &hash [-h]\n" );
+ fprintf( stdout, "usage: &st [-ah]\n" );
fprintf( stdout, "\t performs structural hashing\n" );
+ fprintf( stdout, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@@ -22186,7 +22294,7 @@ int Abc_CommandAbc9Topand( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pAig == NULL )
{
- printf( "Abc_CommandAbc9Hash(): There is no AIG.\n" );
+ printf( "Abc_CommandAbc9Topand(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pAig) > 0 )
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
index d2c5a12c..1512c76f 100644
--- a/src/base/abci/abcBmc.c
+++ b/src/base/abci/abcBmc.c
@@ -64,7 +64,7 @@ printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
// report the classes
// if ( fVerbose )
// Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
- // ABC_FREE stuff
+ // free stuff
Vec_PtrFree( vMapping );
Ivy_ManStop( pFraig );
Ivy_ManStop( pFrames );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 91046340..840068d6 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -19,7 +19,7 @@
***********************************************************************/
#include "abc.h"
-#include "aig.h"
+#include "giaAig.h"
#include "saig.h"
#include "dar.h"
#include "cnf.h"
@@ -2299,7 +2299,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
RetValue = 1;
- }
+ }
else
{
RetValue = 0;
@@ -2375,7 +2375,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
pGia = Gia_ManFromAig( pMan );
if ( Gia_ManSimSimulate( pGia, pPars ) )
{
- if ( (pCex = pMan->pSeqModel) )
+ if ( (pCex = (Fra_Cex_t *)pGia->pCexSeq) )
{
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
@@ -2404,8 +2404,13 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
{
pCex = Fra_SmlGetCounterExample( pSml );
if ( pCex )
+ {
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pCex;
@@ -2557,7 +2562,7 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
@@ -2567,7 +2572,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, 0, fVerbose );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
if ( pTemp->pSeqModel )
{
ABC_FREE( pNtk->pModel );
@@ -3380,7 +3385,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
return NULL;
/*
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, 1 );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 1596e774..6109870e 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -177,12 +177,12 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
{
int i;
- // ABC_FREE the arrays of new fanins
+ // free the arrays of new fanins
if ( p->vFaninsNew )
for ( i = 0; i < p->vFaninsNew->nSize; i++ )
if ( p->vFaninsNew->pArray[i] )
Vec_IntFree( p->vFaninsNew->pArray[i] );
- // ABC_FREE the arrays
+ // free the arrays
if ( p->vSops ) Vec_PtrFree( p->vSops );
if ( p->vSopsNew ) Vec_PtrFree( p->vSopsNew );
if ( p->vFanins ) Vec_PtrFree( p->vFanins );
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index 569275f2..3f3fefcd 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -691,7 +691,7 @@ Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
Hop_ManStop( pMan );
- // ABC_FREE HAIG
+ // free HAIG
return pNtkAig;
}
diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c
index dacd16b2..8ea3697f 100644
--- a/src/base/abci/abcMv.c
+++ b/src/base/abci/abcMv.c
@@ -349,7 +349,7 @@ void Abc_MvDecompose( Mv_Man_t * p )
printf( "%d ", Vec_PtrSize(vCofs) );
Vec_PtrFree( vCofs );
- // ABC_FREE the cofactors
+ // free the cofactors
for ( v1 = 0; v1 < 4; v1++ )
for ( v2 = 0; v2 < 4; v2++ )
Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e65ce11a..d47dfe1f 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -64,7 +64,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
int nPis; // the number of primary inputs
int nPos; // the number of primary outputs
} ParsNew, ParsBest = { 0 };
- // ABC_FREE storage for the name
+ // free storage for the name
if ( pNtk == NULL )
{
ABC_FREE( ParsBest.pName );
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index 3834c00d..e25be81a 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -102,7 +102,7 @@ DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorde
bVar = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) ); Cudd_Ref( pbParts[i] );
}
- // ABC_FREE the global BDDs
+ // free the global BDDs
Abc_NtkFreeGlobalBdds( pNtk, 0 );
// reorder and disable reordering
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 3cee19ca..5e14116c 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -117,7 +117,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsL
pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
Vec_IntFree( vCiIds );
}
- // ABC_FREE the sat_solver
+ // free the sat_solver
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index d1f4d4f7..dfb8137c 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -111,7 +111,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose,
Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
stmm_free_table( tEquiv );
- // ABC_FREE the manager
+ // free the manager
Fraig_ManFree( pMan );
Abc_NtkDelete( pNtkAig );
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 196ff643..251d3953 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -143,7 +143,7 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
Cudd_RecursiveDeref( dd, bTemp );
Cudd_RecursiveDeref( dd, bProd );
}
- // ABC_FREE the global BDDs
+ // free the global BDDs
// Abc_NtkFreeGlobalBdds( pNtk );
Abc_NtkFreeGlobalBdds( pNtk, 0 );
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 60197d29..424c26ec 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -799,7 +799,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
for ( k = 0; k <= iFrame; k++ )
if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy )
pObj->pCopy = (void *)1;
- // ABC_FREE stuff
+ // free stuff
Vec_PtrFree( vSupp );
Abc_NtkDelete( pFrames );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-11 02:15:18 +0000