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

Merge branch 'berkeley-abc:master' into master

This commit is contained in:
Cunxi Yu 2023-09-15 13:25:27 -07:00 committed by GitHub
parent 3488a35472 318d5cb54b
commit 1261f71248
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
56 changed files with 954 additions and 190 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
README.md
View File

@ -4,7 +4,19 @@
# ABC: System for Sequential Logic Synthesis and Formal Verification
ABC is always changing but the current snapshot is believed to be stable.
ABC is always changing but the current snapshot is believed to be stable.
## ABC fork with new features
Here is a [fork](https://github.com/yongshiwo/abc.git) of ABC containing Agdmap, a novel technology mapper for LUT-based FPGAs. Agdmap is based on a technology mapping algorithm with adaptive gate decomposition [1]. It is a cut enumeration based mapping algorithm with bin packing for simultaneous wide gate decomposition, which is a patent pending technology.
The mapper is developed and maintained by Longfei Fan and Prof. Chang Wu at Fudan University in Shanghai, China. The experimental results presented in [1] indicate that Agdmap can substantially improve area (by 10% or more) when compared against the best LUT mapping solutions in ABC, such as command "if".
The source code is provided for research and evaluation only. For commercial usage, please contact Prof. Chang Wu at wuchang@fudan.edu.cn.
References:
[1] L. Fan and C. Wu, "FPGA technology mapping with adaptive gate decompostion", ACM/SIGDA FPGA International Symposium on FPGAs, 2023.
## Compiling:

2
src/aig/gia/gia.h
View File

@ -1527,7 +1527,7 @@ extern void Gia_ManPrintStatsMiter( Gia_Man_t * p, int fVerbose )
extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
extern void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
extern void Gia_ManPrintNpnClasses( Gia_Man_t * p );
extern void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs );
extern void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter, int fInterComb );
/*=== giaMem.c ===========================================================*/
extern Gia_MmFixed_t * Gia_MmFixedStart( int nEntrySize, int nEntriesMax );
extern void Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose );

9
src/aig/gia/giaAiger.c
View File

@ -953,9 +953,12 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
}
}
pInit[i] = 0;
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, fGiaSimple, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
if ( !fSkipStrash )
{
pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, fGiaSimple, 1 );
pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
Gia_ManStop( pTemp );
}
ABC_FREE( pInit );
}
Vec_IntFreeP( &vInits );

1
src/aig/gia/giaCTas.c
View File

@ -1778,6 +1778,7 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
Tas_ManSatPrintStats( p );
Tas_ManStop( p );
Vec_PtrFree( vPres );
Vec_StrFree( vStatus );
}

135
src/aig/gia/giaDup.c
View File

