luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

treewide: Fix spelling mistakes 

A particularly pedantic set of changes currently used in Debian

Authored-By: Ruben Undheim <ruben.undheim@gmail.com>
This commit is contained in:
Daniel Gröber 2023-08-27 14:13:20 +02:00
parent 3309ccabd4
commit b7d1435db1
21 changed files with 40 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/saig/saigIso.c
View File

@ -493,7 +493,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV
// report the results
// Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
// printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
// printf( "Divided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
/*
if ( fVerbose )
{

2
src/aig/saig/saigIsoFast.c
View File

@ -328,7 +328,7 @@ Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig )
// report the results
// Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
printf( "Divided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
if ( Vec_IntSize(vLevel) > 1 )

2
src/aig/saig/saigMiter.c
View File

@ -946,7 +946,7 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
if ( (pFlop0->fMarkA && pFlop0->fMarkB) || (pFlop1->fMarkA && pFlop1->fMarkB) ||
(pFlop0->fMarkA && pFlop1->fMarkA) || (pFlop0->fMarkB && pFlop1->fMarkB) )
printf( "Ouput pair %4d: Difficult case...\n", i/2 );
printf( "Output pair %4d: Difficult case...\n", i/2 );
if ( pFlop0->fMarkB )
{

4
src/aig/saig/saigSimMv.c
View File

@ -903,14 +903,14 @@ ABC_PRT( "Constructing the problem", Abc_Clock() - clk );
if ( f == nFramesSatur )
{
if ( fVerbose )
printf( "Begining to saturate simulation after %d frames\n", f );
printf( "Beginning to saturate simulation after %d frames\n", f );
// find all flops that have at least one X value in the past and set them to X forever
p->vXFlops = Saig_MvManFindXFlops( p );
}
if ( f == 2 * nFramesSatur )
{
if ( fVerbose )
printf( "Agressively saturating simulation after %d frames\n", f );
printf( "Aggressively saturating simulation after %d frames\n", f );
Vec_IntFree( p->vXFlops );
p->vXFlops = Saig_MvManCreateNextSkip( p );
}

2
src/base/abc/abcLatch.c
View File

@ -426,7 +426,7 @@ Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
return Abc_NtkDup( pNtk );
if ( nFlops > 16 )
{
printf( "Cannot reencode %d flops because it will lead to 2^%d states.\n", nFlops, nFlops );
printf( "Cannot re-encode %d flops because it will lead to 2^%d states.\n", nFlops, nFlops );
return NULL;
}
// check if there are latches with DC values

24
src/base/abci/abc.c
View File

@ -774,7 +774,7 @@ void Abc_FrameUpdateGia( Abc_Frame_t * pAbc, Gia_Man_t * pNew )
{
if ( pNew == NULL )
{
Abc_Print( -1, "Abc_FrameUpdateGia(): Tranformation has failed.\n" );
Abc_Print( -1, "Abc_FrameUpdateGia(): Transformation has failed.\n" );
return;
}
if ( Gia_ManPoNum(pNew) == 0 )
@ -7001,7 +7001,7 @@ int Abc_CommandTestNpn( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: testnpn [-AN <num>] [-dbvh] <file>\n" );
Abc_Print( -2, "\t testbench for computing (semi-)canonical forms\n" );
Abc_Print( -2, "\t of completely-specified Boolean functions up to 16 varibles\n" );
Abc_Print( -2, "\t of completely-specified Boolean functions up to 16 variables\n" );
Abc_Print( -2, "\t-A <num> : semi-caninical form computation algorithm [default = %d]\n", NpnType );
Abc_Print( -2, "\t 0: uniqifying truth tables\n" );
Abc_Print( -2, "\t 1: exact NPN canonical form by brute-force enumeration\n" );
@ -13541,7 +13541,7 @@ usage:
Abc_Print( -2, "usage: gen [-NAKL num] [-atsembfnrgvh] <file>\n" );
Abc_Print( -2, "\t generates simple circuits\n" );
Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-A num : the number of agruments (for adder tree) [default = %d]\n", nArgs );
Abc_Print( -2, "\t-A num : the number of arguments (for adder tree) [default = %d]\n", nArgs );
Abc_Print( -2, "\t-K num : the LUT size (to be used with switch -f) [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-L num : the LUT count (to be used with switch -f) [default = %d]\n", nLuts );
Abc_Print( -2, "\t-a : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );
@ -20139,7 +20139,7 @@ usage:
Abc_Print( -2, "\t prints statistics of the DSD manager\n" );
Abc_Print( -2, "\t-N num : show structures whose ID divides by N [default = %d]\n", Number );
Abc_Print( -2, "\t-S num : show structures whose support size is S [default = %d]\n", Support );
Abc_Print( -2, "\t-o : toggles printing occurence distribution [default = %s]\n", fOccurs? "yes": "no" );
Abc_Print( -2, "\t-o : toggles printing occurrence distribution [default = %s]\n", fOccurs? "yes": "no" );
Abc_Print( -2, "\t-t : toggles dumping truth tables [default = %s]\n", fTtDump? "yes": "no" );
Abc_Print( -2, "\t-b : toggles processing second manager [default = %s]\n", fSecond? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
@ -26178,7 +26178,7 @@ usage:
Abc_Print( -2, "\t-Q num : Min clause LBD for binary resolution [default = %d]\n", opts.clause_min_lbd_bin_resol );
Abc_Print( -2, "\n\tConstants used for branching (VSIDS heuristic):\n");
Abc_Print( -2, "\t-R num : Clause activity decay factor (when using float clause activity) [default = %f]\n", opts.clause_decay );
Abc_Print( -2, "\t-S num : Varibale activity decay factor [default = %f]\n", opts.var_decay );
Abc_Print( -2, "\t-S num : Variable activity decay factor [default = %f]\n", opts.var_decay );
#ifdef SATOKO_ACT_VAR_FIXED
Abc_Print( -2, "\t-T num : Variable activity limit valeu [default = 0x%08X]\n", opts.var_act_limit );
Abc_Print( -2, "\t-U num : Variable activity re-scale factor [default = 0x%08X]\n", opts.var_act_rescale );
@ -27532,7 +27532,7 @@ usage:
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-T num : runtime limit, in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
Abc_Print( -2, "\t-H num : runtime limit per output, in milliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
Abc_Print( -2, "\t-G num : runtime gap since the last CEX, in seconds [default = %d]\n", pPars->nTimeOutGap );
Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );
@ -29066,7 +29066,7 @@ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Obj_t * pNodePo;
FILE * hadi = fopen("hadi.txt", "w");
Abc_NtkForEachPo( pNtk, pNodePo, i ) {
printf("Ouput %s\n\n", Abc_ObjName(pNodePo));
printf("Output %s\n\n", Abc_ObjName(pNodePo));
saucyGateWay( pNtk, pNodePo, gFile, 0, fLookForSwaps, fFixOutputs, fFixInputs, fQuiet, fPrintTree );
printf("----------------------------------------\n");
}
@ -29092,7 +29092,7 @@ int Abc_CommandSaucy( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: saucy3 [-O <name>] [-F <file>] [-iosqvh]\n\n" );
Abc_Print( -2, "\t computes functional symmetries of the netowrk\n" );
Abc_Print( -2, "\t computes functional symmetries of the network\n" );
Abc_Print( -2, "\t prints symmetry generators to the standard output\n" );
Abc_Print( -2, "\t-O <name> : (optional) compute symmetries only for output given by name\n");
Abc_Print( -2, "\t only inputs in the output cone are permuted\n");
@ -29480,7 +29480,7 @@ usage:
Abc_Print( -2, "\t-D num : limit on conflicts during ind-generalization (0 = no limit) [default = %d]\n",pPars->nConfGenLimit );
Abc_Print( -2, "\t-Q num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
Abc_Print( -2, "\t-H num : runtime limit per output, in milliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne );
Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap );
Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n", pPars->nRandomSeed );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
@ -34807,7 +34807,7 @@ usage:
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-s : toggle seq vs. comb simulation [default = %s]\n", pPars->fSeqSimulate? "yes": "no" );
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" );
Abc_Print( -2, "\t-d : toggle using two POs instead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@ -35258,7 +35258,7 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" );
Abc_Print( -2, "\t-d : toggle using two POs instead of XOR [default = %s]\n", pPars->fDualOut? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@ -45965,7 +45965,7 @@ usage:
Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", pPars->TimeOutLoc );
Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n", pPars->TimeOutInc );
Abc_Print( -2, "\t-G num : approximate gap runtime limit in seconds [default = %d]\n", pPars->TimeOutGap );
Abc_Print( -2, "\t-H num : timeout per output in miliseconds [default = %d]\n", pPars->TimePerOut );
Abc_Print( -2, "\t-H num : timeout per output in milliseconds [default = %d]\n", pPars->TimePerOut );
Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", pPars->fUseSyn? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping invariant into a file [default = %s]\n", pPars->fDumpFinal? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );

2
src/base/abci/abcCut.c
View File

@ -72,7 +72,7 @@ void Abc_NtkCutsSubtractFanunt( Abc_Ntk_t * pNtk )
Counter++;
}
}
printf("Substracted %d fanouts\n", Counter );
printf("Subtracted %d fanouts\n", Counter );
}
/**Function*************************************************************

6
src/base/cmd/cmd.c
View File

@ -740,7 +740,7 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: source [-psxh] <file_name>\n" );
fprintf( pAbc->Err, "\t-p supply prompt before reading each line [default = %s]\n", prompt? "yes": "no" );
fprintf( pAbc->Err, "\t-s silently ignore nonexistant file [default = %s]\n", silent? "yes": "no" );
fprintf( pAbc->Err, "\t-s silently ignore nonexistent file [default = %s]\n", silent? "yes": "no" );
fprintf( pAbc->Err, "\t-x echo each line as it is executed [default = %s]\n", echo? "yes": "no" );
fprintf( pAbc->Err, "\t-h print the command usage\n" );
return 1;
@ -2445,7 +2445,7 @@ int CmdCommandStarter( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: starter [-N num] [-C cmd] [-vh] <file>\n" );
Abc_Print( -2, "\t runs command lines listed in <file> concurrently on <num> CPUs\n" );
Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controler [default = %d]\n", nCores );
Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controller [default = %d]\n", nCores );
Abc_Print( -2, "\t-C cmd : (optional) ABC command line to execute on benchmarks in <file>\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@ -2557,7 +2557,7 @@ int CmdCommandAutoTuner( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: autotuner [-N num] [-C file] [-F file] [-vh]\n" );
Abc_Print( -2, "\t performs autotuning\n" );
Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controler [default = %d]\n", nCores );
Abc_Print( -2, "\t-N num : the number of concurrent jobs including the controller [default = %d]\n", nCores );
Abc_Print( -2, "\t-C cmd : configuration file with settings for autotuning\n" );
Abc_Print( -2, "\t-F cmd : list of AIGER files to be used for autotuning\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );

2
src/base/io/io.c
View File

@ -1192,7 +1192,7 @@ usage:
fprintf( pAbc->Err, "\t-x : toggles between bin and hex notation [default = %s]\n", fHex? "hex":"bin" );
fprintf( pAbc->Err, "\t-f : toggles reading truth table(s) from file [default = %s]\n", fFile? "yes": "no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\ttruth : truth table with most signficant bit first (e.g. 1000 for AND(a,b))\n" );
fprintf( pAbc->Err, "\ttruth : truth table with most significant bit first (e.g. 1000 for AND(a,b))\n" );
fprintf( pAbc->Err, "\tfile : file name with the truth table\n" );
return 1;
}

2
src/base/io/ioReadDsd.c
View File

@ -205,7 +205,7 @@ Abc_Obj_t * Io_ReadDsd_rec( Abc_Ntk_t * pNtk, char * pCur, char * pSop )
pEnd++;
if ( *pEnd != '(' )
{
printf( "Cannot find the end of hexidecimal truth table.\n" );
printf( "Cannot find the end of hexadecimal truth table.\n" );
return NULL;
}

2
src/base/io/ioUtil.c
View File

@ -390,7 +390,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
pNtkTemp = Abc_NtkToNetlist( pNtk );
else
{
fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" );
fprintf( stdout, "Latches are written into the PLA file at PI/PO pairs.\n" );
pNtkCopy = Abc_NtkDup( pNtk );
Abc_NtkMakeComb( pNtkCopy, 0 );
pNtkTemp = Abc_NtkToNetlist( pNtk );

2
src/bdd/cudd/cuddSubsetSP.c
View File

@ -1099,7 +1099,7 @@ CreatePathTable(
st__free_table(pathTable);
goto OUT_OF_MEM;
} else if (insertValue == 1) {
fprintf(fp, "Something wrong, the entry exists but didnt show up in st__lookup\n");
fprintf(fp, "Something wrong, the entry exists but didn't show up in st__lookup\n");
return(NULL);
}

4
src/map/if/ifTune.c
View File

@ -269,7 +269,7 @@ int Ifn_NtkParseInt_rec( char * pStr, Ifn_Ntk_t * p, char ** ppFinal, int * piNo
pFanins[nFanins++] = *piNode - 1;
}
else
return Ifn_ErrorMessage( "Substring \"%s\" contans unrecognized symbol \'%c\'.\n", pStr, pStr[0] );
return Ifn_ErrorMessage( "Substring \"%s\" contains unrecognized symbol \'%c\'.\n", pStr, pStr[0] );
}
assert( pStr == pLim );
pObj = p->Nodes + (*piNode)++;
@ -400,7 +400,7 @@ int Ifn_NtkParseInt2( char * pStr, Ifn_Ntk_t * p )
else if ( pStr[k+2] == '{' )
p->Nodes[i].Type = IFN_DSD_PRIME, Next = '}';
else
return Ifn_ErrorMessage( "Cannot find openning operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
return Ifn_ErrorMessage( "Cannot find opening operation symbol in the definition of signal \'%c\'.\n", 'a' + i );
for ( n = k + 3; pStr[n]; n++ )
if ( pStr[n] == Next )
break;

2
src/map/mpm/mpmMan.c
View File

@ -188,7 +188,7 @@ void Mpm_ManPrintStats( Mpm_Man_t * p )
Abc_Print( 1, "Runtime breakdown:\n" );
ABC_PRTP( "Complete cut computation ", p->timeDerive , p->timeTotal );
ABC_PRTP( "- Merging cuts ", p->timeMerge , p->timeTotal );
ABC_PRTP( "- Evaluting cut parameters ", p->timeEval , p->timeTotal );
ABC_PRTP( "- Evaluating cut parameters ", p->timeEval , p->timeTotal );
ABC_PRTP( "- Checking cut containment ", p->timeCompare, p->timeTotal );
ABC_PRTP( "- Adding cuts to storage ", p->timeStore , p->timeTotal );
ABC_PRTP( "Other ", p->timeOther , p->timeTotal );

4
src/map/scl/scl.c
View File

@ -1083,7 +1083,7 @@ int Scl_CommandBuffer( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !pPars->fSizeOnly && !pPars->fAddBufs && pNtk->vPhases == NULL )
{
Abc_Print( -1, "Fanin phase information is not avaiable.\n" );
Abc_Print( -1, "Fanin phase information is not available.\n" );
return 1;
}
if ( !pAbc->pLibScl || !Abc_SclHasDelayInfo(pAbc->pLibScl) )
@ -1219,7 +1219,7 @@ int Scl_CommandBufferOld( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( fAddInvs && pNtk->vPhases == NULL )
{
Abc_Print( -1, "Fanin phase information is not avaiable.\n" );
Abc_Print( -1, "Fanin phase information is not available.\n" );
return 1;
}
if ( !pAbc->pLibScl || !Abc_SclHasDelayInfo(pAbc->pLibScl) )

4
src/opt/dau/dauTree.c
View File

@ -1551,7 +1551,7 @@ int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned
Counter++;
if ( DAU_MAX_VAR < nKLutSize )
{
printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, nKLutSize );
printf( "Parameter DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, nKLutSize );
return -1;
}
assert( iDsd[0] <= iDsd[1] );
@ -1703,7 +1703,7 @@ int Mpm_FuncCompute( Dss_Man_t * p, int iDsd0, int iDsd1, Vec_Str_t * vShared, i
assert( iDsd0 <= iDsd1 );
if ( DAU_MAX_VAR < *pnLeaves )
{
printf( "Paramater DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, *pnLeaves );
printf( "Parameter DAU_MAX_VAR (%d) smaller than LUT size (%d).\n", DAU_MAX_VAR, *pnLeaves );
return -1;
}
if ( fVerbose )

6
src/opt/rwr/rwrExp.c
View File

@ -238,9 +238,9 @@ void Rwt_Man5ExplorePrint()
if ( CountMax < Counter )
CountMax = Counter;
}
printf( "Number of cuts considered = %8d.\n", nCuts );
printf( "Classes occurring at least once = %8d.\n", stmm_count(s_pManRwrExp5->tTableNN) );
printf( "The largest number of occurence = %8d.\n", CountMax );
printf( "Number of cuts considered = %8d.\n", nCuts );
printf( "Classes occurring at least once = %8d.\n", stmm_count(s_pManRwrExp5->tTableNN) );
printf( "The largest number of occurrence = %8d.\n", CountMax );
// print the distribution of classes
pDistrib = ABC_ALLOC( int, CountMax + 1 );

2
src/proof/abs/absGla.c
View File

@ -1539,7 +1539,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n",
pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
if ( pPars->fDumpVabs || pPars->fDumpMabs )
Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n",
Abc_Print( 1, "%s will be continuously dumped into file \"%s\".\n",
pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
if ( pPars->fDumpMabs )

2
src/proof/abs/absRpmOld.c
View File

@ -186,7 +186,7 @@ Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose )
Gia_ManStop( pTmp );
if ( fVerbose )
{
printf( "After FF-2-PI tranformation:\n" );
printf( "After FF-2-PI transformation:\n" );
Gia_ManPrintStats( pNew, NULL );
}
return pNew;

2
src/proof/acec/acecFadds.c
View File

@ -860,7 +860,7 @@ Gia_Man_t * Gia_ManDupWithNaturalBoxes( Gia_Man_t * p, int nFaddMin, int fVerbos
if ( Gia_ManRegNum(p) )
{
if ( fVerbose )
printf( "Warning: Sequential design is coverted into combinational one by adding white boxes.\n" );
printf( "Warning: Sequential design is converted into combinational one by adding white boxes.\n" );
pNew->nRegs = 0;
}
assert( !Gia_ManHasDangling(pNew) );

2
src/sat/bmc/bmcMulti.c
View File

@ -175,7 +175,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n",
pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
if ( pPars->fVerbose )
printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n",
printf( "Gap timeout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n",
pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose );
// create output map
vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs