summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abcFanio.c39
-rw-r--r--src/base/abci/abc.c130
-rw-r--r--src/base/abci/abcDar.c67
-rw-r--r--src/base/abci/abcFraig.c12
-rw-r--r--src/base/abci/abcIf.c8
-rw-r--r--src/base/abci/abcQbf.c2
-rw-r--r--src/base/io/ioWriteAiger.c4
7 files changed, 204 insertions, 58 deletions
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index ff6d0590..c8536695 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -30,6 +30,45 @@
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry )
+{
+ if ( p->nSize == p->nCap )
+ {
+ int * pArray;
+ int i;
+
+ if ( p->nSize == 0 )
+ p->nCap = 1;
+ if ( pMemMan )
+ pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
+ else
+ pArray = ALLOC( int, p->nCap * 2 );
+ if ( p->pArray )
+ {
+ for ( i = 0; i < p->nSize; i++ )
+ pArray[i] = p->pArray[i];
+ if ( pMemMan )
+ Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
+ else
+ free( p->pArray );
+ }
+ p->nCap *= 2;
+ p->pArray = pArray;
+ }
+ p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
Synopsis [Creates fanout/fanin relationship between the nodes.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 571aa02c..22a8ad54 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -115,6 +115,7 @@ static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCompress2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDChoice ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -283,6 +284,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "drw", Abc_CommandDRewrite, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drf", Abc_CommandDRefactor, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dcompress2", Abc_CommandDCompress2, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "dchoice", Abc_CommandDChoice, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drwsat", Abc_CommandDrwsat, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 );
@@ -2977,8 +2979,8 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
- printf("This command will be available soon\n");
- return 0;
+// printf("This command will be available soon\n");
+// return 0;
// set defaults
memset( pPars, 0, sizeof(Lpk_Par_t) );
@@ -6177,6 +6179,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
int nLevels;
+ int fVerbose;
// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
// extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
@@ -6187,15 +6190,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ fVerbose = 0;
nLevels = 1000;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
{
switch ( c )
{
@@ -6210,6 +6215,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nLevels < 0 )
goto usage;
break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -6311,7 +6319,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// pNtkRes = Abc_NtkDar( pNtk );
- pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
+// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
+ pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -6323,6 +6332,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: test [-h]\n" );
fprintf( pErr, "\t testbench for new procedures\n" );
+ 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;
}
@@ -7138,6 +7148,84 @@ usage:
return 1;
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int fBalance, fVerbose, fUpdateLevel, c;
+
+ extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fBalance = 1;
+ fUpdateLevel = 1;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'b':
+ fBalance ^= 1;
+ break;
+ case 'l':
+ fUpdateLevel ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "This command works only for strashed networks.\n" );
+ return 1;
+ }
+ pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: dchoice [-blvh]\n" );
+ fprintf( pErr, "\t performs partitioned choicing using a new AIG package\n" );
+ fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
+ fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
Synopsis []
@@ -11819,24 +11907,24 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFrames = 0; // if 0, iterates through frames
+ nFrames =16;
fRetimeFirst = 1;
fVerbose = 0;
fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF )
{
switch ( c )
{
- case 'F':
+ case 'K':
if ( globalUtilOptind >= argc )
{
- fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nFrames <= 0 )
+ if ( nFrames < 0 )
goto usage;
break;
case 'r':
@@ -11872,9 +11960,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dsec [-F num] [-rwvh] <file1> <file2>\n" );
+ fprintf( pErr, "usage: dsec [-K num] [-rwvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs inductive sequential equivalence checking\n" );
- fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
@@ -11914,24 +12002,24 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFrames = 0; // if 0, iterates through frames
- fRetimeFirst = 1;
- fVerbose = 0;
- fVeryVerbose = 0;
+ nFrames = 16;
+ fRetimeFirst = 1;
+ fVerbose = 0;
+ fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF )
{
switch ( c )
{
- case 'F':
+ case 'K':
if ( globalUtilOptind >= argc )
{
- fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nFrames <= 0 )
+ if ( nFrames < 0 )
goto usage;
break;
case 'r':
@@ -11964,9 +12052,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
+ fprintf( pErr, "usage: dprove [-K num] [-rwvh]\n" );
fprintf( pErr, "\t performs SEC on the sequential miter\n" );
- fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index f8f7d20e..356a5565 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -67,6 +67,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
}
// create the manager
pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
+ pMan->pName = Extra_UtilStrsav( pNtk->pName );
// save the number of registers
if ( fRegisters )
pMan->nRegs = Abc_NtkLatchNum(pNtk);
@@ -250,6 +251,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
Aig_ManForEachPi( pMan, pObj, i )
pObj->pData = Abc_NtkCi(pNtkNew, i);
+
// rebuild the AIG
vNodes = Aig_ManDfsChoices( pMan );
Vec_PtrForEachEntry( vNodes, pObj, i )
@@ -265,21 +267,8 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
pAbcRepr->pData = pAbcObj;
}
}
-printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
+//printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
Vec_PtrFree( vNodes );
-/*
- {
- Abc_Obj_t * pNode;
- int k, Counter = 0;
- Abc_NtkForEachNode( pNtkNew, pNode, k )
- if ( pNode->pData != 0 )
- {
- int x = 0;
- Counter++;
- }
- printf( "Choices = %d.\n", Counter );
- }
-*/
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
@@ -496,11 +485,11 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
return NULL;
Fra_ParamsDefault( pPars );
pPars->nBTLimitNode = nConfLimit;
- pPars->fVerbose = fVerbose;
- pPars->fProve = fProve;
+ pPars->fChoicing = fChoicing;
pPars->fDoSparse = fDoSparse;
pPars->fSpeculate = fSpeculate;
- pPars->fChoicing = fChoicing;
+ pPars->fProve = fProve;
+ pPars->fVerbose = fVerbose;
pMan = Fra_FraigPerform( pTemp = pMan, pPars );
if ( fChoicing )
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
@@ -631,7 +620,7 @@ clk = clock();
***********************************************************************/
Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
{
- Aig_Man_t * pMan;//, * pTemp;
+ Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
int clk;
assert( Abc_NtkIsStrash(pNtk) );
@@ -641,8 +630,8 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
// Aig_ManPrintStats( pMan );
clk = clock();
- pMan = Dar_ManCompress2( pMan, fBalance, fUpdateLevel, fVerbose );
-// Aig_ManStop( pTemp );
+ pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
+ Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
// Aig_ManPrintStats( pMan );
@@ -662,9 +651,35 @@ clk = clock();
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
+{
+ Aig_Man_t * pMan, * pTemp;
+ Abc_Ntk_t * pNtkAig;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0 );
+ if ( pMan == NULL )
+ return NULL;
+ pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
+ Aig_ManStop( pTemp );
+ pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
{
- Aig_Man_t * pMan;//, * pTemp;
+ Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
int clk;
assert( Abc_NtkIsStrash(pNtk) );
@@ -674,8 +689,8 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
// Aig_ManPrintStats( pMan );
clk = clock();
- pMan = Dar_ManRwsat( pMan, fBalance, fVerbose );
-// Aig_ManStop( pTemp );
+ pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose );
+ Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
// Aig_ManPrintStats( pMan );
@@ -1118,8 +1133,10 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbos
Aig_ManSeqCleanup( pMan );
if ( fLatchSweep )
{
- pMan = Aig_ManReduceLaches( pMan, fVerbose );
- pMan = Aig_ManConstReduce( pMan, fVerbose );
+ if ( pMan->nRegs )
+ pMan = Aig_ManReduceLaches( pMan, fVerbose );
+ if ( pMan->nRegs )
+ pMan = Aig_ManConstReduce( pMan, fVerbose );
}
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
Aig_ManStop( pMan );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 64cb2b38..be8a25f1 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -673,7 +673,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
}
}
Vec_PtrPush( vStore, pNtk );
- printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
+// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
return 1;
}
@@ -704,9 +704,15 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
printf( "There are no network currently in storage.\n" );
return NULL;
}
- printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
+// printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
pNtk = Vec_PtrEntry( vStore, 0 );
+ // swap the first and last network
+ // this should lead to the primary choice being "better" because of synthesis
+ pNtk = Vec_PtrPop( vStore );
+ Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) );
+ Vec_PtrWriteEntry( vStore, 0, pNtk );
+
// to determine the number of simulation patterns
// use the following strategy
// at least 64 words (32 words random and 32 words dynamic)
@@ -731,7 +737,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
// perform partitioned computation of structural choices
pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
Abc_NtkFraigStoreClean();
-PRT( "Total choicing time", clock() - clk );
+//PRT( "Total choicing time", clock() - clk );
return pFraig;
}
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index a9c42ceb..bb56c22c 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -299,12 +299,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
}
else
{
- extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
- // transform truth table into the decomposition tree
- Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
- // derive the AIG for the decomposition tree
- pNodeNew->pData = Kit_GraphToHop( pNtkNew->pManFunc, pGraph );
- Kit_GraphFree( pGraph );
+ extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
+ pNodeNew->pData = Kit_TruthToHop( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
}
// complement the node if the cut was complemented
if ( pCutBest->fCompl )
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index 6d4e480b..b839f812 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -140,7 +140,7 @@ clkV = clock() - clkV;
printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
printf( " " );
- PRTn( "Syn", clkS );
+// PRTn( "Syn", clkS );
PRT( "Ver", clkV );
}
}
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 958e3d96..e805fbc2 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -249,8 +249,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
// write the comment
fprintf( pFile, "c\n" );
fprintf( pFile, "%s\n", pNtk->pName );
- fprintf( pFile, "This file in the AIGER format was written by ABC on %s\n", Extra_TimeStamp() );
- fprintf( pFile, "For information about the format, refer to %s\n", "http://fmv.jku.at/aiger" );
+ fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
+ fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
fclose( pFile );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-29 23:00:23 +0000