@ -1604,6 +1604,47 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates while adding self-loops to the registers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupMiterCones( Gia_Man_t * p, Vec_Int_t * vPairs )
{
Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iLit0, iLit1;
pNew = Gia_ManStart( Gia_ManObjNum(p) + 3 * Vec_IntSize(vPairs) );
pNew->pName = Abc_UtilStrsav( "miter" );
Gia_ManHashAlloc( pNew );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntForEachEntryDouble( vPairs, iLit0, iLit1, i )
{
int Lit0 = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit0))->Value, Abc_LitIsCompl(iLit0) );
int Lit1 = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit1))->Value, Abc_LitIsCompl(iLit1) );
Vec_IntPush( vTemp, Gia_ManHashXor(pNew, Lit0, Lit1) );
}
Vec_IntForEachEntry( vTemp, iLit0, i )
Gia_ManAppendCo( pNew, iLit0 );
Vec_IntFree( vTemp );
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG in the DFS order.]
@ -5584,6 +5625,100 @@ void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla
Vec_IntFree( vRes );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 );
pNew->pName = Abc_UtilStrsav(p->pName);
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManAppendCo( pNew, 0 );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)+1 );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
{
Vec_Int_t * vLits;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iLit;
if ( Gia_ManBufNum(p1) == 0 ) {
printf( "The first AIG should have a boundary.\n" );
return NULL;
}
if ( Gia_ManBufNum(p2) != 0 ) {
printf( "The second AIG should have no boundary.\n" );
return NULL;
}
assert( Gia_ManBufNum(p1) > 0 );
assert( Gia_ManBufNum(p2) == 0 );
assert( Gia_ManRegNum(p1) == 0 );
assert( Gia_ManRegNum(p2) == 0 );
assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) );
assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) );
vLits = Vec_IntAlloc( Gia_ManBufNum(p1) );
if ( fVerbose )
printf( "Creating a boundary miter with %d inputs, %d outputs, and %d buffers.\n",
Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) );
pNew = Gia_ManStart( Gia_ManObjNum(p1) + Gia_ManObjNum(p2) );
pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 );
sprintf( pNew->pName, "%s_bmiter", p1->pName );
Gia_ManHashStart( pNew );
Gia_ManConst0(p1)->Value = 0;
Gia_ManConst0(p2)->Value = 0;
Gia_ManForEachCi( p1, pObj, i )
pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p2, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachAnd( p1, pObj, i ) {
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Gia_ObjIsBuf(pObj) )
Vec_IntPush( vLits, pObj->Value );
}
Gia_ManForEachCo( p2, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
//Gia_ManForEachCo( p1, pObj, i )
// Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntForEachEntry( vLits, iLit, i )
Gia_ManAppendCo( pNew, iLit );
Vec_IntFree( vLits );
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

7
src/aig/gia/giaKf.c
View File

@ -21,13 +21,18 @@
#include "gia.h"
#include "misc/vec/vecSet.h"
#ifdef _MSC_VER
#define unlink _unlink
#else
#include <unistd.h>
#endif
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#endif

304
src/aig/gia/giaMan.c
View File

@ -1241,6 +1241,89 @@ void Gia_ManDfsSlacksPrint( Gia_Man_t * p )
}
/**Function*************************************************************
Synopsis [Dump interface module]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManWriteNamesInter( FILE * pFile, char c, int n, int Start, int Skip, int nRegs )
{
int Length = Start, i, fFirst = 1;
char pName[100];
for ( i = 0; i < n-nRegs; i++ )
{
sprintf( pName, "%c[%d]", c, i );
Length += strlen(pName) + 2;
if ( Length > 60 )
{
fprintf( pFile, ",\n " );
Length = Skip;
fFirst = 1;
}
fprintf( pFile, "%s%s", fFirst ? "":", ", pName );
fFirst = 0;
}
for ( i = n-nRegs; i < n; i++ )
{
sprintf( pName, "%c%c[%d]", c, c, i );
Length += strlen(pName) + 2;
if ( Length > 60 )
{
fprintf( pFile, ",\n " );
Length = Skip;
fFirst = 1;
}
fprintf( pFile, "%s%s", fFirst ? "":", ", pName );
fFirst = 0;
}}
void Gia_ManDumpModuleName( FILE * pFile, char * pName )
{
int i;
for ( i = 0; i < (int)strlen(pName); i++ )
if ( isalpha(pName[i]) || isdigit(pName[i]) )
fprintf( pFile, "%c", pName[i] );
else
fprintf( pFile, "_" );
}
void Gia_ManDumpInterface2( Gia_Man_t * p, FILE * pFile )
{
int fPrintClk = 0;
fprintf( pFile, "module " );
Gia_ManDumpModuleName( pFile, p->pName );
fprintf( pFile, "_wrapper" );
fprintf( pFile, " (%s i, o );\n\n", fPrintClk && Gia_ManRegNum(p) ? " clk," : "" );
if ( fPrintClk && Gia_ManRegNum(p) )
fprintf( pFile, " input clk;\n" );
fprintf( pFile, " input [%d:0] i;\n", Gia_ManPiNum(p)-1 );
fprintf( pFile, " output [%d:0] o;\n\n", Gia_ManPoNum(p)-1 );
if ( Gia_ManRegNum(p) ) {
fprintf( pFile, " wire [%d:%d] ii;\n", Gia_ManCiNum(p)-1, Gia_ManPiNum(p) );
fprintf( pFile, " wire [%d:%d] oo;\n\n", Gia_ManCoNum(p)-1, Gia_ManPoNum(p) );
fprintf( pFile, " always @ (posedge %s)\n ii <= oo;\n\n", fPrintClk ? "clk" : "i[0]" );
}
fprintf( pFile, " " );
Gia_ManDumpModuleName( pFile, p->pName );
fprintf( pFile, " " );
Gia_ManDumpModuleName( pFile, p->pName );
fprintf( pFile, "_inst" );
fprintf( pFile, " (\n " );
Gia_ManWriteNamesInter( pFile, 'i', Gia_ManCiNum(p), 4, 4, Gia_ManRegNum(p) );
fprintf( pFile, ",\n " );
Gia_ManWriteNamesInter( pFile, 'o', Gia_ManCoNum(p), 4, 4, Gia_ManRegNum(p) );
fprintf( pFile, "\n );\n\n" );
fprintf( pFile, "endmodule\n\n" );
}
/**Function*************************************************************
Synopsis [Compute arrival/required times.]
@ -1323,38 +1406,40 @@ void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Sta
fFirst = 0;
}
}
void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs )
void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter, int fInterComb )
{
FILE * pFile;
Gia_Obj_t * pObj;
Vec_Bit_t * vInvs, * vUsed;
int nDigits = Abc_Base10Log( Gia_ManObjNum(p) );
int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) );
int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) );
int i, k, iObj;
if ( Gia_ManRegNum(p) )
int i, k, iObj, nRegs = Gia_ManRegNum(p);
if ( fInterComb )
{
printf( "Currently cannot write sequential AIG.\n" );
extern void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName );
Gia_ManDumpInterface( p, pFileName );
return;
}
pFile = fopen( pFileName, "wb" );
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open output file \"%s\".\n", pFileName );
return;
}
if ( fInter || nRegs )
Gia_ManDumpInterface2( p, pFile );
//Gia_ManSetRegNum( p, 0 );
p->nRegs = 0;
vInvs = Gia_ManGenUsed( p, 0 );
vUsed = Gia_ManGenUsed( p, 1 );
//fprintf( pFile, "// This Verilog file is written by ABC on %s\n\n", Extra_TimeStamp() );
fprintf( pFile, "module " );
for ( i = 0; i < (int)strlen(p->pName); i++ )
if ( isalpha(p->pName[i]) || isdigit(p->pName[i]) )
fprintf( pFile, "%c", p->pName[i] );
else
fprintf( pFile, "_" );
Gia_ManDumpModuleName( pFile, p->pName );
if ( fVerBufs )
{
@ -1505,6 +1590,203 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int
Vec_BitFree( vInvs );
Vec_BitFree( vUsed );
Gia_ManSetRegNum( p, nRegs );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName )
{
Gia_Obj_t * pObj;
Vec_Bit_t * vInvs, * vUsed;
int nDigits = Abc_Base10Log( Gia_ManObjNum(p) );
int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) );
int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) );
int i;
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open output file \"%s\".\n", pFileName );
return;
}
vInvs = Gia_ManGenUsed( p, 0 );
vUsed = Gia_ManGenUsed( p, 1 );
fprintf( pFile, "module " );
Gia_ManDumpModuleName( pFile, p->pName );
fprintf( pFile, "_wrapper" );
fprintf( pFile, " ( _i_, _o_ );\n\n" );
fprintf( pFile, " input [%d:0] _i_;\n", Gia_ManCiNum(p)-1 );
fprintf( pFile, " output [%d:0] _o_;\n\n", Gia_ManCoNum(p)-1 );
fprintf( pFile, " wire " );
Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
fprintf( pFile, ";\n\n" );
fprintf( pFile, " wire " );
Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
fprintf( pFile, ";\n\n" );
fprintf( pFile, " assign { " );
Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL );
fprintf( pFile, " } = _i_;\n\n" );
fprintf( pFile, " assign _o_ = { " );
Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL );
fprintf( pFile, " };\n\n" );
if ( Vec_BitCount(vUsed) )
{
fprintf( pFile, " wire " );
Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed );
fprintf( pFile, ";\n\n" );
}
if ( Vec_BitCount(vInvs) )
{
fprintf( pFile, " wire " );
Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs );
fprintf( pFile, ";\n\n" );
}
// input inverters
Gia_ManForEachCi( p, pObj, i )
{
if ( Vec_BitEntry(vUsed, Gia_ObjId(p, pObj)) )
{
fprintf( pFile, " buf ( %s,", Gia_ObjGetDumpName(NULL, 'n', Gia_ObjId(p, pObj), nDigits) );
fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
}
if ( Vec_BitEntry(vInvs, Gia_ObjId(p, pObj)) )
{
fprintf( pFile, " not ( %s,", Gia_ObjGetDumpName(NULL, 'i', Gia_ObjId(p, pObj), nDigits) );
fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
}
}
// internal nodes and their inverters
fprintf( pFile, "\n" );
Gia_ManForEachAnd( p, pObj, i )
{
fprintf( pFile, " and ( %s,", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
fprintf( pFile, " %s,", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) );
fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) );
if ( Vec_BitEntry(vInvs, i) )
{
fprintf( pFile, " not ( %s,", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) );
fprintf( pFile, " %s );\n", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
}
}
// output drivers
fprintf( pFile, "\n" );
Gia_ManForEachCo( p, pObj, i )
{
fprintf( pFile, " buf ( %s, ", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) );
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
fprintf( pFile, "1\'b%d );\n", Gia_ObjFaninC0(pObj) );
else
fprintf( pFile, "%s );\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0p(p, pObj), nDigits) );
}
fprintf( pFile, "\nendmodule\n\n" );
fclose( pFile );
Vec_BitFree( vInvs );
Vec_BitFree( vUsed );
}
/**Function*************************************************************
Synopsis [Generate hierarchical design.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_FreeMany( Gia_Man_t ** pGias, int nGias )
{
int i;
for ( i = 0; i < nGias; i++ )
Gia_ManStopP( &pGias[i] );
}
void Gia_GenSandwich( char ** pFNames, int nFNames )
{
FILE * pFile = NULL;
char * pFileName = (char *)"sandwich.v";
Gia_Man_t * pGias[16] = {0};
int i, k;
assert( nFNames <= 16 );
for ( i = 0; i < nFNames; i++ )
{
FILE * pFile = fopen( pFNames[i], "rb" );
if ( pFile == NULL ) {
printf( "Cannot open input file \"%s\".\n", pFNames[i] );
Gia_FreeMany( pGias, nFNames );
return;
}
fclose( pFile );
pGias[i] = Gia_AigerRead( pFNames[i], 0, 0, 0 );
if ( pGias[i] == NULL ) {
printf( "Failed to read an AIG from file \"%s\".\n", pFNames[i] );
Gia_FreeMany( pGias, nFNames );
return;
}
}
for ( i = 0; i < nFNames-1; i++ )
if ( Gia_ManPoNum(pGias[i]) < Gia_ManPiNum(pGias[i+1]) ) {
printf( "AIG in file \"%s\" has fewer outputs than inputs of AIG in file \"%s\".\n", pFNames[i], pFNames[i+1] );
Gia_FreeMany( pGias, nFNames );
return;
}
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open output file \"%s\".\n", pFileName );
Gia_FreeMany( pGias, nFNames );
return;
}
fprintf( pFile, "\n" );
for ( i = 0; i < nFNames; i++ )
fprintf( pFile, "`include \"%s\"\n", Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v") );
fprintf( pFile, "\n" );
fprintf( pFile, "module sandwich ( in, out );\n" );
fprintf( pFile, " input [%3d:0] in;\n", Gia_ManPiNum(pGias[0])-1 );
fprintf( pFile, " output [%3d:0] out;\n", Gia_ManPoNum(pGias[nFNames-1])-1 );
fprintf( pFile, " wire [%3d:0] tmp0 = in;\n", Gia_ManPiNum(pGias[0])-1 );
for ( i = 0; i < nFNames; i++ ) {
fprintf( pFile, " wire [%3d:0] tmp%d; ", Gia_ManPoNum(pGias[i])-1, i+1 );
Gia_ManDumpModuleName( pFile, pGias[i]->pName );
fprintf( pFile, "_wrapper" );
for ( k = strlen(pGias[i]->pName); k < 24; k++ )
fprintf( pFile, " " );
fprintf( pFile, " i%d ( tmp%d, tmp%d );\n", i+1, i, i+1 );
}
fprintf( pFile, " assign out = tmp%d;\n", nFNames );
fprintf( pFile, "endmodule\n" );
fclose( pFile );
for ( i = 0; i < nFNames; i++ ) {
Gia_ManDumpVerilog( pGias[i], Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v"), NULL, 0, 0, 1 );
printf( "Dumped Verilog file \"%s\"\n", Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v") );
}
Gia_FreeMany( pGias, nFNames );
printf( "Dumped hierarchical design into file \"%s\"\n", pFileName );
}
////////////////////////////////////////////////////////////////////////

6
src/aig/gia/giaStoch.c
View File

@ -22,6 +22,11 @@
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#ifdef _MSC_VER
#define unlink _unlink
#else
#include <unistd.h>
#endif
#ifdef ABC_USE_PTHREADS
@ -29,7 +34,6 @@
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#endif

7
src/aig/gia/giaTranStoch.c
View File

@ -29,13 +29,18 @@
#include <opt/sfm/sfm.h>
#include <opt/fxu/fxu.h>
#ifdef _MSC_VER
#define unlink _unlink
#else
#include <unistd.h>
#endif
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#endif

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/aig/saig/saigTrans.c
View File

@ -6,7 +6,7 @@
PackageName [Sequential AIG package.]
Synopsis [Dynamic simplication of the transition relation.]
Synopsis [Dynamic simplification of the transition relation.]
Author [Alan Mishchenko]

3
src/base/abc/abcAig.c
View File

@ -860,7 +860,8 @@ int Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fU
pOld = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceOld );
pNew = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceNew );
if ( Abc_ObjFanoutNum(pOld) == 0 )
return 0;
//return 0;
continue;
Abc_AigReplace_int( pMan, pOld, pNew, fUpdateLevel );
}
if ( fUpdateLevel )

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

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

@ -922,6 +922,8 @@ int Abc_SopCheckReadTruth( Vec_Ptr_t * vRes, char * pToken, int fHex )
{
char * pBase; int nVars;
int Log2 = Abc_Base2Log( strlen(pToken) );
if ( fHex && strlen(pToken) == 1 )
Log2 = 0;
if ( (1 << Log2) != (int)strlen(pToken) )
{
printf( "The truth table length (%d) is not power-of-2.\n", (int)strlen(pToken) );

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

@ -594,6 +594,9 @@ static int Abc_CommandAbc9Gla2Fla ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Gen ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ProdAdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -775,7 +778,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 )
@ -1362,6 +1365,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&gen", Abc_CommandAbc9Gen, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cfs", Abc_CommandAbc9Cfs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&prodadd", Abc_CommandAbc9ProdAdd, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
{
@ -7003,7 +7009,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" );
@ -13708,7 +13714,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" );
@ -17981,7 +17987,7 @@ int Abc_CommandRecPs3( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkRecIsRunning3() )
{
Abc_Print( -1, "This command works for AIGs only after calling \"rec_start2\".\n" );
Abc_Print( -1, "This command works for AIGs only after calling \"rec_start3\".\n" );
return 0;
}
Abc_NtkRecPs3(fPrintLib);
@ -18033,7 +18039,7 @@ int Abc_CommandRecAdd3( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkRecIsRunning3() )
{
Abc_Print( -1, "This command works for AIGs after calling \"rec_start2\".\n" );
Abc_Print( -1, "This command works for AIGs after calling \"rec_start3\".\n" );
return 0;
}
Abc_NtkRecAdd3( pNtk, fUseSOPB );
@ -20306,7 +20312,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" );
@ -26345,7 +26351,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 );
@ -27699,7 +27705,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 );
@ -29233,7 +29239,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");
}
@ -29259,7 +29265,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");
@ -29647,7 +29653,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" );
@ -31924,13 +31930,15 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew;
int fUnique = 0;
int fVerilog = 0;
int fInter = 0;
int fInterComb = 0;
int fVerBufs = 0;
int fMiniAig = 0;
int fMiniLut = 0;
int fWriteNewLine = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "upbmlnvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "upicbmlnvh" ) ) != EOF )
{
switch ( c )
{
@ -31940,6 +31948,12 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
fVerilog ^= 1;
break;
case 'i':
fInter ^= 1;
break;
case 'c':
fInterComb ^= 1;
break;
case 'b':
fVerBufs ^= 1;
break;
@ -31981,7 +31995,7 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManStop( pGia );
}
else if ( fVerilog )
Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs );
Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs, fInter, fInterComb );
else if ( fMiniAig )
Gia_ManWriteMiniAig( pAbc->pGia, pFileName );
else if ( fMiniLut )
@ -31991,10 +32005,12 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &w [-upbmlnvh] <file>\n" );
Abc_Print( -2, "usage: &w [-upicbmlnvh] <file>\n" );
Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" );
Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
Abc_Print( -2, "\t-p : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" );
Abc_Print( -2, "\t-i : toggle writing the interface module in Verilog [default = %s]\n", fInter? "yes" : "no" );
Abc_Print( -2, "\t-c : toggle writing the interface module in Verilog [default = %s]\n", fInterComb? "yes" : "no" );
Abc_Print( -2, "\t-b : toggle writing additional buffers in Verilog [default = %s]\n", fVerBufs? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
@ -34974,7 +34990,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;
@ -35425,7 +35441,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;
@ -46132,7 +46148,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" );
@ -51605,6 +51621,173 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9AddFlop( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p );
Gia_Man_t * pTemp;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AddFlop(): There is no AIG.\n" );
return 0;
}
pTemp = Gia_ManDupAddFlop( pAbc->pGia );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &addflop [-vh]\n" );
Abc_Print( -2, "\t adds one flop to the design\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
Gia_Man_t * pTemp, * pSecond;
char * FileName = NULL;
FILE * pFile = NULL;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9BMiter(): There is no AIG.\n" );
return 0;
}
if ( argc != globalUtilOptind + 1 )
{
Abc_Print( -1, "Abc_CommandAbc9BMiter(): AIG should be given on the command line.\n" );
return 0;
}
// get the input file name
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9BMiter(): Cannot read the file name on the command line.\n" );
return 0;
}
pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose );
Gia_ManStop( pSecond );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &bmiter [-vh] <file>\n" );
Abc_Print( -2, "\t creates the boundary miter\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the implementation file\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GenHie( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_GenSandwich( char ** pFNames, int nFNames );
int c, fVerbose = 0;
char ** pArgvNew;
int nArgcNew;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
Gia_GenSandwich( pArgvNew, nArgcNew );
return 0;
usage:
Abc_Print( -2, "usage: &gen_hie [-vh] <file[1]> <file[2]> ... <file[N]>\n" );
Abc_Print( -2, "\t generates a hierarchical design\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<files> : the AIG files for the instance modules\n");
Abc_Print( -2, "\t (the PO count of <file[i]> should not be less than the PI count of <file[i+1]>)\n");
return 1;}
/**Function*************************************************************

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*************************************************************

1
src/base/abci/abcLutmin.c
View File

@ -112,6 +112,7 @@ void Abc_NtkCheckAbsorb( Abc_Ntk_t * pNtk, int nLutSize )
Counter, 100.0 * Counter / Abc_NtkNodeNum(pNtk),
Counter2, 100.0 * Counter2 / Abc_NtkNodeNum(pNtk) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Vec_IntFree( vCounts );
}
/**Function*************************************************************

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

@ -2483,6 +2483,8 @@ saucy_search(
/* Keep running till we're out of automorphisms */
while (do_search(s));
ABC_FREE(g);
}
void

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

@ -652,7 +652,7 @@ void Abc_NtkTimePrint( Abc_Ntk_t * pNtk )
/**Function*************************************************************
Synopsis [Expends the storage for timing information.]
Synopsis [Expands the storage for timing information.]
Description []

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" );

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

@ -102,7 +102,7 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command )
***********************************************************************/
void Cmd_HistoryRead( Abc_Frame_t * p )
{
#if defined(WIN32) && defined(ABC_USE_HISTORY)
#if defined(ABC_USE_HISTORY)
char Buffer[ABC_MAX_STR];
FILE * pFile;
assert( Vec_PtrSize(p->aHistory) == 0 );
@ -133,7 +133,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p )
***********************************************************************/
void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
{
#if defined(WIN32) && defined(ABC_USE_HISTORY)
#if defined(ABC_USE_HISTORY)
FILE * pFile;
char * pStr;
int i;
@ -163,7 +163,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
***********************************************************************/
void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit )
{
#if defined(WIN32) && defined(ABC_USE_HISTORY)
#if defined(ABC_USE_HISTORY)
char * pStr;
int i;
Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );

2
src/base/exor/exorUtil.c
View File

@ -189,7 +189,7 @@ int WriteResultIntoFile( char * pFileName )
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( pFile, "\n\nCannot open the output file\n" );
fprintf( stderr, "\n\nCannot open the output file\n" );
return 1;
}

4
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;
}
@ -1542,7 +1542,7 @@ int IoCommandWrite( Abc_Frame_t * pAbc, int argc, char **argv )
if ( !strcmp( Extra_FileNameExtension(pFileName), "genlib" ) )
sprintf( Command, "write_genlib %s", pFileName );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "lib" ) )
sprintf( Command, "write_liberty %s", pFileName );
sprintf( Command, "write_lib %s", pFileName );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) )
sprintf( Command, "dsd_save %s", pFileName );
if ( Command[0] )

10
src/base/io/ioReadBlifMv.c
View File

@ -548,10 +548,10 @@ typedef struct buflist {
struct buflist * next;
} buflist;
char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize )
char * Io_MvLoadFileBz2( char * pFileName, long * pnFileSize )
{
FILE * pFile;
int nFileSize = 0;
long nFileSize = 0;
char * pContents;
BZFILE * b;
int bzError, RetValue;
@ -628,12 +628,12 @@ char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize )
SeeAlso []
***********************************************************************/
static char * Io_MvLoadFileGz( char * pFileName, int * pnFileSize )
static char * Io_MvLoadFileGz( char * pFileName, long * pnFileSize )
{
const int READ_BLOCK_SIZE = 100000;
gzFile pFile;
char * pContents;
int amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
pContents = ABC_ALLOC( char, nFileSize );
readBlock = 0;
@ -665,7 +665,7 @@ static char * Io_MvLoadFileGz( char * pFileName, int * pnFileSize )
static char * Io_MvLoadFile( char * pFileName )
{
FILE * pFile;
int nFileSize;
long nFileSize;
char * pContents;
int RetValue;
if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )

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;
}

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

@ -157,8 +157,10 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck
fprintf( stdout, "Reading network from file has failed.\n" );
return NULL;
}
if ( fCheck && (Abc_NtkBlackboxNum(pNtk) || Abc_NtkWhiteboxNum(pNtk)) )
if ( fCheck && (Abc_NtkBlackboxNum(pNtk) || Abc_NtkWhiteboxNum(pNtk)) && pNtk->pDesign )
{
int i, fCycle = 0;
Abc_Ntk_t * pModel;
// fprintf( stdout, "Warning: The network contains hierarchy.\n" );
@ -390,7 +392,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/base/wln/wlnCom.c
View File

@ -206,7 +206,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: %%yosys [-T <module>] [-D <defines>] [-bismcvh] <file_name>\n" );
Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" );
Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\"\n" );
Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" );
Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" );
Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" );
Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );

1
src/base/wln/wlnRead.c
View File

@ -2748,6 +2748,7 @@ Gia_Man_t * Gia_ManDupPermIO( Gia_Man_t * p, Vec_Int_t * vPermI, Vec_Int_t * vPe
assert( Vec_IntSize(vPermI) == Gia_ManCiNum(p) );
assert( Vec_IntSize(vPermO) == Gia_ManCoNum(p) );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav(p->pName);
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
Gia_ManCi(p, Vec_IntEntry(vPermI, i))->Value = Gia_ManAppendCi(pNew);

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 );

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

@ -130,7 +130,36 @@ void Scl_End( Abc_Frame_t * pAbc )
Scl_ConUpdateMan( pAbc, NULL );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
SC_Lib * Scl_ReadLibraryFile( Abc_Frame_t * pAbc, char * pFileName, int fVerbose, int fVeryVerbose, SC_DontUse dont_use )
{
SC_Lib * pLib;
FILE * pFile;
if ( (pFile = fopen( pFileName, "rb" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
return NULL;
}
fclose( pFile );
// read new library
pLib = Abc_SclReadLiberty( pFileName, fVerbose, fVeryVerbose, dont_use);
if ( pLib == NULL )
{
fprintf( pAbc->Err, "Reading SCL library from file \"%s\" has failed. \n", pFileName );
return NULL;
}
return pLib;
}
/**Function*************************************************************
@ -145,8 +174,6 @@ void Scl_End( Abc_Frame_t * pAbc )
***********************************************************************/
int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char * pFileName;
FILE * pFile;
SC_Lib * pLib;
int c, fDump = 0;
float Slew = 0;
@ -230,25 +257,29 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the input file name
pFileName = argv[globalUtilOptind];
if ( (pFile = fopen( pFileName, "rb" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
if ( argc == globalUtilOptind + 2 ) { // expecting two files
SC_Lib * pLib1 = Scl_ReadLibraryFile( pAbc, argv[globalUtilOptind], fVerbose, fVeryVerbose, dont_use );
SC_Lib * pLib2 = Scl_ReadLibraryFile( pAbc, argv[globalUtilOptind+1], fVerbose, fVeryVerbose, dont_use );
ABC_FREE(dont_use.dont_use_list);
return 1;
if ( pLib1 == NULL || pLib2 == NULL ) {
if (pLib1) Abc_SclLibFree(pLib1);
if (pLib2) Abc_SclLibFree(pLib2);
return 1;
}
pLib = Abc_SclMergeLibraries( pLib1, pLib2 );
Abc_SclLibFree(pLib1);
Abc_SclLibFree(pLib2);
}
fclose( pFile );
// read new library
pLib = Abc_SclReadLiberty( pFileName, fVerbose, fVeryVerbose, dont_use);
ABC_FREE(dont_use.dont_use_list);
if ( pLib == NULL )
{
fprintf( pAbc->Err, "Reading SCL library from file \"%s\" has failed. \n", pFileName );
return 1;
else if ( argc == globalUtilOptind + 1 ) { // expecting one file
pLib = Scl_ReadLibraryFile( pAbc, argv[globalUtilOptind], fVerbose, fVeryVerbose, dont_use );
ABC_FREE(dont_use.dont_use_list);
}
else {
ABC_FREE(dont_use.dont_use_list);
goto usage;
}
if ( pLib == NULL )
return 1;
if ( Abc_SclLibClassNum(pLib) < 3 )
{
fprintf( pAbc->Err, "Library with only %d cell classes cannot be used.\n", Abc_SclLibClassNum(pLib) );
@ -261,7 +292,7 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_SclShortNames( pLib );
// dump the resulting library
if ( fDump && pAbc->pLibScl )
Abc_SclWriteLiberty( Extra_FileNameGenericAppend(pFileName, "_temp.lib"), (SC_Lib *)pAbc->pLibScl );
Abc_SclWriteLiberty( Extra_FileNameGenericAppend(argv[globalUtilOptind], "_temp.lib"), (SC_Lib *)pAbc->pLibScl );
if ( fUnit )
{
SC_Cell * pCell; int i;
@ -277,7 +308,7 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: read_lib [-SG float] [-M num] [-dnuvwh] [-X cell_name] <file>\n" );
fprintf( pAbc->Err, "usage: read_lib [-SG float] [-M num] [-dnuvwh] [-X cell_name] <file> <file2>\n" );
fprintf( pAbc->Err, "\t reads Liberty library from file\n" );
fprintf( pAbc->Err, "\t-S float : the slew parameter used to generate the library [default = %.2f]\n", Slew );
fprintf( pAbc->Err, "\t-G float : the gain parameter used to generate the library [default = %.2f]\n", Gain );
@ -290,6 +321,7 @@ usage:
fprintf( pAbc->Err, "\t-w : toggle writing information about skipped gates [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\t<file> : the name of a file to read\n" );
fprintf( pAbc->Err, "\t<file2> : the name of a file to read (optional)\n" );
return 1;
}
@ -1083,7 +1115,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) )
@ -1104,9 +1136,9 @@ int Scl_CommandBuffer( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pAbc->Err, "usage: buffer [-GSN num] [-sbpcvwh]\n" );
fprintf( pAbc->Err, "\t performs buffering and sizing and mapped network\n" );
fprintf( pAbc->Err, "\t performs buffering and sizing on mapped network\n" );
fprintf( pAbc->Err, "\t-G <num> : target gain percentage [default = %d]\n", pPars->GainRatio );
fprintf( pAbc->Err, "\t-S <num> : target slew in pisoseconds [default = %d]\n", pPars->Slew );
fprintf( pAbc->Err, "\t-S <num> : target slew in picoseconds [default = %d]\n", pPars->Slew );
fprintf( pAbc->Err, "\t-N <num> : the maximum fanout count [default = %d]\n", pPars->nDegree );
fprintf( pAbc->Err, "\t-s : toggle performing only sizing [default = %s]\n", pPars->fSizeOnly? "yes": "no" );
fprintf( pAbc->Err, "\t-b : toggle using buffers instead of inverters [default = %s]\n", pPars->fAddBufs? "yes": "no" );
@ -1219,7 +1251,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) )
@ -1755,9 +1787,9 @@ int Scl_CommandDnsize( Abc_Frame_t * pAbc, int argc, char **argv )
usage:
fprintf( pAbc->Err, "usage: dnsize [-IJNDGTX num] [-csdvwh]\n" );
fprintf( pAbc->Err, "\t selectively decreases gate sizes while maintaining delay\n" );
fprintf( pAbc->Err, "\t-I <num> : the number of upsizing iterations to perform [default = %d]\n", pPars->nIters );
fprintf( pAbc->Err, "\t-I <num> : the number of downsizing iterations to perform [default = %d]\n", pPars->nIters );
fprintf( pAbc->Err, "\t-J <num> : the number of iterations without improvement to stop [default = %d]\n", pPars->nIterNoChange );
fprintf( pAbc->Err, "\t-N <num> : limit on discrete upsizing steps at a node [default = %d]\n", pPars->Notches );
fprintf( pAbc->Err, "\t-N <num> : limit on discrete downsizing steps at a node [default = %d]\n", pPars->Notches );
fprintf( pAbc->Err, "\t-D <num> : delay target set by the user, in picoseconds [default = %d]\n", pPars->DelayUser );
fprintf( pAbc->Err, "\t-G <num> : delay gap during updating, in picoseconds [default = %d]\n", pPars->DelayGap );
fprintf( pAbc->Err, "\t-T <num> : approximate timeout in seconds [default = %d]\n", pPars->TimeOut );

2
src/map/scl/sclDnsize.c
View File

@ -265,7 +265,7 @@ void Abc_SclDnsizePerformInt( SC_Lib * pLib, Abc_Ntk_t * pNtk, SC_SizePars * pPa
assert( p->vGatesBest == NULL );
p->vGatesBest = Vec_IntDup( p->pNtk->vGates );
// perform upsizing
// perform downsizing
vNodes = Vec_IntAlloc( 1000 );
vEvals = Vec_IntAlloc( 1000 );
vTryLater = Vec_IntAlloc( 1000 );

1
src/map/scl/sclLib.h
View File

@ -748,6 +748,7 @@ extern SC_Lib * Abc_SclReadFromStr( Vec_Str_t * vOut );
extern SC_Lib * Abc_SclReadFromFile( char * pFileName );
extern void Abc_SclWriteScl( char * pFileName, SC_Lib * p );
extern void Abc_SclWriteLiberty( char * pFileName, SC_Lib * p );
extern SC_Lib * Abc_SclMergeLibraries( SC_Lib * pLib1, SC_Lib * pLib2 );
/*=== sclLibUtil.c ===============================================================*/
extern void Abc_SclHashCells( SC_Lib * p );
extern int Abc_SclCellFind( SC_Lib * p, char * pName );

160
src/map/scl/sclLibScl.c
View File

@ -483,71 +483,22 @@ static void Abc_SclWriteSurface( Vec_Str_t * vOut, SC_Surface * p )
for ( i = 0; i < 6; i++ )
Vec_StrPutF( vOut, p->approx[2][i] );
}
static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p )
static void Abc_SclWriteLibraryCellsOnly( Vec_Str_t * vOut, SC_Lib * p, int fAddOn )
{
SC_WireLoad * pWL;
SC_WireLoadSel * pWLS;
SC_Cell * pCell;
SC_Pin * pPin;
int n_valid_cells;
int i, j, k;
Vec_StrPutI( vOut, ABC_SCL_CUR_VERSION );
// Write non-composite fields:
Vec_StrPutS( vOut, p->pName );
Vec_StrPutS( vOut, p->default_wire_load );
Vec_StrPutS( vOut, p->default_wire_load_sel );
Vec_StrPutF( vOut, p->default_max_out_slew );
assert( p->unit_time >= 0 );
assert( p->unit_cap_snd >= 0 );
Vec_StrPutI( vOut, p->unit_time );
Vec_StrPutF( vOut, p->unit_cap_fst );
Vec_StrPutI( vOut, p->unit_cap_snd );
// Write 'wire_load' vector:
Vec_StrPutI( vOut, Vec_PtrSize(&p->vWireLoads) );
SC_LibForEachWireLoad( p, pWL, i )
{
Vec_StrPutS( vOut, pWL->pName );
Vec_StrPutF( vOut, pWL->cap );
Vec_StrPutF( vOut, pWL->slope );
Vec_StrPutI( vOut, Vec_IntSize(&pWL->vFanout) );
for ( j = 0; j < Vec_IntSize(&pWL->vFanout); j++ )
{
Vec_StrPutI( vOut, Vec_IntEntry(&pWL->vFanout, j) );
Vec_StrPutF( vOut, Vec_FltEntry(&pWL->vLen, j) );
}
}
// Write 'wire_load_sel' vector:
Vec_StrPutI( vOut, Vec_PtrSize(&p->vWireLoadSels) );
SC_LibForEachWireLoadSel( p, pWLS, i )
{
Vec_StrPutS( vOut, pWLS->pName );
Vec_StrPutI( vOut, Vec_FltSize(&pWLS->vAreaFrom) );
for ( j = 0; j < Vec_FltSize(&pWLS->vAreaFrom); j++)
{
Vec_StrPutF( vOut, Vec_FltEntry(&pWLS->vAreaFrom, j) );
Vec_StrPutF( vOut, Vec_FltEntry(&pWLS->vAreaTo, j) );
Vec_StrPutS( vOut, (char *)Vec_PtrEntry(&pWLS->vWireLoadModel, j) );
}
}
// Write 'cells' vector:
n_valid_cells = 0;
SC_LibForEachCell( p, pCell, i )
if ( !(pCell->seq || pCell->unsupp) )
n_valid_cells++;
Vec_StrPutI( vOut, n_valid_cells );
int i, j, k;
SC_LibForEachCell( p, pCell, i )
{
if ( pCell->seq || pCell->unsupp )
continue;
if ( fAddOn ) {
Vec_StrPush( vOut, 'L' );
Vec_StrPush( vOut, '0'+(char)fAddOn );
Vec_StrPush( vOut, '_' );
}
Vec_StrPutS( vOut, pCell->pName );
Vec_StrPutF( vOut, pCell->area );
Vec_StrPutF( vOut, pCell->leakage );
@ -608,13 +559,78 @@ static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p )
assert( Vec_PtrSize(&pRTime->vTimings) == 0 );
}
}
}
}
int Abc_SclCountValidCells( SC_Lib * p )
{
SC_Cell * pCell;
int i, n_valid_cells = 0;
SC_LibForEachCell( p, pCell, i )
if ( !(pCell->seq || pCell->unsupp) )
n_valid_cells++;
return n_valid_cells;
}
static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p, int nExtra )
{
SC_WireLoad * pWL;
SC_WireLoadSel * pWLS;
int n_valid_cells;
int i, j;
Vec_StrPutI( vOut, ABC_SCL_CUR_VERSION );
// Write non-composite fields:
Vec_StrPutS( vOut, p->pName );
Vec_StrPutS( vOut, p->default_wire_load );
Vec_StrPutS( vOut, p->default_wire_load_sel );
Vec_StrPutF( vOut, p->default_max_out_slew );
assert( p->unit_time >= 0 );
assert( p->unit_cap_snd >= 0 );
Vec_StrPutI( vOut, p->unit_time );
Vec_StrPutF( vOut, p->unit_cap_fst );
Vec_StrPutI( vOut, p->unit_cap_snd );
// Write 'wire_load' vector:
Vec_StrPutI( vOut, Vec_PtrSize(&p->vWireLoads) );
SC_LibForEachWireLoad( p, pWL, i )
{
Vec_StrPutS( vOut, pWL->pName );
Vec_StrPutF( vOut, pWL->cap );
Vec_StrPutF( vOut, pWL->slope );
Vec_StrPutI( vOut, Vec_IntSize(&pWL->vFanout) );
for ( j = 0; j < Vec_IntSize(&pWL->vFanout); j++ )
{
Vec_StrPutI( vOut, Vec_IntEntry(&pWL->vFanout, j) );
Vec_StrPutF( vOut, Vec_FltEntry(&pWL->vLen, j) );
}
}
// Write 'wire_load_sel' vector:
Vec_StrPutI( vOut, Vec_PtrSize(&p->vWireLoadSels) );
SC_LibForEachWireLoadSel( p, pWLS, i )
{
Vec_StrPutS( vOut, pWLS->pName );
Vec_StrPutI( vOut, Vec_FltSize(&pWLS->vAreaFrom) );
for ( j = 0; j < Vec_FltSize(&pWLS->vAreaFrom); j++)
{
Vec_StrPutF( vOut, Vec_FltEntry(&pWLS->vAreaFrom, j) );
Vec_StrPutF( vOut, Vec_FltEntry(&pWLS->vAreaTo, j) );
Vec_StrPutS( vOut, (char *)Vec_PtrEntry(&pWLS->vWireLoadModel, j) );
}
}
// Write 'cells' vector:
n_valid_cells = Abc_SclCountValidCells( p );
Vec_StrPutI( vOut, n_valid_cells + nExtra );
Abc_SclWriteLibraryCellsOnly( vOut, p, (int)(nExtra > 0) );
}
void Abc_SclWriteScl( char * pFileName, SC_Lib * p )
{
Vec_Str_t * vOut;
vOut = Vec_StrAlloc( 10000 );
Abc_SclWriteLibrary( vOut, p );
Abc_SclWriteLibrary( vOut, p, 0 );
if ( Vec_StrSize(vOut) > 0 )
{
FILE * pFile = fopen( pFileName, "wb" );
@ -835,10 +851,36 @@ void Abc_SclWriteLiberty( char * pFileName, SC_Lib * p )
{
Abc_SclWriteLibraryText( pFile, p );
fclose( pFile );
printf( "Dumped internal library into Liberty file \"%s\".\n", pFileName );
printf( "Dumped internal library with %d cells into Liberty file \"%s\".\n", SC_LibCellNum(p), pFileName );
}
}
/**Function*************************************************************
Synopsis [Appends cells of pLib2 to those of pLib1.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
SC_Lib * Abc_SclMergeLibraries( SC_Lib * pLib1, SC_Lib * pLib2 )
{
Vec_Str_t * vOut = Vec_StrAlloc( 10000 );
int n_valid_cells2 = Abc_SclCountValidCells( pLib2 );
Abc_SclWriteLibrary( vOut, pLib1, n_valid_cells2 );
Abc_SclWriteLibraryCellsOnly( vOut, pLib2, 2 );
SC_Lib * p = Abc_SclReadFromStr( vOut );
p->pFileName = Abc_UtilStrsav( pLib1->pFileName );
p->pName = ABC_ALLOC( char, strlen(pLib1->pName) + strlen(pLib2->pName) + 10 );
sprintf( p->pName, "%s__and__%s", pLib1->pName, pLib2->pName );
Vec_StrFree( vOut );
printf( "Updated library \"%s\" with additional %d cells from library \"%s\".\n", pLib1->pName, n_valid_cells2, pLib2->pName );
return p;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

14
src/map/scl/sclLiberty.c
View File

@ -70,7 +70,7 @@ struct Scl_Tree_t_
{
char * pFileName; // input Liberty file name
char * pContents; // file contents
int nContents; // file size
long nContents; // file size
int nLines; // line counter
int nItems; // number of items
int nItermAlloc; // number of items allocated
@ -521,10 +521,10 @@ void Scl_LibertyFixFileName( char * pFileName )
if ( *pHead == '>' )
*pHead = '\\';
}
int Scl_LibertyFileSize( char * pFileName )
long Scl_LibertyFileSize( char * pFileName )
{
FILE * pFile;
int nFileSize;
long nFileSize;
pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
{
@ -536,7 +536,7 @@ int Scl_LibertyFileSize( char * pFileName )
fclose( pFile );
return nFileSize;
}
char * Scl_LibertyFileContents( char * pFileName, int nContents )
char * Scl_LibertyFileContents( char * pFileName, long nContents )
{
FILE * pFile = fopen( pFileName, "rb" );
char * pContents = ABC_ALLOC( char, nContents+1 );
@ -573,7 +573,7 @@ void Scl_LibertyStringDump( char * pFileName, Vec_Str_t * vStr )
Scl_Tree_t * Scl_LibertyStart( char * pFileName )
{
Scl_Tree_t * p;
int RetValue;
long RetValue;
// read the file into the buffer
Scl_LibertyFixFileName( pFileName );
RetValue = Scl_LibertyFileSize( pFileName );
@ -867,7 +867,7 @@ int Scl_LibertyReadTimeUnit( Scl_Tree_t * p )
return 12;
break;
}
printf( "Libery parser cannot read \"time_unit\". Assuming time_unit : \"1ns\".\n" );
printf( "Liberty parser cannot read \"time_unit\". Assuming time_unit : \"1ns\".\n" );
return 9;
}
void Scl_LibertyReadLoadUnit( Scl_Tree_t * p, Vec_Str_t * vOut )
@ -887,7 +887,7 @@ void Scl_LibertyReadLoadUnit( Scl_Tree_t * p, Vec_Str_t * vOut )
else break;
return;
}
printf( "Libery parser cannot read \"capacitive_load_unit\". Assuming capacitive_load_unit(1, pf).\n" );
printf( "Liberty parser cannot read \"capacitive_load_unit\". Assuming capacitive_load_unit(1, pf).\n" );
Vec_StrPutF_( vOut, 1.0 );
Vec_StrPutI_( vOut, 12 );
}

16
src/map/scl/sclSize.c
View File

@ -140,6 +140,9 @@ void Abc_SclTimeNtkPrint( SC_Man * p, int fShowAll, int fPrintPath )
Abc_Obj_t * pObj, * pPivot = Abc_SclFindCriticalCo( p, &fRise );
float maxDelay = Abc_SclObjTimeOne( p, pPivot, fRise );
p->ReportDelay = maxDelay;
// used for Floyds cycle detection algorithm
unsigned int tortoiseIndex = 0;
int tortoiseStep = 0;
#ifdef WIN32
printf( "WireLoad = \"%s\" ", p->pWLoadUsed ? p->pWLoadUsed->pName : "none" );
@ -197,7 +200,7 @@ void Abc_SclTimeNtkPrint( SC_Man * p, int fShowAll, int fPrintPath )
while ( pObj && Abc_ObjIsNode(pObj) )
{
i++;
nLength = Abc_MaxInt( nLength, Abc_SclObjCell(pObj) ? strlen(Abc_SclObjCell(pObj)->pName) : 2 /* strlen("pi") */ );
nLength = Abc_MaxInt( nLength, strlen(Abc_SclObjCell(pObj)->pName) );
pObj = Abc_SclFindMostCriticalFanin( p, &fRise, pObj );
}
@ -221,10 +224,18 @@ void Abc_SclTimeNtkPrint( SC_Man * p, int fShowAll, int fPrintPath )
Vec_PtrPush( vPath, pPivot );
pObj = Abc_ObjFanin0(pPivot);
while ( pObj )//&& Abc_ObjIsNode(pObj) )
{
{
Vec_PtrPush( vPath, pObj );
pPrev = pObj;
pObj = Abc_SclFindMostCriticalFanin( p, &fRise, pObj );
// move the tortoise at half the speed (trailing)
tortoiseStep = (tortoiseStep + 1) % 2;
tortoiseIndex += tortoiseStep;
// if they see the same element, we are in a loop
if(vPath->pArray[tortoiseIndex] == pObj) {
break;
}
}
Vec_PtrForEachEntryReverse( Abc_Obj_t *, vPath, pObj, i )
{
@ -913,3 +924,4 @@ void Abc_SclPrintBuffers( SC_Lib * pLib, Abc_Ntk_t * pNtk, int fVerbose )
ABC_NAMESPACE_IMPL_END

8
src/misc/extra/extraUtilUtil.c
View File

@ -394,9 +394,17 @@ ABC_NAMESPACE_IMPL_START
double Extra_CpuTimeDouble()
{
/*
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
*/
struct timespec ts;
if ( clock_gettime(CLOCK_MONOTONIC, &ts) < 0 )
return (double)-1;
double res = ((double) ts.tv_sec);
res += ((double) ts.tv_nsec) / 1000000000;
return res;
}
#endif

2
src/opt/dar/darRefact.c
View File

@ -586,7 +586,7 @@ p->timeEval += Abc_Clock() - clk;
// if we end up here, a rewriting step is accepted
nNodeBefore = Aig_ManNodeNum( pAig );
pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest );
assert( (int)Aig_Regular(pObjNew)->Level <= Required );
//assert( (int)Aig_Regular(pObjNew)->Level <= Required );
// replace the node
Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
// compare the gains

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 );

3
src/opt/sim/simUtils.c
View File

@ -60,7 +60,8 @@ Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, int fClean )
int i;
assert( nSize > 0 && nWords > 0 );
vInfo = Vec_PtrAlloc( nSize );
vInfo->pArray[0] = ABC_ALLOC( unsigned, nSize * nWords );
vInfo->pArray[0] = ABC_ALLOC( unsigned, (long)nSize * (long)nWords );
assert( vInfo->pArray[0]);
if ( fClean )
memset( vInfo->pArray[0], 0, sizeof(unsigned) * nSize * nWords );
for ( i = 1; i < nSize; i++ )

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) );

41
src/proof/cec/cecSatG2.c
View File

@ -101,6 +101,7 @@ struct Cec4_Man_t_
Vec_Int_t * vDisprPairs;
Vec_Bit_t * vFails;
Vec_Bit_t * vCoDrivers;
Vec_Int_t * vPairs;
int iPosRead; // candidate reading position
int iPosWrite; // candidate writing position
int iLastConst; // last const node proved
@ -250,6 +251,7 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
p->vPat = Vec_IntAlloc( 100 );
p->vDisprPairs = Vec_IntAlloc( 100 );
p->vFails = Vec_BitStart( Gia_ManObjNum(pAig) );
p->vPairs = pPars->fUseCones ? Vec_IntAlloc( 100 ) : NULL;
//pAig->pData = p->pSat; // point AIG manager to the solver
//Vec_IntFreeP( &p->pAig->vPats );
//p->pAig->vPats = Vec_IntAlloc( 1000 );
@ -304,6 +306,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
Vec_IntFreeP( &p->vPat );
Vec_IntFreeP( &p->vDisprPairs );
Vec_BitFreeP( &p->vFails );
Vec_IntFreeP( &p->vPairs );
Vec_BitFreeP( &p->vCoDrivers );
Vec_IntFreeP( &p->vRefClasses );
Vec_IntFreeP( &p->vRefNodes );
@ -1686,12 +1689,26 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
{
p->nSatUndec++;
assert( status == GLUCOSE_UNDEC );
Gia_ObjSetFailed( p->pAig, iObj );
Vec_BitWriteEntry( p->vFails, iObj, 1 );
//if ( iRepr )
//Vec_BitWriteEntry( p->vFails, iRepr, 1 );
p->timeSatUndec += Abc_Clock() - clk;
RetValue = 2;
if ( p->vPairs ) // speculate
{
Vec_IntPushTwo( p->vPairs, Abc_Var2Lit(iRepr, 0), Abc_Var2Lit(iObj, fCompl) );
p->timeSatUndec += Abc_Clock() - clk;
// mark as proved
pObj->Value = Abc_LitNotCond( pRepr->Value, fCompl );
Gia_ObjSetProved( p->pAig, iObj );
if ( iRepr == 0 )
p->iLastConst = iObj;
RetValue = 1;
}
else
{
Gia_ObjSetFailed( p->pAig, iObj );
Vec_BitWriteEntry( p->vFails, iObj, 1 );
//if ( iRepr )
//Vec_BitWriteEntry( p->vFails, iRepr, 1 );
p->timeSatUndec += Abc_Clock() - clk;
RetValue = 2;
}
}
return RetValue;
}
@ -1896,6 +1913,18 @@ finalize:
pMan->nSatSat, pMan->nConflicts[0][0], (float)pMan->nConflicts[0][1]/Abc_MaxInt(1, pMan->nSatSat -pMan->nConflicts[0][0]), pMan->nConflicts[0][2],
pMan->nSatUndec,
pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) );
if ( pMan->vPairs && Vec_IntSize(pMan->vPairs) )
{
extern char * Extra_FileNameGeneric( char * FileName );
char pFileName[1000], * pBase = Extra_FileNameGeneric(p->pName);
extern Gia_Man_t * Gia_ManDupMiterCones( Gia_Man_t * p, Vec_Int_t * vPairs );
Gia_Man_t * pM = Gia_ManDupMiterCones( p, pMan->vPairs );
sprintf( pFileName, "%s_sm.aig", pBase );
Gia_AigerWrite( pM, pFileName, 0, 0, 0 );
Gia_ManStop( pM );
ABC_FREE( pBase );
printf( "Dumped miter \"%s\" with %d pairs.\n", pFileName, pMan->vPairs ? Vec_IntSize(pMan->vPairs)/2 : -1 );
}
Cec4_ManDestroy( pMan );
//Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 );

2
src/proof/fraig/fraigInt.h
View File

@ -383,7 +383,7 @@ extern void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordSt
/*=== fraigPrime.c =============================================================*/
extern int s_FraigPrimes[FRAIG_MAX_PRIMES];
/*=== fraigSat.c ===============================================================*/
extern int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
extern int Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
/*=== fraigTable.c =============================================================*/
extern Fraig_HashTable_t * Fraig_HashTableCreate( int nSize );
extern void Fraig_HashTableFree( Fraig_HashTable_t * p );

2
src/proof/fraig/fraigSat.c
View File

@ -548,7 +548,7 @@ p->time3 += Abc_Clock() - clk;
SeeAlso []
***********************************************************************/
int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
int Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
{
int RetValue, RetValue1, i, fComp;
abctime clk;

4
src/proof/fraig/fraigUtil.c
View File

@ -872,13 +872,13 @@ clk = Abc_Clock();
pNode2 = vPivots->pArray[k];
if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) )
{
if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) )
if ( Fraig_NodeIsImplification( pMan, pNode, pNode2, -1 ) )
nProved++;
Counter++;
}
else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) )
{
if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) )
if ( Fraig_NodeIsImplification( pMan, pNode2, pNode, -1 ) )
nProved++;
Counter++;
}

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

4
src/sat/cnf/cnfUtil.c
View File

@ -21,8 +21,6 @@
#include "cnf.h"
#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
#ifdef _MSC_VER
#define unlink _unlink
#else
@ -39,6 +37,8 @@ ABC_NAMESPACE_IMPL_START
#endif
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////

4
src/sat/glucose/AbcGlucose.cpp
View File

@ -842,7 +842,7 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars, int fDumpCnf )
if ( pPars->pre )
{
S.eliminate(true);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fDumpCnf )
@ -1510,7 +1510,7 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars)
if (pPars->pre)
{
S.eliminate(true);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

4
src/sat/glucose2/AbcGlucose2.cpp
View File

@ -869,7 +869,7 @@ void Glucose2_SolveCnf( char * pFileName, Glucose2_Pars * pPars )
if ( pPars->pre )
{
S.eliminate(true);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
@ -1528,7 +1528,7 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars)
if (pPars->pre)
{
S.eliminate(true);
printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
printf( "c Simplification removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}