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

Merge remote-tracking branch 'upstream/master' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2023-09-11 16:16:47 +02:00
parent bb64142b07 20f9095cf2
commit 9537f391fd
93 changed files with 8185 additions and 574 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -6,6 +6,7 @@ ReleaseLib/
ReleaseExe/
ReleaseExt/
_/
_TEST/
lib/abc*
lib/m114*

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:

4
abclib.dsp
View File

@ -387,6 +387,10 @@ SOURCE=.\src\base\abci\abcOrder.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcOrchestration.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcPart.c
# End Source File
# Begin Source File

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 );
/*=== 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 );
}

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

@ -120,6 +120,7 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in
}
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{
if ( !Abc_FrameIsBatchMode() )
printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i );
break;
}

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

@ -1069,6 +1069,51 @@ Gia_Man_t * Gia_ManDupPiPerm( Gia_Man_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManCreatePerm( int n )
{
Vec_Int_t * vPerm = Vec_IntStartNatural( n );
int i, * pPerm = Vec_IntArray( vPerm );
for ( i = 0; i < n; i++ )
{
int j = Abc_Random(0) % n;
ABC_SWAP( int, pPerm[i], pPerm[j] );
}
return vPerm;
}
Gia_Man_t * Gia_ManDupRandPerm( Gia_Man_t * p )
{
Vec_Int_t * vPiPerm = Gia_ManCreatePerm( Gia_ManCiNum(p) );
Vec_Int_t * vPoPerm = Gia_ManCreatePerm( Gia_ManCoNum(p) );
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
Gia_ManPi(p, Vec_IntEntry(vPiPerm,i))->Value = Gia_ManAppendCi(pNew) ^ (Abc_Random(0) & 1);
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm,i))) ^ (Abc_Random(0) & 1) );
Vec_IntFree( vPiPerm );
Vec_IntFree( vPoPerm );
return pNew;
}
/**Function*************************************************************
Synopsis [Appends second AIG without any changes.]
@ -1559,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.]
@ -5539,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

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

@ -803,7 +803,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p )
Vec_Int_t * vLeaves, * vTruth, * vVisited;
int * pLutClass, ClassCounts[222] = {0};
int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2;
unsigned * pTruth;
unsigned * pTruth; int nLutSize = 0;
assert( Gia_ManHasMapping(p) );
assert( Gia_ManLutSizeMax( p ) <= 4 );
vLeaves = Vec_IntAlloc( 100 );
@ -813,6 +813,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p )
Gia_ManCleanTruth( p );
Gia_ManForEachLut( p, i )
{
nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p,i) );
if ( Gia_ObjLutSize(p,i) > 4 )
continue;
Vec_IntClear( vLeaves );
@ -872,6 +873,55 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p )
Abc_Print( 1, "Approximate number of 4:1 MUX structures: All = %6d (%7.2f %%) MFFC = %6d (%7.2f %%)\n",
OtherClasses, 100.0 * OtherClasses / (nTotal+1),
OtherClasses2, 100.0 * OtherClasses2 / (nTotal+1) );
// print information about LUT pairs
if ( nLutSize <= 4 )
{
int nTopPairs = 100, nTopShow = 30;
int i, j, k, iFan, * pVec = NULL;
Vec_Int_t * vPairs = Vec_IntAlloc( 3 * nTopPairs );
Gia_ManForEachLut( p, j ) {
Gia_LutForEachFanin( p, j, iFan, k ) {
int Num1 = pLutClass[iFan];
int Num2 = pLutClass[j];
assert( Vec_IntSize(vPairs) % 3 == 0 );
for ( i = 0; i < Vec_IntSize(vPairs); i += 3 )
if ( Vec_IntEntry(vPairs, i+0) == Num1 && Vec_IntEntry(vPairs, i+1) == Num2 )
break;
if ( i == Vec_IntSize(vPairs) ) {
if ( Vec_IntSize(vPairs) < 3*nTopPairs ) {
Vec_IntPush( vPairs, Num1 );
Vec_IntPush( vPairs, Num2 );
Vec_IntPush( vPairs, 1 );
}
continue;
}
// found this pair
assert( Vec_IntEntry(vPairs, i+0) == Num1 );
assert( Vec_IntEntry(vPairs, i+1) == Num2 );
Vec_IntAddToEntry( vPairs, i+2, 1 );
// sort
pVec = Vec_IntArray( vPairs );
while ( i > 0 && pVec[i+2] > pVec[i-1] ) {
ABC_SWAP( int, pVec[i+0], pVec[i-3] )
ABC_SWAP( int, pVec[i+1], pVec[i-2] )
ABC_SWAP( int, pVec[i+2], pVec[i-1] )
i -= 3;
}
while ( i < Vec_IntSize(vPairs) - 3 && pVec[i+2] < pVec[i+5] ) {
ABC_SWAP( int, pVec[i+0], pVec[i+3] )
ABC_SWAP( int, pVec[i+1], pVec[i+4] )
ABC_SWAP( int, pVec[i+2], pVec[i+5] )
i += 3;
assert( 0 );
}
}
}
pVec = Vec_IntArray( vPairs );
nTopShow = Abc_MinInt( nTopShow, Vec_IntSize(vPairs)/3 );
for ( i = 0; i < 3*nTopShow; i += 3 )
printf( "%3d : (%3d %3d) x %3d\n", i/3, pVec[i+0], pVec[i+1], pVec[i+2] );
Vec_IntFree( vPairs );
}
ABC_FREE( pLutClass );
}
@ -1191,6 +1241,90 @@ 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_ManDumpInterface( 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.]
@ -1273,38 +1407,33 @@ 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 )
{
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) )
{
printf( "Currently cannot write sequential AIG.\n" );
return;
}
pFile = fopen( pFileName, "wb" );
int i, k, iObj, nRegs = Gia_ManRegNum(p);
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open output file \"%s\".\n", pFileName );
return;
}
if ( fInter || nRegs )
Gia_ManDumpInterface( 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 )
{
@ -1455,6 +1584,8 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int
Vec_BitFree( vInvs );
Vec_BitFree( vUsed );
Gia_ManSetRegNum( p, nRegs );
}
////////////////////////////////////////////////////////////////////////

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

@ -813,6 +813,13 @@ int * Abc_FrameReadMiniAigEquivClasses( Abc_Frame_t * pAbc )
printf( "Equivalence classes of internal GIA are not available.\n" );
return NULL;
}
else if ( 0 )
{
int i;
for ( i = 1; i < Gia_ManObjNum(pAbc->pGia2); i++ )
if ( Gia_ObjHasRepr(pAbc->pGia2, i) )
printf( "Obj %3d : Repr %3d Proved %d Failed %d\n", i, Gia_ObjRepr(pAbc->pGia2, i), Gia_ObjProved(pAbc->pGia2, i), Gia_ObjFailed(pAbc->pGia2, i) );
}
if ( Gia_ManObjNum(pAbc->pGia2) != Gia_ManObjNum(pAbc->pGiaMiniAig) )
printf( "Internal GIA with equivalence classes is not directly derived from MiniAig.\n" );
// derive the set of equivalent node pairs

112
src/aig/gia/giaSatMap.c
View File

@ -269,6 +269,118 @@ static inline int sat_solver_add_and2( sat_solver * pSat, int iVar, int iVar0, i
return 3;
}
/**Function*************************************************************
Synopsis [Adds a general cardinality constraint in terms of vVars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Card_AddClause( Vec_Int_t * p, int* begin, int* end )
{
Vec_IntPush( p, (int)(end-begin) );
while ( begin < end )
Vec_IntPush( p, (int)*begin++ );
return 1;
}
static inline int Card_AddHalfSorter( Vec_Int_t * p, int iVarA, int iVarB, int iVar0, int iVar1 )
{
lit Lits[3];
int Cid;
Lits[0] = toLitCond( iVarA, 0 );
Lits[1] = toLitCond( iVar0, 1 );
Cid = Card_AddClause( p, Lits, Lits + 2 );
assert( Cid );
Lits[0] = toLitCond( iVarA, 0 );
Lits[1] = toLitCond( iVar1, 1 );
Cid = Card_AddClause( p, Lits, Lits + 2 );
assert( Cid );
Lits[0] = toLitCond( iVarB, 0 );
Lits[1] = toLitCond( iVar0, 1 );
Lits[2] = toLitCond( iVar1, 1 );
Cid = Card_AddClause( p, Lits, Lits + 3 );
assert( Cid );
return 3;
}
static inline void Card_AddSorter( Vec_Int_t * p, int * pVars, int i, int k, int * pnVars )
{
int iVar1 = (*pnVars)++;
int iVar2 = (*pnVars)++;
Card_AddHalfSorter( p, iVar1, iVar2, pVars[i], pVars[k] );
pVars[i] = iVar1;
pVars[k] = iVar2;
}
static inline void Card_AddCardinConstrMerge( Vec_Int_t * p, int * pVars, int lo, int hi, int r, int * pnVars )
{
int i, step = r * 2;
if ( step < hi - lo )
{
Card_AddCardinConstrMerge( p, pVars, lo, hi-r, step, pnVars );
Card_AddCardinConstrMerge( p, pVars, lo+r, hi, step, pnVars );
for ( i = lo+r; i < hi-r; i += step )
Card_AddSorter( p, pVars, i, i+r, pnVars );
for ( i = lo+r; i < hi-r-1; i += r )
{
lit Lits[2] = { Abc_Var2Lit(pVars[i], 0), Abc_Var2Lit(pVars[i+r], 1) };
int Cid = Card_AddClause( p, Lits, Lits + 2 );
assert( Cid );
}
}
}
static inline void Card_AddCardinConstrRange( Vec_Int_t * p, int * pVars, int lo, int hi, int * pnVars )
{
if ( hi - lo >= 1 )
{
int i, mid = lo + (hi - lo) / 2;
for ( i = lo; i <= mid; i++ )
Card_AddSorter( p, pVars, i, i + (hi - lo + 1) / 2, pnVars );
Card_AddCardinConstrRange( p, pVars, lo, mid, pnVars );
Card_AddCardinConstrRange( p, pVars, mid+1, hi, pnVars );
Card_AddCardinConstrMerge( p, pVars, lo, hi, 1, pnVars );
}
}
int Card_AddCardinConstrPairWise( Vec_Int_t * p, Vec_Int_t * vVars )
{
int nVars = Vec_IntSize(vVars);
Card_AddCardinConstrRange( p, Vec_IntArray(vVars), 0, nVars - 1, &nVars );
return nVars;
}
int Card_AddCardinSolver( int LogN, Vec_Int_t ** pvVars, Vec_Int_t ** pvRes )
{
int nVars = 1 << LogN;
int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1);
Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
int nVarsReal = Card_AddCardinConstrPairWise( vRes, vVars );
assert( nVarsReal == nVarsAlloc );
Vec_IntPush( vRes, -1 );
*pvVars = vVars;
*pvRes = vRes;
return nVarsReal;
}
sat_solver * Sbm_AddCardinSolver2( int LogN, Vec_Int_t ** pvVars, Vec_Int_t ** pvRes )
{
Vec_Int_t * vVars = NULL;
Vec_Int_t * vRes = NULL;
int nVarsReal = Card_AddCardinSolver( LogN, &vVars, &vRes ), i, size;
sat_solver * pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVarsReal );
for ( i = 0, size = Vec_IntEntry(vRes, i++); i < Vec_IntSize(vRes); i += size, size = Vec_IntEntry(vRes, i++) )
sat_solver_addclause( pSat, Vec_IntEntryP(vRes, i), Vec_IntEntryP(vRes, i+size) );
if ( pvVars ) *pvVars = vVars;
if ( pvRes ) *pvRes = vRes;
return pSat;
}
/**Function*************************************************************
Synopsis [Adds a general cardinality constraint in terms of vVars.]

52
src/aig/gia/giaSimBase.c
View File

@ -3689,6 +3689,58 @@ Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p )
return vOut;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q )
{
Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
Vec_Wrd_t * vSimsP = Gia_ManSimPatSimOut( p, vSimsPi, 0 );
Vec_Wrd_t * vSimsQ = Gia_ManSimPatSimOut( q, vSimsPi, 0 );
int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p), Count = 0;
Gia_Obj_t * pObjP, * pObjQ;
Gia_ManSetPhase( p );
Gia_ManSetPhase( q );
Gia_ManForEachObj( p, pObjP, i ) {
word * pSim = Vec_WrdEntryP( vSimsP, i * nWords );
if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
}
Gia_ManForEachObj( q, pObjQ, i ) {
word * pSim = Vec_WrdEntryP( vSimsQ, i * nWords );
if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
}
Gia_ManForEachAnd( q, pObjQ, i ) {
word * pSimQ = Vec_WrdEntryP( vSimsQ, i * nWords );
int fFirst = 1;
Gia_ManForEachObj( p, pObjP, k ) {
word * pSimP = Vec_WrdEntryP( vSimsP, k * nWords );
if ( !Abc_TtEqual(pSimQ, pSimP, nWords) )
continue;
if ( fFirst ) {
printf( "%5d :", i );
fFirst = 0;
Count++;
}
printf( " %5d(%d)", k, pObjQ->fPhase ^ pObjP->fPhase );
}
if ( !fFirst )
printf( "\n");
}
printf( "Found %d equivalent nodes.\n", Count );
Vec_WrdFree( vSimsP );
Vec_WrdFree( vSimsQ );
Vec_WrdFree( vSimsPi );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -22,6 +22,23 @@
#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
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#endif
#endif
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
@ -32,6 +49,169 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Processing on a single core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_StochProcessOne( Gia_Man_t * p, char * pScript, int Rand, int TimeSecs )
{
Gia_Man_t * pNew;
char FileName[100], Command[1000];
sprintf( FileName, "%06x.aig", Rand );
Gia_AigerWrite( p, FileName, 0, 0, 0 );
sprintf( Command, "./abc -q \"&read %s; %s; &write %s\"", FileName, pScript, FileName );
if ( system( (char *)Command ) )
{
fprintf( stderr, "The following command has returned non-zero exit status:\n" );
fprintf( stderr, "\"%s\"\n", (char *)Command );
fprintf( stderr, "Sorry for the inconvenience.\n" );
fflush( stdout );
unlink( FileName );
return Gia_ManDup(p);
}
pNew = Gia_AigerRead( FileName, 0, 0, 0 );
unlink( FileName );
if ( pNew && Gia_ManAndNum(pNew) < Gia_ManAndNum(p) )
return pNew;
Gia_ManStopP( &pNew );
return Gia_ManDup(p);
}
void Gia_StochProcessArray( Vec_Ptr_t * vGias, char * pScript, int TimeSecs, int fVerbose )
{
Gia_Man_t * pGia, * pNew; int i;
Vec_Int_t * vRands = Vec_IntAlloc( Vec_PtrSize(vGias) );
Abc_Random(1);
for ( i = 0; i < Vec_PtrSize(vGias); i++ )
Vec_IntPush( vRands, Abc_Random(0) % 0x1000000 );
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
{
pNew = Gia_StochProcessOne( pGia, pScript, Vec_IntEntry(vRands, i), TimeSecs );
Gia_ManStop( pGia );
Vec_PtrWriteEntry( vGias, i, pNew );
}
Vec_IntFree( vRands );
}
/**Function*************************************************************
Synopsis [Processing on a many cores.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#ifndef ABC_USE_PTHREADS
void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose )
{
Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose );
}
#else // pthreads are used
#define PAR_THR_MAX 100
typedef struct Gia_StochThData_t_
{
Vec_Ptr_t * vGias;
char * pScript;
int Index;
int Rand;
int nTimeOut;
int fWorking;
} Gia_StochThData_t;
void * Gia_StochWorkerThread( void * pArg )
{
Gia_StochThData_t * pThData = (Gia_StochThData_t *)pArg;
volatile int * pPlace = &pThData->fWorking;
Gia_Man_t * pGia, * pNew;
while ( 1 )
{
while ( *pPlace == 0 );
assert( pThData->fWorking );
if ( pThData->Index == -1 )
{
pthread_exit( NULL );
assert( 0 );
return NULL;
}
pGia = (Gia_Man_t *)Vec_PtrEntry( pThData->vGias, pThData->Index );
pNew = Gia_StochProcessOne( pGia, pThData->pScript, pThData->Rand, pThData->nTimeOut );
Gia_ManStop( pGia );
Vec_PtrWriteEntry( pThData->vGias, pThData->Index, pNew );
pThData->fWorking = 0;
}
assert( 0 );
return NULL;
}
void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose )
{
Gia_StochThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
int i, k, status;
if ( fVerbose )
printf( "Running concurrent synthesis with %d processes.\n", nProcs );
fflush( stdout );
if ( nProcs < 2 )
return Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose );
// subtract manager thread
nProcs--;
assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
// start threads
Abc_Random(1);
for ( i = 0; i < nProcs; i++ )
{
ThData[i].vGias = vGias;
ThData[i].pScript = pScript;
ThData[i].Index = -1;
ThData[i].Rand = Abc_Random(0) % 0x1000000;
ThData[i].nTimeOut = TimeSecs;
ThData[i].fWorking = 0;
status = pthread_create( WorkerThread + i, NULL, Gia_StochWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
}
// look at the threads
for ( k = 0; k < Vec_PtrSize(vGias); k++ )
{
for ( i = 0; i < nProcs; i++ )
{
if ( ThData[i].fWorking )
continue;
ThData[i].Index = k;
ThData[i].fWorking = 1;
break;
}
if ( i == nProcs )
k--;
}
// wait till threads finish
for ( i = 0; i < nProcs; i++ )
if ( ThData[i].fWorking )
i = -1;
// stop threads
for ( i = 0; i < nProcs; i++ )
{
assert( !ThData[i].fWorking );
// stop
ThData[i].Index = -1;
ThData[i].fWorking = 1;
}
}
#endif // pthreads are used
/**Function*************************************************************
Synopsis []
@ -184,7 +364,7 @@ Gia_Man_t * Gia_ManDupDivideOne( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vA
pNew->vMapping = vMapping;
return pNew;
}
Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript )
Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript, int nProcs, int TimeOut )
{
Vec_Ptr_t * vAigs = Vec_PtrAlloc( Vec_WecSize(vCis) ); int i;
for ( i = 0; i < Vec_WecSize(vCis); i++ )
@ -192,7 +372,8 @@ Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds
Gia_ManCollectNodes( p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i) );
Vec_PtrPush( vAigs, Gia_ManDupDivideOne(p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i)) );
}
Gia_ManStochSynthesis( vAigs, pScript );
//Gia_ManStochSynthesis( vAigs, pScript );
Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 );
return vAigs;
}
Gia_Man_t * Gia_ManDupStitch( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, Vec_Ptr_t * vAigs, int fHash )
@ -388,7 +569,7 @@ Vec_Wec_t * Gia_ManStochOutputs( Gia_Man_t * p, Vec_Wec_t * vAnds )
SeeAlso []
***********************************************************************/
void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript )
void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs )
{
abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0;
abctime clkStart = Abc_Clock();
@ -407,7 +588,7 @@ void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerb
Vec_Wec_t * vAnds = Gia_ManStochNodes( pGia, nMaxSize, Abc_Random(0) & 0x7FFFFFFF );
Vec_Wec_t * vIns = Gia_ManStochInputs( pGia, vAnds );
Vec_Wec_t * vOuts = Gia_ManStochOutputs( pGia, vAnds );
Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript );
Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript, nProcs, TimeOut );
Gia_Man_t * pNew = Gia_ManDupStitchMap( pGia, vIns, vAnds, vOuts, vAigs );
int fMapped = Gia_ManHasMapping(pGia) && Gia_ManHasMapping(pNew);
Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );

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]

18
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 )
@ -897,7 +898,20 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
{
if ( Abc_ObjIsCo(pFanout) )
{
Abc_ObjPatchFanin( pFanout, pOld, pNew );
pFanin1 = Abc_ObjRegular( pNew );
if ( pFanin1->fMarkB )
Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin1 );
if ( fUpdateLevel && pMan->pNtkAig->vLevelsR )
{
Abc_ObjSetReverseLevel( pFanin1, Abc_ObjReverseLevel(pOld) );
assert( pFanin1->fMarkB == 0 );
if ( !Abc_ObjIsCi(pFanin1) )
{
pFanin1->fMarkB = 1;
Vec_VecPush( pMan->vLevelsR, Abc_ObjReverseLevel(pFanin1), pFanin1 );
}
}
Abc_ObjPatchFanin( pFanout, pOld, pNew );
continue;
}
// find the old node as a fanin of this fanout

36
src/base/abc/abcFunc.c
View File

@ -1265,6 +1265,42 @@ int Abc_NtkToAig( Abc_Ntk_t * pNtk )
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_ObjFaninSort( Abc_Obj_t * pObj )
{
Vec_Int_t * vFanins = Abc_ObjFaninVec( pObj );
char * pCube, * pSop = (char*)pObj->pData;
int i, j, nVars = Abc_SopGetVarNum( pSop );
assert( nVars == Vec_IntSize(vFanins) );
for ( i = 0; i < Vec_IntSize(vFanins); i++ )
for ( j = i+1; j < Vec_IntSize(vFanins); j++ )
{
if ( Vec_IntEntry(vFanins, i) < Vec_IntEntry(vFanins, j) )
continue;
ABC_SWAP( int, Vec_IntArray(vFanins)[i], Vec_IntArray(vFanins)[j] );
for ( pCube = pSop; *pCube; pCube += nVars + 3 ) {
ABC_SWAP( char, pCube[i], pCube[j] );
}
}
}
void Abc_NtkFaninSort( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj; int i;
assert( Abc_NtkIsSopLogic(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
Abc_ObjFaninSort( pObj );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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/abcNetlist.c
View File

@ -220,7 +220,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
if ( pObj->pCopy->pCopy ) // the net of the new object is already created
continue;
// create the new net
sprintf( Buffer, "new_%s_", Abc_ObjName(pObj) );
sprintf( Buffer, "new_%s", Abc_ObjName(pObj) );
//pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) ); // here we create net names such as "n48", where 48 is the ID of the node
pNet = Abc_NtkFindOrCreateNet( pNtkNew, Buffer );
Abc_ObjAddFanin( pNet, pObj->pCopy );

95
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) );
@ -984,29 +986,41 @@ char * Abc_SopFromTruthBin( char * pTruth )
if ( Digit == 1 )
Vec_IntPush( vMints, nTruthSize - 1 - i );
}
/*
if ( Vec_IntSize( vMints ) == 0 || Vec_IntSize( vMints ) == nTruthSize )
{
Vec_IntFree( vMints );
printf( "Cannot create constant function.\n" );
return NULL;
}
// create the SOP representation of the minterms
Length = Vec_IntSize(vMints) * (nVars + 3);
pSopCover = ABC_ALLOC( char, Length + 1 );
pSopCover[Length] = 0;
Vec_IntForEachEntry( vMints, Mint, i )
*/
if ( Vec_IntSize(vMints) == 0 || Vec_IntSize(vMints) == (1 << nVars) )
{
pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ )
// if ( Mint & (1 << (nVars-1-b)) )
if ( Mint & (1 << b) )
pCube[b] = '1';
else
pCube[b] = '0';
pCube[nVars + 0] = ' ';
pCube[nVars + 1] = '1';
pCube[nVars + 2] = '\n';
pSopCover = ABC_ALLOC( char, 4 );
pSopCover[0] = ' ';
pSopCover[1] = '0' + (Vec_IntSize(vMints) > 0);
pSopCover[2] = '\n';
pSopCover[3] = 0;
}
else
{
// create the SOP representation of the minterms
Length = Vec_IntSize(vMints) * (nVars + 3);
pSopCover = ABC_ALLOC( char, Length + 1 );
pSopCover[Length] = 0;
Vec_IntForEachEntry( vMints, Mint, i )
{
pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ )
// if ( Mint & (1 << (nVars-1-b)) )
if ( Mint & (1 << b) )
pCube[b] = '1';
else
pCube[b] = '0';
pCube[nVars + 0] = ' ';
pCube[nVars + 1] = '1';
pCube[nVars + 2] = '\n';
}
}
Vec_IntFree( vMints );
return pSopCover;
@ -1074,37 +1088,34 @@ char * Abc_SopFromTruthHex( char * pTruth )
}
// create the SOP representation of the minterms
Length = Vec_IntSize(vMints) * (nVars + 3);
pSopCover = ABC_ALLOC( char, Length + 1 );
pSopCover[Length] = 0;
Vec_IntForEachEntry( vMints, Mint, i )
if ( Vec_IntSize(vMints) == 0 || Vec_IntSize(vMints) == (1 << nVars) )
{
pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ )
// if ( Mint & (1 << (nVars-1-b)) )
if ( Mint & (1 << b) )
pCube[b] = '1';
else
pCube[b] = '0';
pCube[nVars + 0] = ' ';
pCube[nVars + 1] = '1';
pCube[nVars + 2] = '\n';
pSopCover = ABC_ALLOC( char, 4 );
pSopCover[0] = ' ';
pSopCover[1] = '0' + (Vec_IntSize(vMints) > 0);
pSopCover[2] = '\n';
pSopCover[3] = 0;
}
/*
// create TT representation
else
{
extern void Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
unsigned uTruth = 0;
int nVarsAll = 4;
assert( nVarsAll == 4 );
assert( nVars <= nVarsAll );
Length = Vec_IntSize(vMints) * (nVars + 3);
pSopCover = ABC_ALLOC( char, Length + 1 );
pSopCover[Length] = 0;
Vec_IntForEachEntry( vMints, Mint, i )
uTruth |= (1 << Mint);
// uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24);
uTruth = uTruth | (uTruth << 16);
Bdc_ManDecomposeTest( uTruth, nVarsAll );
{
pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ )
// if ( Mint & (1 << (nVars-1-b)) )
if ( Mint & (1 << b) )
pCube[b] = '1';
else
pCube[b] = '0';
pCube[nVars + 0] = ' ';
pCube[nVars + 1] = '1';
pCube[nVars + 2] = '\n';
}
}
*/
Vec_IntFree( vMints );
return pSopCover;
}

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

File diff suppressed because it is too large Load Diff

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

8
src/base/abci/abcDsd.c
View File

@ -175,11 +175,11 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
// save the CI nodes in the DSD nodes
Abc_AigConst1(pNtk)->pCopy = pNodeNew = Abc_NtkCreateNodeConst1(pNtkNew);
Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(ABC_PTRINT_T)pNodeNew );
Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (word)(ABC_PTRINT_T)pNodeNew );
Abc_NtkForEachCi( pNtk, pNode, i )
{
pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNode->pCopy );
Dsd_NodeSetMark( pNodeDsd, (word)(ABC_PTRINT_T)pNode->pCopy );
}
// collect DSD nodes in DFS order (leaves and const1 are not collected)
@ -298,7 +298,7 @@ printf( "\n" );
}
}
pNodeNew->pData = bLocal;
Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNodeNew );
Dsd_NodeSetMark( pNodeDsd, (word)(ABC_PTRINT_T)pNodeNew );
return pNodeNew;
}
@ -417,7 +417,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
Abc_ObjForEachFanin( pNode, pFanin, i )
{
pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
Dsd_NodeSetMark( pFaninDsd, (int)(ABC_PTRINT_T)pFanin );
Dsd_NodeSetMark( pFaninDsd, (word)(ABC_PTRINT_T)pFanin );
}
// construct the intermediate nodes

66
src/base/abci/abcGen.c
View File

@ -706,7 +706,7 @@ void Abc_GenRandom( char * pFileName, int nPis )
unsigned * pTruth;
int i, b, w, nWords = Abc_TruthWordNum( nPis );
int nDigitsIn;
Aig_ManRandom( 1 );
//Aig_ManRandom( 1 );
pTruth = ABC_ALLOC( unsigned, nWords );
for ( w = 0; w < nWords; w++ )
pTruth[w] = Aig_ManRandom( 0 );
@ -1140,6 +1140,70 @@ void Abc_GenBooth( char * pFileName, int nVars )
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_GenGraph( char * pFileName, int nPis )
{
FILE * pFile;
int i, a, b, w, nDigitsIn, nWords = Abc_TruthWordNum( nPis*(nPis-1)/2 );
unsigned * pTruth = ABC_CALLOC( unsigned, nWords );
unsigned char M[10][10] = {{0}}, C[100][2] = {{0}}, nVars = 0;
assert( nPis <= 8 );
for ( a = 0; a < nPis; a++ )
for ( b = a+1; b < nPis; b++ )
C[nVars][0] = a, C[nVars][1] = b, nVars++;
for ( i = 0; i < (1<<nVars); i++ )
{
int fChanges = 1;
for ( w = 0; w < nVars; w++ )
M[C[w][0]][C[w][1]] = M[C[w][1]][C[w][0]] = (i >> w) & 1;
while ( fChanges && !M[0][1] ) {
fChanges = 0;
for ( a = 0; a < nPis; a++ )
for ( b = 0; b < nPis; b++ )
if ( M[a][b] )
for ( w = 0; w < nPis; w++ )
if ( M[b][w] && !M[a][w] )
M[a][w] = 1, fChanges = 1;
}
if ( M[0][1] )
Abc_InfoSetBit(pTruth, i);
}
pFile = fopen( pFileName, "w" );
fprintf( pFile, "# Function with %d inputs generated by ABC on %s\n", nVars, Extra_TimeStamp() );
fprintf( pFile, ".model fun%d\n", nVars );
fprintf( pFile, ".inputs" );
nDigitsIn = Abc_Base10Log( nVars );
for ( i = 0; i < nVars; i++ )
fprintf( pFile, " i%0*d", nDigitsIn, i );
fprintf( pFile, "\n" );
fprintf( pFile, ".outputs f\n" );
fprintf( pFile, ".names" );
nDigitsIn = Abc_Base10Log( nVars );
for ( b = nVars-1; b >= 0; b-- )
fprintf( pFile, " i%0*d", nDigitsIn, b );
fprintf( pFile, " f\n" );
for ( i = 0; i < (1<<nVars); i++ )
if ( Abc_InfoHasBit(pTruth, i) )
{
for ( b = nVars-1; b >= 0; b-- )
fprintf( pFile, "%d", (i>>b)&1 );
fprintf( pFile, " 1\n" );
}
fprintf( pFile, ".end\n" );
fprintf( pFile, "\n" );
fclose( pFile );
ABC_FREE( pTruth );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

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

5328
src/base/abci/abcOrchestration.c Normal file
View File

File diff suppressed because it is too large Load Diff

13
src/base/abci/abcPrint.c
View File

@ -1199,6 +1199,17 @@ void Abc_NtkPrintSop( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames )
SeeAlso []
***********************************************************************/
char * Abc_NodeGetPrintName( Abc_Obj_t * pObj )
{
Abc_Obj_t * pFan, * pFanout = NULL; int k, nPos = 0;
if ( !Abc_ObjIsNode(pObj) )
return Abc_ObjName(pObj);
Abc_ObjForEachFanout( pObj, pFan, k ) {
if ( Abc_ObjIsPo(pFan) )
pFanout = pFan, nPos++;
}
return Abc_ObjName(nPos == 1 ? pFanout : pObj);
}
void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fVerbose )
{
Abc_Obj_t * pNode;
@ -1214,7 +1225,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListN
printf( "%2d : ", i );
Abc_NtkForEachNode( pNtk, pNode, k )
if ( (int)pNode->Level == i )
printf( " %s", Abc_ObjName(pNode) );
printf( " %s", Abc_NodeGetPrintName(pNode) );
printf( "\n" );
}
return;

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

@ -160,6 +160,8 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
word * pTruth;
abctime clk;
int i, nNodesSaved, nNodesAdded, Required;
if ( fUseZeros )
nMinSaved = 0;
p->nNodesConsidered++;

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 []

1
src/base/abci/module.make
View File

@ -41,6 +41,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcNtbdd.c \
src/base/abci/abcNpn.c \
src/base/abci/abcNpnSave.c \
src/base/abci/abcOrchestration.c \
src/base/abci/abcOdc.c \
src/base/abci/abcOrder.c \
src/base/abci/abcPart.c \

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;
@ -2449,7 +2449,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");
@ -2561,7 +2561,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

@ -1519,7 +1519,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;
}
@ -1869,7 +1869,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 );

8
src/base/io/ioWriteEqn.c
View File

@ -85,6 +85,10 @@ void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName )
SeeAlso []
***********************************************************************/
char * Io_NamePrepro( char * pName )
{
return strncmp(pName, "new_", 4) ? pName : pName + 4;
}
void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk )
{
Vec_Vec_t * vLevels;
@ -108,10 +112,10 @@ void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk )
Abc_NtkForEachNode( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
fprintf( pFile, "%s = ", Abc_ObjName(Abc_ObjFanout0(pNode)) );
fprintf( pFile, "%s = ", Io_NamePrepro( Abc_ObjName(Abc_ObjFanout0(pNode)) ) );
// set the input names
Abc_ObjForEachFanin( pNode, pFanin, k )
Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData = Abc_ObjName(pFanin);
Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData = Io_NamePrepro( Abc_ObjName(pFanin) );
// write the formula
Hop_ObjPrintEqn( pFile, (Hop_Obj_t *)pNode->pData, vLevels, 0 );
fprintf( pFile, ";\n" );

14
src/base/io/ioWriteVerilog.c
View File

@ -557,11 +557,18 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
}
else
{
Vec_Int_t * vMap = Vec_IntStartFull( 2*Abc_NtkObjNumMax(pNtk) );
//Vec_Int_t * vMap = Vec_IntStartFull( 2*Abc_NtkObjNumMax(pNtk) );
vLevels = Vec_VecAlloc( 10 );
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( Abc_ObjFaninNum(pObj) == 1 && Abc_ObjIsCo(Abc_ObjFanout0(Abc_ObjFanout0(pObj))) )
if ( Abc_ObjFaninNum(pObj) == 0 )
{
fprintf( pFile, " assign %s = ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
fprintf( pFile, "1\'b%d;\n", Abc_NodeIsConst1(pObj) );
continue;
}
/*
if ( Abc_ObjFaninNum(pObj) == 1 || Abc_ObjIsCo(Abc_ObjFanout0(Abc_ObjFanout0(pObj))) )
{
int iLit = Abc_Var2Lit( Abc_ObjId( Abc_ObjFanin0(Abc_ObjFanin0(pObj)) ), Abc_NodeIsInv(pObj) );
int iObj = Vec_IntEntry( vMap, iLit );
@ -574,6 +581,7 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
continue;
}
}
*/
pFunc = (Hop_Obj_t *)pObj->pData;
fprintf( pFile, " assign %s = ", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(pObj))) );
// set the input names
@ -595,7 +603,7 @@ void Io_WriteVerilogObjects( FILE * pFile, Abc_Ntk_t * pNtk, int fOnlyAnds )
ABC_FREE( Hop_IthVar((Hop_Man_t *)pNtk->pManFunc, k)->pData );
}
Vec_VecFree( vLevels );
Vec_IntFree( vMap );
//Vec_IntFree( vMap );
}
}

21
src/base/wlc/wlcBlast.c
View File

@ -575,6 +575,26 @@ void Wlc_BlastMultiplier( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA,
Wlc_BlastFullAdderCtrl( pNew, 1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], 0 );
//Vec_IntWriteEntry( vRes, nArgA + nArgB, Carry );
}
void Wlc_BlastMultiplierC( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vTemp, Vec_Int_t * vRes, int fSigned )
{
int * pRes, * pArgC, * pArgS, a, b, Carry = !fSigned; // change
assert( nArgA > 0 && nArgB > 0 );
assert( fSigned == 0 || fSigned == 1 );
Vec_IntFill( vRes, nArgA + nArgB, 0 );
pRes = Vec_IntArray( vRes );
Vec_IntFill( vTemp, 2 * nArgA, 1 ); // change
pArgC = Vec_IntArray( vTemp );
pArgS = pArgC + nArgA;
for ( b = 0; b < nArgB; b++ )
for ( a = 0; a < nArgA; a++ )
Wlc_BlastFullAdderCtrl( pNew, pArgA[a], pArgB[b], pArgS[a], pArgC[a],
&pArgC[a], a ? &pArgS[a-1] : &pRes[b], !(fSigned && ((a+1 == nArgA) ^ (b+1 == nArgB))) ); // change
pArgS[nArgA-1] = !fSigned; // change
for ( a = 0; a < nArgA; a++ )
Wlc_BlastFullAdderCtrl( pNew, 1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], 0 );
for ( b = 0; b < nArgA + nArgB; b++ ) // change
pRes[b] = Abc_LitNot(pRes[b]);
}
void Wlc_BlastDivider( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
{
int * pRes = Wlc_VecCopy( vRes, pNum, nNum );
@ -1817,6 +1837,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
Wlc_BlastMultiplier3( pNew, pArg0, pArg1, nRange0, nRange1, vRes, Wlc_ObjIsSignedFanin01(p, pObj), pPar->fCla, NULL );
else
Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
//Wlc_BlastMultiplierC( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
if ( nRange > Vec_IntSize(vRes) )
Vec_IntFillExtra( vRes, nRange, fSigned ? Vec_IntEntryLast(vRes) : 0 );
else

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

6
src/bdd/cudd/cuddBddIte.c
View File

@ -1203,8 +1203,8 @@ bddVarToCanonical(
unsigned int * topgp,
unsigned int * tophp)
{
register DdNode *F, *G, *H, *r, *f, *g, *h;
register unsigned int topf, topg, toph;
DdNode *F, *G, *H, *r, *f, *g, *h;
unsigned int topf, topg, toph;
DdNode *one = dd->one;
int comple, change;
@ -1305,7 +1305,7 @@ bddVarToCanonicalSimple(
unsigned int * topgp,
unsigned int * tophp)
{
register DdNode *r, *f, *g, *h;
DdNode *r, *f, *g, *h;
int comple, change;
f = *fp;

6
src/bdd/cudd/cuddCache.c
View File

@ -229,7 +229,7 @@ cuddCacheInsert(
{
int posn;
unsigned hash;
register DdCache *entry;
DdCache *entry;
ptruint uf, ug, uh;
ptruint ufc, ugc, uhc;
@ -283,7 +283,7 @@ cuddCacheInsert2(
{
int posn;
unsigned hash;
register DdCache *entry;
DdCache *entry;
hash = ddCHash2_(op,cuddF2L(f),cuddF2L(g));
// posn = ddCHash2(op,cuddF2L(f),cuddF2L(g),table->cacheShift);
@ -328,7 +328,7 @@ cuddCacheInsert1(
{
int posn;
unsigned hash;
register DdCache *entry;
DdCache *entry;
hash = ddCHash2_(op,cuddF2L(f),cuddF2L(f));
// posn = ddCHash2(op,cuddF2L(f),cuddF2L(f),table->cacheShift);

4
src/bdd/cudd/cuddSat.c
View File

@ -279,7 +279,7 @@ Cudd_LargestCube(
DdNode * f,
int * length)
{
register DdNode *F;
DdNode *F;
st__table *visited;
DdNode *sol;
cuddPathPair *rootPair;
@ -351,7 +351,7 @@ Cudd_ShortestLength(
DdNode * f,
int * weight)
{
register DdNode *F;
DdNode *F;
st__table *visited;
cuddPathPair *my_pair;
int complement, cost;

4
src/bdd/cudd/cuddSplit.c
View File

@ -638,8 +638,8 @@ bddAnnotateMintermCount(
{
DdNode *N,*Nv,*Nnv;
register double min_v,min_nv;
register double min_N;
double min_v,min_nv;
double min_N;
double *pmin;
double *dummy;

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/bdd/dsd/dsd.h
View File

@ -92,8 +92,8 @@ extern DdNode * Dsd_NodeReadSupp( Dsd_Node_t * p );
extern Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p );
extern Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i );
extern int Dsd_NodeReadDecsNum( Dsd_Node_t * p );
extern int Dsd_NodeReadMark( Dsd_Node_t * p );
extern void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark );
extern word Dsd_NodeReadMark( Dsd_Node_t * p );
extern void Dsd_NodeSetMark( Dsd_Node_t * p, word Mark );
extern DdManager * Dsd_ManagerReadDd( Dsd_Manager_t * pMan );
extern Dsd_Node_t * Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i );
extern Dsd_Node_t * Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i );

4
src/bdd/dsd/dsdApi.c
View File

@ -56,7 +56,7 @@ DdNode * Dsd_NodeReadSupp( Dsd_Node_t * p ) { return p->S; }
Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p ) { return p->pDecs; }
Dsd_Node_t * Dsd_NodeReadDec ( Dsd_Node_t * p, int i ) { return p->pDecs[i]; }
int Dsd_NodeReadDecsNum( Dsd_Node_t * p ) { return p->nDecs; }
int Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; }
word Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; }
/**Function*************************************************************
@ -74,7 +74,7 @@ int Dsd_NodeReadMark( Dsd_Node_t * p ) { return p->Mark; }
SeeAlso []
***********************************************************************/
void Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark; }
void Dsd_NodeSetMark( Dsd_Node_t * p, word Mark ){ p->Mark = Mark; }
/**Function*************************************************************

2
src/bdd/dsd/dsdInt.h
View File

@ -57,7 +57,7 @@ struct Dsd_Node_t_
DdNode * G; // function of the node
DdNode * S; // support of this function
Dsd_Node_t ** pDecs; // pointer to structures for formal inputs
int Mark; // the mark used by CASE 4 of disjoint decomposition
word Mark; // the mark used by CASE 4 of disjoint decomposition
short nDecs; // the number of formal inputs
short nVisits; // the counter of visits
};

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

91
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;
@ -156,9 +183,13 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
int fUnit = 0;
int fVerbose = 1;
int fVeryVerbose = 0;
SC_DontUse dont_use = {0};
dont_use.dont_use_list = ABC_ALLOC(char *, argc);
dont_use.size = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SGMdnuvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SGMXdnuvwh" ) ) != EOF )
{
switch ( c )
{
@ -195,6 +226,16 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nGatesMin < 0 )
goto usage;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by a string.\n" );
goto usage;
}
dont_use.dont_use_list[dont_use.size] = argv[globalUtilOptind];
dont_use.size++;
globalUtilOptind++;
break;
case 'd':
fDump ^= 1;
break;
@ -216,23 +257,29 @@ int Scl_CommandReadLib( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
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);
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);
}
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;
// get the input file name
pFileName = argv[globalUtilOptind];
if ( (pFile = fopen( pFileName, "rb" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
return 1;
}
fclose( pFile );
// read new library
pLib = Abc_SclReadLiberty( pFileName, fVerbose, fVeryVerbose );
if ( pLib == NULL )
{
fprintf( pAbc->Err, "Reading SCL library from file \"%s\" has failed. \n", pFileName );
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) );
@ -245,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;
@ -261,11 +308,12 @@ 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] <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 );
fprintf( pAbc->Err, "\t-M num : skip gate classes whose size is less than this [default = %d]\n", nGatesMin );
fprintf( pAbc->Err, "\t-X name : adds name to the list of cells ABC shouldn't use. Flag can be passed multiple times\n");
fprintf( pAbc->Err, "\t-d : toggle dumping the parsed library into file \"*_temp.lib\" [default = %s]\n", fDump? "yes": "no" );
fprintf( pAbc->Err, "\t-n : toggle replacing gate/pin names by short strings [default = %s]\n", fShortNames? "yes": "no" );
fprintf( pAbc->Err, "\t-u : toggle setting unit area for all cells [default = %s]\n", fUnit? "yes": "no" );
@ -273,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;
}
@ -1066,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) )
@ -1202,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) )

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

@ -59,6 +59,13 @@ typedef enum // -- timing sense, positive-, negative- or non-unate
sc_ts_Non,
} SC_TSense;
typedef struct SC_DontUse_ SC_DontUse;
struct SC_DontUse_
{
int size;
char ** dont_use_list;
};
typedef struct SC_Pair_ SC_Pair;
struct SC_Pair_
{
@ -734,13 +741,14 @@ static inline void Scl_LibHandleInputDriver2( SC_Cell * pCell, SC_PairI * pLoadI
}
/*=== sclLiberty.c ===============================================================*/
extern SC_Lib * Abc_SclReadLiberty( char * pFileName, int fVerbose, int fVeryVerbose );
extern SC_Lib * Abc_SclReadLiberty( char * pFileName, int fVerbose, int fVeryVerbose, SC_DontUse dont_use );
/*=== sclLibScl.c ===============================================================*/
extern SC_Lib * Abc_SclReadFromGenlib( void * pLib );
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 ///
////////////////////////////////////////////////////////////////////////

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

@ -17,6 +17,13 @@
Revision [$Id: sclLiberty.c,v 1.0 2012/08/24 00:00:00 alanmi Exp $]
***********************************************************************/
#include <string.h>
#ifdef _WIN32
#include <shlwapi.h>
#pragma comment(lib, "shlwapi.lib")
#else
#include <fnmatch.h>
#endif
#include "sclLib.h"
#include "misc/st/st.h"
@ -73,6 +80,14 @@ struct Scl_Tree_t_
Vec_Str_t * vBuffer; // temp string buffer
};
static inline int Scl_LibertyGlobMatch(const char * pattern, const char * string) {
#ifdef _WIN32
return PathMatchSpec(string, pattern);
#else
return fnmatch(pattern, string, 0) == 0;
#endif
}
static inline Scl_Item_t * Scl_LibertyRoot( Scl_Tree_t * p ) { return p->pItems; }
static inline Scl_Item_t * Scl_LibertyItem( Scl_Tree_t * p, long v ) { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v; }
static inline long Scl_LibertyCompare( Scl_Tree_t * p, Scl_Pair_t Pair, char * pStr ) { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ) || ((long)strlen(pStr) != Pair.End-Pair.Beg); }
@ -635,12 +650,20 @@ int Scl_LibertyReadCellIsFlop( Scl_Tree_t * p, Scl_Item_t * pCell )
return 1;
return 0;
}
int Scl_LibertyReadCellIsDontUse( Scl_Tree_t * p, Scl_Item_t * pCell )
int Scl_LibertyReadCellIsDontUse( Scl_Tree_t * p, Scl_Item_t * pCell, SC_DontUse dont_use )
{
Scl_Item_t * pAttr;
Scl_ItemForEachChild( p, pCell, pAttr )
{
if ( !Scl_LibertyCompare(p, pAttr->Key, "dont_use") )
return 1;
const char * cell_name = Scl_LibertyReadString(p, pCell->Head);
for (int i = 0; i < dont_use.size; i++) {
if (Scl_LibertyGlobMatch(dont_use.dont_use_list[i], cell_name)) {
return 1;
}
}
}
return 0;
}
char * Scl_LibertyReadCellArea( Scl_Tree_t * p, Scl_Item_t * pCell )
@ -703,7 +726,7 @@ long Scl_LibertyReadCellOutputNum( Scl_Tree_t * p, Scl_Item_t * pCell )
SeeAlso []
***********************************************************************/
Vec_Str_t * Scl_LibertyReadGenlibStr( Scl_Tree_t * p, int fVerbose )
Vec_Str_t * Scl_LibertyReadGenlibStr( Scl_Tree_t * p, int fVerbose, SC_DontUse dont_use )
{
Vec_Str_t * vStr;
Scl_Item_t * pCell, * pOutput, * pInput;
@ -718,7 +741,7 @@ Vec_Str_t * Scl_LibertyReadGenlibStr( Scl_Tree_t * p, int fVerbose )
if ( fVerbose ) printf( "Scl_LibertyReadGenlib() skipped sequential cell \"%s\".\n", Scl_LibertyReadString(p, pCell->Head) );
continue;
}
if ( Scl_LibertyReadCellIsDontUse(p, pCell) )
if ( Scl_LibertyReadCellIsDontUse(p, pCell, dont_use) )
{
if ( fVerbose ) printf( "Scl_LibertyReadGenlib() skipped cell \"%s\" due to dont_use attribute.\n", Scl_LibertyReadString(p, pCell->Head) );
continue;
@ -768,20 +791,6 @@ Vec_Str_t * Scl_LibertyReadGenlibStr( Scl_Tree_t * p, int fVerbose )
// printf( "%s", Vec_StrArray(vStr) );
return vStr;
}
Vec_Str_t * Scl_LibertyParseGenlibStr( char * pFileName, int fVerbose )
{
Scl_Tree_t * p;
Vec_Str_t * vStr;
p = Scl_LibertyParse( pFileName, fVerbose );
if ( p == NULL )
return NULL;
// Scl_LibertyRead( p, "temp_.lib" );
vStr = Scl_LibertyReadGenlibStr( p, fVerbose );
Scl_LibertyStop( p, fVerbose );
// Scl_LibertyStringDump( "test_genlib.lib", vStr );
return vStr;
}
/**Function*************************************************************
@ -858,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 )
@ -878,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 );
}
@ -1429,7 +1438,7 @@ Vec_Ptr_t * Scl_LibertyReadTemplates( Scl_Tree_t * p )
// Scl_LibertyPrintTemplates( vRes );
return vRes;
}
Vec_Str_t * Scl_LibertyReadSclStr( Scl_Tree_t * p, int fVerbose, int fVeryVerbose )
Vec_Str_t * Scl_LibertyReadSclStr( Scl_Tree_t * p, int fVerbose, int fVeryVerbose, SC_DontUse dont_use )
{
int fUseFirstTable = 0;
Vec_Str_t * vOut;
@ -1472,7 +1481,7 @@ Vec_Str_t * Scl_LibertyReadSclStr( Scl_Tree_t * p, int fVerbose, int fVeryVerbos
nSkipped[0]++;
continue;
}
if ( Scl_LibertyReadCellIsDontUse(p, pCell) )
if ( Scl_LibertyReadCellIsDontUse(p, pCell, dont_use) )
{
if ( fVeryVerbose ) printf( "Scl_LibertyReadGenlib() skipped cell \"%s\" due to dont_use attribute.\n", Scl_LibertyReadString(p, pCell->Head) );
nSkipped[3]++;
@ -1500,7 +1509,7 @@ Vec_Str_t * Scl_LibertyReadSclStr( Scl_Tree_t * p, int fVerbose, int fVeryVerbos
{
if ( Scl_LibertyReadCellIsFlop(p, pCell) )
continue;
if ( Scl_LibertyReadCellIsDontUse(p, pCell) )
if ( Scl_LibertyReadCellIsDontUse(p, pCell, dont_use) )
continue;
if ( Scl_LibertyReadCellIsThreeState(p, pCell) )
continue;
@ -1677,7 +1686,7 @@ Vec_Str_t * Scl_LibertyReadSclStr( Scl_Tree_t * p, int fVerbose, int fVeryVerbos
}
return vOut;
}
SC_Lib * Abc_SclReadLiberty( char * pFileName, int fVerbose, int fVeryVerbose )
SC_Lib * Abc_SclReadLiberty( char * pFileName, int fVerbose, int fVeryVerbose, SC_DontUse dont_use )
{
SC_Lib * pLib;
Scl_Tree_t * p;
@ -1687,7 +1696,7 @@ SC_Lib * Abc_SclReadLiberty( char * pFileName, int fVerbose, int fVeryVerbose )
return NULL;
// Scl_LibertyParseDump( p, "temp_.lib" );
// collect relevant data
vStr = Scl_LibertyReadSclStr( p, fVerbose, fVeryVerbose );
vStr = Scl_LibertyReadSclStr( p, fVerbose, fVeryVerbose, dont_use );
Scl_LibertyStop( p, fVeryVerbose );
if ( vStr == NULL )
return NULL;
@ -1725,7 +1734,8 @@ void Scl_LibertyTest()
if ( p == NULL )
return;
// Scl_LibertyParseDump( p, "temp_.lib" );
vStr = Scl_LibertyReadSclStr( p, fVerbose, fVeryVerbose );
SC_DontUse dont_use = {0};
vStr = Scl_LibertyReadSclStr( p, fVerbose, fVeryVerbose, dont_use);
Scl_LibertyStringDump( "test_scl.lib", vStr );
Vec_StrFree( vStr );
Scl_LibertyStop( p, fVerbose );

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

12
src/misc/bzlib/compress.c
View File

@ -190,15 +190,15 @@ void generateMTFValues ( EState* s )
zPend = 0;
}
{
register UChar rtmp;
register UChar* ryy_j;
register UChar rll_i;
UChar rtmp;
UChar* ryy_j;
UChar rll_i;
rtmp = yy[1];
yy[1] = yy[0];
ryy_j = &(yy[1]);
rll_i = ll_i;
while ( rll_i != rtmp ) {
register UChar rtmp2;
UChar rtmp2;
ryy_j++;
rtmp2 = rtmp;
rtmp = *ryy_j;
@ -360,8 +360,8 @@ void sendMTFValues ( EState* s )
if (nGroups == 6 && 50 == ge-gs+1) {
/*--- fast track the common case ---*/
register UInt32 cost01, cost23, cost45;
register UInt16 icv;
UInt32 cost01, cost23, cost45;
UInt16 icv;
cost01 = cost23 = cost45 = 0;
# define BZ_ITER(nn) \

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

@ -97,8 +97,8 @@ void Extra_UtilGetoptReset()
***********************************************************************/
int Extra_UtilGetopt( int argc, char *argv[], const char *optstring )
{
register int c;
register const char *place;
int c;
const char *place;
globalUtilOptarg = NULL;
@ -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

22
src/misc/util/abc_global.h
View File

@ -325,8 +325,8 @@ static inline int Abc_Var2Lit4( int Var, int Att ) { assert(!(Att >>
static inline int Abc_Lit2Var4( int Lit ) { assert(Lit >= 0); return Lit >> 4; }
static inline int Abc_Lit2Att4( int Lit ) { assert(Lit >= 0); return Lit & 15; }
// time counting
typedef ABC_INT64_T abctime;
// counting wall time
static inline abctime Abc_Clock()
{
#if defined(__APPLE__) && defined(__MACH__)
@ -335,6 +335,25 @@ static inline abctime Abc_Clock()
#define APPLE_MACH 0
#endif
#if (defined(LIN) || defined(LIN64)) && !APPLE_MACH && !defined(__MINGW32__) && !defined(__wasm)
struct timespec ts;
if ( clock_gettime(CLOCK_MONOTONIC, &ts) < 0 )
return (abctime)-1;
abctime res = ((abctime) ts.tv_sec) * CLOCKS_PER_SEC;
res += (((abctime) ts.tv_nsec) * CLOCKS_PER_SEC) / 1000000000;
return res;
#else
return (abctime) clock();
#endif
}
// counting thread time
static inline abctime Abc_ThreadClock()
{
#if defined(__APPLE__) && defined(__MACH__)
#define APPLE_MACH (__APPLE__ & __MACH__)
#else
#define APPLE_MACH 0
#endif
#if (defined(LIN) || defined(LIN64)) && !APPLE_MACH && !defined(__MINGW32__)
struct timespec ts;
if ( clock_gettime(CLOCK_THREAD_CPUTIME_ID, &ts) < 0 )
return (abctime)-1;
@ -346,7 +365,6 @@ static inline abctime Abc_Clock()
#endif
}
// misc printing procedures
enum Abc_VerbLevel
{

8
src/misc/zlib/crc32.c
View File

@ -269,8 +269,8 @@ unsigned long ZEXPORT crc32(unsigned long crc, const unsigned char FAR *buf, uIn
/* ========================================================================= */
local unsigned long crc32_little(unsigned long crc, const unsigned char FAR *buf, unsigned len)
{
register u4 c;
register const u4 FAR *buf4;
u4 c;
const u4 FAR *buf4;
c = (u4)crc;
c = ~c;
@ -306,8 +306,8 @@ local unsigned long crc32_little(unsigned long crc, const unsigned char FAR *buf
/* ========================================================================= */
local unsigned long crc32_big(unsigned long crc, const unsigned char FAR *buf, unsigned len)
{
register u4 c;
register const u4 FAR *buf4;
u4 c;
const u4 FAR *buf4;
c = REV((u4)crc);
c = ~c;

30
src/misc/zlib/deflate.c
View File

@ -1027,9 +1027,9 @@ local void lm_init (deflate_state *s)
local uInt longest_match(deflate_state *s, IPos cur_match)
{
unsigned chain_length = s->max_chain_length;/* max hash chain length */
register Bytef *scan = s->window + s->strstart; /* current string */
register Bytef *match; /* matched string */
register int len; /* length of current match */
Bytef *scan = s->window + s->strstart; /* current string */
Bytef *match; /* matched string */
int len; /* length of current match */
int best_len = s->prev_length; /* best match length so far */
int nice_match = s->nice_match; /* stop if match long enough */
IPos limit = s->strstart > (IPos)MAX_DIST(s) ?
@ -1044,13 +1044,13 @@ local uInt longest_match(deflate_state *s, IPos cur_match)
/* Compare two bytes at a time. Note: this is not always beneficial.
* Try with and without -DUNALIGNED_OK to check.
*/
register Bytef *strend = s->window + s->strstart + MAX_MATCH - 1;
register ush scan_start = *(ushf*)scan;
register ush scan_end = *(ushf*)(scan+best_len-1);
Bytef *strend = s->window + s->strstart + MAX_MATCH - 1;
ush scan_start = *(ushf*)scan;
ush scan_end = *(ushf*)(scan+best_len-1);
#else
register Bytef *strend = s->window + s->strstart + MAX_MATCH;
register Byte scan_end1 = scan[best_len-1];
register Byte scan_end = scan[best_len];
Bytef *strend = s->window + s->strstart + MAX_MATCH;
Byte scan_end1 = scan[best_len-1];
Byte scan_end = scan[best_len];
#endif
/* The code is optimized for HASH_BITS >= 8 and MAX_MATCH-2 multiple of 16.
@ -1173,10 +1173,10 @@ local uInt longest_match(deflate_state *s, IPos cur_match)
*/
local uInt longest_match(deflate_state *s, IPos cur_match)
{
register Bytef *scan = s->window + s->strstart; /* current string */
register Bytef *match; /* matched string */
register int len; /* length of current match */
register Bytef *strend = s->window + s->strstart + MAX_MATCH;
Bytef *scan = s->window + s->strstart; /* current string */
Bytef *match; /* matched string */
int len; /* length of current match */
Bytef *strend = s->window + s->strstart + MAX_MATCH;
/* The code is optimized for HASH_BITS >= 8 and MAX_MATCH-2 multiple of 16.
* It is easy to get rid of this optimization if necessary.
@ -1261,8 +1261,8 @@ local void check_match(deflate_state *s, IPos start, IPos match, int length)
*/
local void fill_window(deflate_state *s)
{
register unsigned n, m;
register Posf *p;
unsigned n, m;
Posf *p;
unsigned more; /* Amount of free space at the end of the window. */
uInt wsize = s->w_size;

2
src/misc/zlib/trees.c
View File

@ -1144,7 +1144,7 @@ local int detect_data_type(deflate_state *s)
*/
local unsigned bi_reverse(unsigned code, int len)
{
register unsigned res = 0;
unsigned res = 0;
do {
res |= code & 1;
code >>= 1, res <<= 1;

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

@ -87,6 +87,8 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
abctime clk = 0, clkStart;
int Counter = 0;
int nMffcSize;//, nMffcGains[MAX_VAL+1][MAX_VAL+1] = {{0}};
if ( pPars->fUseZeros )
pPars->nMinSaved = 0;
// prepare the library
Dar_LibPrepare( pPars->nSubgMax );
// create rewriting manager

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

2
src/proof/cec/cec.h
View File

@ -147,6 +147,8 @@ struct Cec_ParCor_t_
int nFrames; // the number of time frames
int nPrefix; // the number of time frames in the prefix
int nBTLimit; // conflict limit at a node
int nProcs; // the number of processes
int nPartSize; // the partition size
int nLevelMax; // (scorr only) the max number of levels
int nStepsMax; // (scorr only) the max number of induction steps
int nLimitMax; // (scorr only) stop after this many iterations if little or no improvement

57
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;
}
@ -1731,7 +1748,21 @@ Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
}
void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
{
int i, iObj, iPrev, Counter = 0;
int i = 0, iObj, iPrev, Counter = 0;
for ( iPrev = i, iObj = Gia_ObjNext(p, i); -1 < iObj; iObj = Gia_ObjNext(p, iPrev) )
{
Gia_Obj_t * pRepr = Gia_ObjReprObj(p, iObj);
assert( pRepr == Gia_ManConst0(p) );
if( !Gia_ObjFailed(p,iObj) && Abc_Lit2Var(Gia_ManObj(p,iObj)->Value) == Abc_Lit2Var(pRepr->Value) )
{
iPrev = iObj;
continue;
}
Gia_ObjSetRepr( p, iObj, GIA_VOID );
Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
Gia_ObjSetNext( p, iObj, 0 );
Counter++;
}
Gia_ManForEachClass( p, i )
{
for ( iPrev = i, iObj = Gia_ObjNext(p, i); -1 < iObj; iObj = Gia_ObjNext(p, iPrev) )
@ -1882,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/cec/cecSplit.c
View File

@ -705,7 +705,7 @@ finish:
// wait till threads finish
for ( i = 0; i < nProcs; i++ )
if ( ThData[i].fWorking )
i = 0;
i = -1;
// stop threads
for ( i = 0; i < nProcs; i++ )
{

6
src/proof/fra/fraSim.c
View File

@ -958,6 +958,12 @@ void Fra_SmlPrintOutputs( Fra_Sml_t * p, int nPatterns )
int i, k;
for ( k = 0; k < nPatterns; k++ )
{
Aig_ManForEachCi( p->pAig, pObj, i )
{
pSims = Fra_ObjSim( p, pObj->Id );
printf( "%d", Abc_InfoHasBit( pSims, k ) );
}
printf( " " ); ;
Aig_ManForEachCo( p->pAig, pObj, i )
{
pSims = Fra_ObjSim( p, pObj->Id );

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

1
src/proof/ssw/ssw.h
View File

@ -42,6 +42,7 @@ struct Ssw_Pars_t_
{
int nPartSize; // size of the partition
int nOverSize; // size of the overlap between partitions
int nProcs; // the number of processors
int nFramesK; // the induction depth
int nFramesAddSim; // the number of additional frames to simulate
int fConstrs; // treat the last nConstrs POs as seq constraints

289
src/proof/ssw/sswPart.c
View File

@ -20,10 +20,23 @@
#include "sswInt.h"
#include "aig/ioa/ioa.h"
#include "aig/gia/giaAig.h"
#include "proof/cec/cec.h"
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#endif
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@ -32,6 +45,141 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performing SAT sweeping for the array of AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_SignalCorrespondenceArray1( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
{
Gia_Man_t * pGia; int i;
Cec_ParCor_t CorPars, * pCorPars = &CorPars;
Cec_ManCorSetDefaultParams( pCorPars );
pCorPars->nBTLimit = pPars->nBTLimit;
pCorPars->fVerbose = pPars->fVerbose;
pCorPars->fUseCSat = 1;
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
if ( Gia_ManPiNum(pGia) > 0 )
Cec_ManLSCorrespondenceClasses( pGia, pCorPars );
}
/**Function*************************************************************
Synopsis [Performing SAT sweeping for the array of AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#ifndef ABC_USE_PTHREADS
void Ssw_SignalCorrespondenceArray( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
{
Ssw_SignalCorrespondenceArray1( vGias, pPars );
}
#else // pthreads are used
#define PAR_THR_MAX 100
typedef struct Par_ScorrThData_t_
{
Cec_ParCor_t CorPars;
Gia_Man_t * p;
int * pMap;
int iThread;
int nTimeOut;
int fWorking;
} Par_ScorrThData_t;
void * Ssw_GiaWorkerThread( void * pArg )
{
Par_ScorrThData_t * pThData = (Par_ScorrThData_t *)pArg;
volatile int * pPlace = &pThData->fWorking;
while ( 1 )
{
while ( *pPlace == 0 );
assert( pThData->fWorking );
if ( pThData->p == NULL )
{
pthread_exit( NULL );
assert( 0 );
return NULL;
}
Cec_ManLSCorrespondenceClasses( pThData->p, &pThData->CorPars );
pThData->fWorking = 0;
}
assert( 0 );
return NULL;
}
void Ssw_SignalCorrespondenceArray( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
{
//abctime clkTotal = Abc_Clock();
Par_ScorrThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
int i, status, nProcs = pPars->nProcs;
Vec_Ptr_t * vStack;
Cec_ParCor_t CorPars, * pCorPars = &CorPars;
Cec_ManCorSetDefaultParams( pCorPars );
if ( pPars->fVerbose )
printf( "Running concurrent &scorr with %d processes.\n", nProcs );
fflush( stdout );
if ( pPars->nProcs < 2 )
return Ssw_SignalCorrespondenceArray1( vGias, pPars );
// subtract manager thread
nProcs--;
assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
// start threads
for ( i = 0; i < nProcs; i++ )
{
ThData[i].CorPars = *pCorPars;
ThData[i].iThread = i;
//ThData[i].nTimeOut = pPars->nTimeOut;
ThData[i].fWorking = 0;
status = pthread_create( WorkerThread + i, NULL, Ssw_GiaWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
}
// look at the threads
vStack = Vec_PtrDup( vGias );
while ( Vec_PtrSize(vStack) > 0 )
{
for ( i = 0; i < nProcs; i++ )
{
if ( ThData[i].fWorking )
continue;
ThData[i].p = (Gia_Man_t*)Vec_PtrPop( vStack );
ThData[i].fWorking = 1;
break;
}
}
Vec_PtrFree( vStack );
// wait till threads finish
for ( i = 0; i < nProcs; i++ )
if ( ThData[i].fWorking )
i = -1;
// stop threads
for ( i = 0; i < nProcs; i++ )
{
assert( !ThData[i].fWorking );
// stop
ThData[i].p = NULL;
ThData[i].fWorking = 1;
}
}
#endif // pthreads are used
/**Function*************************************************************
Synopsis [Performs partitioned sequential SAT sweeping.]
@ -45,7 +193,7 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
int fPrintParts = 0;
int fPrintParts = 1;
char Buffer[100];
Aig_Man_t * pTemp, * pNew;
Vec_Ptr_t * vResult;
@ -132,6 +280,143 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
}
/**Function*************************************************************
Synopsis [Performs partitioned sequential SAT sweeping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondencePart2( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
int fPrintParts = 1;
//char Buffer[100];
Aig_Man_t * pTemp, * pNew;
Vec_Ptr_t * vAigs;
Vec_Ptr_t * vGias;
Vec_Ptr_t * vMaps;
Vec_Ptr_t * vResult;
Vec_Int_t * vPart;
int * pMapBack = NULL;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
abctime clk = Abc_Clock();
if ( pPars->fConstrs )
{
Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
return NULL;
}
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
// generate partitions
if ( pAig->vClockDoms )
{
// divide large clock domains into separate partitions
vResult = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
{
if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
else
Vec_PtrPush( vResult, Vec_IntDup(vPart) );
}
}
else
vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
// collect partitions
vAigs = Vec_PtrAlloc( 100 );
vGias = Vec_PtrAlloc( 100 );
vMaps = Vec_PtrAlloc( 100 );
if ( fPrintParts )
Abc_Print( 1, "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
Aig_ManSetRegNum( pTemp, pTemp->nRegs );
Vec_PtrPush( vAigs, pTemp );
Vec_PtrPush( vGias, Gia_ManFromAigSimple(pTemp) );
Vec_PtrPush( vMaps, pMapBack );
//sprintf( Buffer, "part%03d.aig", i );
//Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
if ( fPrintParts )
Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
}
// solve partitions
Ssw_SignalCorrespondenceArray( vGias, pPars );
// collect the results
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
int * pMapBack = (int *)Vec_PtrEntry( vMaps, i );
Gia_Man_t * pGia = (Gia_Man_t *)Vec_PtrEntry( vGias, i );
Aig_Man_t * pTemp2 = Gia_ManToAigSimple( pGia );
pTemp = (Aig_Man_t *)Vec_PtrEntry( vAigs, i );
Gia_ManReprToAigRepr2( pTemp2, pGia );
// remap back
nClasses = Aig_TransferMappedClasses( pAig, pTemp2, pMapBack );
if ( fVerbose )
Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), 0, 0, Aig_ManNodeNum(pTemp), 0, nClasses );
Aig_ManStop( pTemp );
Aig_ManStop( pTemp2 );
Gia_ManStop( pGia );
ABC_FREE( pMapBack );
}
Vec_PtrFree( vAigs );
Vec_PtrFree( vGias );
Vec_PtrFree( vMaps );
// remap the AIG
pNew = Aig_ManDupRepr( pAig, 0 );
Aig_ManSeqCleanup( pNew );
// Aig_ManPrintStats( pAig );
// Aig_ManPrintStats( pNew );
Vec_VecFree( (Vec_Vec_t *)vResult );
pPars->nPartSize = nPartSize;
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
ABC_PRT( "Total time", Abc_Clock() - clk );
}
return pNew;
}
void Gia_ManRestoreNodeMapping( Aig_Man_t * pAig, Gia_Man_t * pGia )
{
Aig_Obj_t * pObjAig; int i;
assert( Gia_ManObjNum(pGia) == Aig_ManObjNum(pAig) );
Aig_ManForEachObj( pAig, pObjAig, i )
pObjAig->iData = Abc_Var2Lit(i, 0);
}
Gia_Man_t * Gia_SignalCorrespondencePart( Gia_Man_t * p, Cec_ParCor_t * pPars )
{
Gia_Man_t * pRes = NULL;
Aig_Man_t * pNew = NULL;
Aig_Man_t * pAig = Gia_ManToAigSimple(p);
Ssw_Pars_t SswPars, * pSswPars = &SswPars;
assert( pPars->nProcs > 0 );
assert( pPars->nPartSize > 0 );
Ssw_ManSetDefaultParams( pSswPars );
pSswPars->nBTLimit = pPars->nBTLimit;
pSswPars->nProcs = pPars->nProcs;
pSswPars->nPartSize = pPars->nPartSize;
pSswPars->fVerbose = pPars->fVerbose;
pNew = Ssw_SignalCorrespondencePart2( pAig, pSswPars );
Gia_ManRestoreNodeMapping( pAig, p );
Gia_ManReprFromAigRepr2( pAig, p );
pRes = Gia_ManFromAigSimple(pNew);
Aig_ManStop( pNew );
Aig_ManStop( pAig );
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

16
src/sat/bmc/bmcMaj.c
View File

@ -1637,22 +1637,6 @@ Vec_Int_t * Exa4_ManSolve( char * pFileNameIn, char * pFileNameOut, int TimeOut,
char * pKissat = "kissat";
#endif
char Command[1000], * pCommand = (char *)&Command;
{
FILE * pFile = fopen( pKissat, "rb" );
if ( pFile == NULL )
{
printf( "Cannot find the Kissat binary \"%s\".\n", pKissat );
pKissat = "./kissat";
pFile = fopen( pKissat, "rb" );
if ( pFile == NULL )
{
printf( "Cannot find the Kissat binary \"%s\".\n", pKissat );
return NULL;
}
fclose( pFile );
}
fclose( pFile );
}
if ( TimeOut )
sprintf( pCommand, "%s --time=%d %s %s > %s", pKissat, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
else

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

2
src/sat/cnf/cnf.h
View File

@ -154,6 +154,8 @@ extern void Cnf_ManStop( Cnf_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals );
extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p );
extern Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit );
extern Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips );

49
src/sat/cnf/cnfMan.c
View File

@ -103,10 +103,8 @@ void Cnf_ManStop( Cnf_Man_t * p )
***********************************************************************/
Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
{
Vec_Int_t * vCiIds;
Aig_Obj_t * pObj;
int i;
vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
Aig_Obj_t * pObj; int i;
Vec_Int_t * vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
Aig_ManForEachCi( p, pObj, i )
Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
return vCiIds;
@ -126,9 +124,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals )
{
Cnf_Dat_t * pCnf;
int i;
pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->pMan = pAig;
pCnf->nVars = nVars;
pCnf->nClauses = nClauses;
@ -136,10 +132,8 @@ Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiter
pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(pAig) );
// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
pCnf->pVarNums[i] = -1;
if ( pCnf->pVarNums )
pCnf->pVarNums = ABC_FALLOC( int, Aig_ManObjNumMax(pAig) );
return pCnf;
}
@ -160,11 +154,44 @@ Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p )
int i;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
if ( p->pVarNums )
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
return pCnf;
}
Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit )
{
Cnf_Dat_t * pCnf;
int i;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+1, p->nLiterals+1 );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
if ( pCnf->pVarNums )
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
pCnf->pClauses[p->nClauses] = pCnf->pClauses[0] + p->nLiterals;
pCnf->pClauses[p->nClauses][0] = Lit;
assert( pCnf->pClauses[p->nClauses+1] == pCnf->pClauses[0] + p->nLiterals+1 );
return pCnf;
}
Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits )
{
Cnf_Dat_t * pCnf;
int i, iLit;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+Vec_IntSize(vLits), p->nLiterals+Vec_IntSize(vLits) );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
if ( pCnf->pVarNums )
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
Vec_IntForEachEntry( vLits, iLit, i ) {
pCnf->pClauses[p->nClauses+i] = pCnf->pClauses[0] + p->nLiterals+i;
pCnf->pClauses[p->nClauses+i][0] = iLit;
}
assert( pCnf->pClauses[p->nClauses+Vec_IntSize(vLits)] == pCnf->pClauses[0] + p->nLiterals+Vec_IntSize(vLits) );
return pCnf;
}
/**Function*************************************************************

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

@ -9,7 +9,7 @@
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
@ -21,57 +21,260 @@
#include "cnf.h"
#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
#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>
#endif
#endif
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Vec_Int_t *Exa4_ManParse(char *pFileName);
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Synopsis [Solving problems using one core.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
Vec_Int_t *Cnf_RunSolverOnce(int Id, int Rand, int TimeOut, int fVerbose)
{
Aig_Obj_t * pLeaf;
Dar_Cut_t * pCutBest;
int aArea, i;
if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
return 0;
assert( Aig_ObjIsAnd(pObj) );
// collect the node first to derive pre-order
if ( vMapped )
Vec_PtrPush( vMapped, pObj );
// visit the transitive fanin of the selected cut
if ( pObj->fMarkB )
int fVerboseSolver = 0;
Vec_Int_t *vRes = NULL;
abctime clkTotal = Abc_Clock();
char FileNameIn[100], FileNameOut[100];
sprintf(FileNameIn, "%02d.cnf", Id);
sprintf(FileNameOut, "%02d.txt", Id);
#ifdef _WIN32
char *pKissat = "kissat.exe";
#else
char *pKissat = "kissat";
#endif
char Command[1000], *pCommand = (char *)&Command;
if (TimeOut)
sprintf(pCommand, "%s --seed=%d --time=%d %s %s > %s", pKissat, Rand, TimeOut, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
else
sprintf(pCommand, "%s --seed=%d %s %s > %s", pKissat, Rand, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
//printf( "Thread command: %s\n", pCommand);
FILE * pFile = fopen(FileNameIn, "rb");
if ( pFile != NULL ) {
fclose( pFile );
if (system(pCommand) == -1) {
fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand);
return 0;
}
vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here
}
if (fVerbose) {
double SolvingTime = ((double)(Abc_Clock() - clkTotal))/((double)CLOCKS_PER_SEC);
if (vRes)
printf("Problem %2d has a solution. ", Id);
else if (vRes == NULL && (TimeOut == 0 || SolvingTime < (double)TimeOut))
printf("Problem %2d has no solution. ", Id);
else if (vRes == NULL)
printf("Problem %2d has no solution or timed out after %d sec. ", Id, TimeOut);
Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal );
}
else if (vRes) {
printf("Problem %2d has a solution. ", Id);
Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal );
printf("(Currently waiting for %d sec for other threads to finish.)\n", TimeOut);
}
return vRes;
}
Vec_Int_t * Cnf_RunSolverArray(int nProcs, int TimeOut, int fVerbose)
{
Vec_Int_t *vRes = NULL; int i;
for ( i = 0; i < nProcs; i++ )
if ((vRes = Cnf_RunSolverOnce(i, 0, TimeOut, fVerbose)))
break;
return vRes;
}
/**Function*************************************************************
Synopsis [Solving problems using many cores.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#ifndef ABC_USE_PTHREADS
Vec_Int_t *Cnf_RunSolver(int nProcs, int TimeOut, int fVerbose)
{
return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose);
}
#else // pthreads are used
#define PAR_THR_MAX 100
typedef struct Cnf_ThData_t_
{
Vec_Int_t *vRes;
int Index;
int Rand;
int nTimeOut;
int fWorking;
int fVerbose;
} Cnf_ThData_t;
void *Cnf_WorkerThread(void *pArg)
{
Cnf_ThData_t *pThData = (Cnf_ThData_t *)pArg;
volatile int *pPlace = &pThData->fWorking;
while (1)
{
Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
Aig_ObjCollectSuper( pObj, vSuper );
while (*pPlace == 0)
;
assert(pThData->fWorking);
if (pThData->Index == -1)
{
pthread_exit(NULL);
assert(0);
return NULL;
}
pThData->vRes = Cnf_RunSolverOnce(pThData->Index, pThData->Rand, pThData->nTimeOut, pThData->fVerbose);
pThData->fWorking = 0;
}
assert(0);
return NULL;
}
Vec_Int_t *Cnf_RunSolver(int nProcs, int TimeOut, int fVerbose)
{
Vec_Int_t *vRes = NULL;
Cnf_ThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
int i, k, status;
if (fVerbose)
printf("Running concurrent solving with %d processes.\n", nProcs);
fflush(stdout);
if (nProcs < 2)
return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose);
// subtract manager thread
// nProcs--;
assert(nProcs >= 1 && nProcs <= PAR_THR_MAX);
// start threads
for (i = 0; i < nProcs; i++)
{
ThData[i].vRes = NULL;
ThData[i].Index = -1;
ThData[i].Rand = Abc_Random(0) % 0x1000000;
ThData[i].nTimeOut = TimeOut;
ThData[i].fWorking = 0;
ThData[i].fVerbose = fVerbose;
status = pthread_create(WorkerThread + i, NULL, Cnf_WorkerThread, (void *)(ThData + i));
assert(status == 0);
}
// look at the threads
for (k = 0; k < nProcs;)
{
for (i = 0; i < nProcs; i++)
{
if (ThData[i].fWorking)
continue;
if (ThData[i].vRes)
{
k = nProcs;
break;
}
ThData[i].Index = k++;
ThData[i].fWorking = 1;
break;
}
}
// wait till threads finish
for (i = 0; i < nProcs; i++)
if (ThData[i].fWorking)
i = -1;
// stop threads
for (i = 0; i < nProcs; i++)
{
assert(!ThData[i].fWorking);
if (ThData[i].vRes && vRes == NULL)
{
vRes = ThData[i].vRes;
ThData[i].vRes = NULL;
}
Vec_IntFreeP(&ThData[i].vRes);
// stop
ThData[i].Index = -1;
ThData[i].fWorking = 1;
}
return vRes;
}
#endif // pthreads are used
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped)
{
Aig_Obj_t *pLeaf;
Dar_Cut_t *pCutBest;
int aArea, i;
if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj))
return 0;
assert(Aig_ObjIsAnd(pObj));
// collect the node first to derive pre-order
if (vMapped)
Vec_PtrPush(vMapped, pObj);
// visit the transitive fanin of the selected cut
if (pObj->fMarkB)
{
Vec_Ptr_t *vSuper = Vec_PtrAlloc(100);
Aig_ObjCollectSuper(pObj, vSuper);
aArea = Vec_PtrSize(vSuper) + 1;
Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped );
Vec_PtrFree( vSuper );
Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i)
aArea += Aig_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped);
Vec_PtrFree(vSuper);
////////////////////////////
pObj->fMarkB = 1;
}
else
{
pCutBest = Dar_ObjBestCut( pObj );
aArea = Cnf_CutSopCost( p, pCutBest );
Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
pCutBest = Dar_ObjBestCut(pObj);
aArea = Cnf_CutSopCost(p, pCutBest);
Dar_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i)
aArea += Aig_ManScanMapping_rec(p, pLeaf, vMapped);
}
return aArea;
}
@ -81,28 +284,28 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
Vec_Ptr_t *Aig_ManScanMapping(Cnf_Man_t *p, int fCollect)
{
Vec_Ptr_t * vMapped = NULL;
Aig_Obj_t * pObj;
Vec_Ptr_t *vMapped = NULL;
Aig_Obj_t *pObj;
int i;
// clean all references
Aig_ManForEachObj( p->pManAig, pObj, i )
Aig_ManForEachObj(p->pManAig, pObj, i)
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
if (fCollect)
vMapped = Vec_PtrAlloc(1000);
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
Aig_ManForEachCo( p->pManAig, pObj, i )
p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
Aig_ManForEachCo(p->pManAig, pObj, i)
p->aArea += Aig_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped);
// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
return vMapped;
}
@ -111,48 +314,48 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped, int fPreorder )
int Cnf_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped, int fPreorder)
{
Aig_Obj_t * pLeaf;
Cnf_Cut_t * pCutBest;
Aig_Obj_t *pLeaf;
Cnf_Cut_t *pCutBest;
int aArea, i;
if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj))
return 0;
assert( Aig_ObjIsAnd(pObj) );
assert( pObj->pData != NULL );
assert(Aig_ObjIsAnd(pObj));
assert(pObj->pData != NULL);
// add the node to the mapping
if ( vMapped && fPreorder )
Vec_PtrPush( vMapped, pObj );
if (vMapped && fPreorder)
Vec_PtrPush(vMapped, pObj);
// visit the transitive fanin of the selected cut
if ( pObj->fMarkB )
if (pObj->fMarkB)
{
Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
Aig_ObjCollectSuper( pObj, vSuper );
Vec_Ptr_t *vSuper = Vec_PtrAlloc(100);
Aig_ObjCollectSuper(pObj, vSuper);
aArea = Vec_PtrSize(vSuper) + 1;
Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder );
Vec_PtrFree( vSuper );
Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i)
aArea += Cnf_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped, fPreorder);
Vec_PtrFree(vSuper);
////////////////////////////
pObj->fMarkB = 1;
}
else
{
pCutBest = (Cnf_Cut_t *)pObj->pData;
// assert( pCutBest->nFanins > 0 );
assert( pCutBest->Cost < 127 );
// assert( pCutBest->nFanins > 0 );
assert(pCutBest->Cost < 127);
aArea = pCutBest->Cost;
Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped, fPreorder );
Cnf_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i)
aArea += Cnf_ManScanMapping_rec(p, pLeaf, vMapped, fPreorder);
}
// add the node to the mapping
if ( vMapped && !fPreorder )
Vec_PtrPush( vMapped, pObj );
if (vMapped && !fPreorder)
Vec_PtrPush(vMapped, pObj);
return aArea;
}
@ -161,28 +364,28 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
Vec_Ptr_t *Cnf_ManScanMapping(Cnf_Man_t *p, int fCollect, int fPreorder)
{
Vec_Ptr_t * vMapped = NULL;
Aig_Obj_t * pObj;
Vec_Ptr_t *vMapped = NULL;
Aig_Obj_t *pObj;
int i;
// clean all references
Aig_ManForEachObj( p->pManAig, pObj, i )
Aig_ManForEachObj(p->pManAig, pObj, i)
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
if (fCollect)
vMapped = Vec_PtrAlloc(1000);
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
Aig_ManForEachCo( p->pManAig, pObj, i )
p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
Aig_ManForEachCo(p->pManAig, pObj, i)
p->aArea += Cnf_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped, fPreorder);
// printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
return vMapped;
}
@ -191,20 +394,20 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
Synopsis [Returns the array of CI IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Vec_Int_t *Cnf_DataCollectCiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
{
Vec_Int_t * vCiIds;
Aig_Obj_t * pObj;
Vec_Int_t *vCiIds;
Aig_Obj_t *pObj;
int i;
vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
Aig_ManForEachCi( p, pObj, i )
Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
vCiIds = Vec_IntAlloc(Aig_ManCiNum(p));
Aig_ManForEachCi(p, pObj, i)
Vec_IntPush(vCiIds, pCnf->pVarNums[pObj->Id]);
return vCiIds;
}
@ -213,20 +416,20 @@ Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Synopsis [Returns the array of CI IDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Vec_Int_t *Cnf_DataCollectCoSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
{
Vec_Int_t * vCoIds;
Aig_Obj_t * pObj;
Vec_Int_t *vCoIds;
Aig_Obj_t *pObj;
int i;
vCoIds = Vec_IntAlloc( Aig_ManCoNum(p) );
Aig_ManForEachCo( p, pObj, i )
Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] );
vCoIds = Vec_IntAlloc(Aig_ManCoNum(p));
Aig_ManForEachCo(p, pObj, i)
Vec_IntPush(vCoIds, pCnf->pVarNums[pObj->Id]);
return vCoIds;
}
@ -235,58 +438,58 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
unsigned char *Cnf_DataDeriveLitPolarities(Cnf_Dat_t *p)
{
int i, c, iClaBeg, iClaEnd, * pLit;
unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses );
for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ )
int i, c, iClaBeg, iClaEnd, *pLit;
unsigned *pPols0 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
unsigned *pPols1 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
unsigned char *pPres = ABC_CALLOC(unsigned char, p->nClauses);
for (i = 0; i < Aig_ManObjNumMax(p->pMan); i++)
{
if ( p->pObj2Count[i] == 0 )
if (p->pObj2Count[i] == 0)
continue;
iClaBeg = p->pObj2Clause[i];
iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i];
// go through the negative polarity clauses
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
if ( Abc_LitIsCompl(p->pClauses[c][0]) )
pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
for (c = iClaBeg; c < iClaEnd; c++)
for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
if (Abc_LitIsCompl(p->pClauses[c][0]))
pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
else
pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
// record these clauses
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
if ( Abc_LitIsCompl(p->pClauses[c][0]) )
pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
for (c = iClaBeg; c < iClaEnd; c++)
for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
if (Abc_LitIsCompl(p->pClauses[c][0]))
pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
else
pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
// clean negative polarity
for ( c = iClaBeg; c < iClaEnd; c++ )
for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
for (c = iClaBeg; c < iClaEnd; c++)
for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0;
}
ABC_FREE( pPols0 );
ABC_FREE( pPols1 );
/*
// for ( c = 0; c < p->nClauses; c++ )
for ( c = 0; c < 100; c++ )
{
printf( "Clause %6d : ", c );
for ( i = 0; i < 4; i++ )
printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
printf( " " );
for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
printf( "%6d ", *pLit );
printf( "\n" );
}
*/
ABC_FREE(pPols0);
ABC_FREE(pPols1);
/*
// for ( c = 0; c < p->nClauses; c++ )
for ( c = 0; c < 100; c++ )
{
printf( "Clause %6d : ", c );
for ( i = 0; i < 4; i++ )
printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
printf( " " );
for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
printf( "%6d ", *pLit );
printf( "\n" );
}
*/
return pPres;
}
@ -295,96 +498,96 @@ unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DataReadFromFile( char * pFileName )
Cnf_Dat_t *Cnf_DataReadFromFile(char *pFileName)
{
int MaxLine = 1000000;
int Var, Lit, nVars = -1, nClas = -1, i, Entry, iLine = 0;
Cnf_Dat_t * pCnf = NULL;
Vec_Int_t * vClas = NULL;
Vec_Int_t * vLits = NULL;
char * pBuffer, * pToken;
FILE * pFile = fopen( pFileName, "rb" );
if ( pFile == NULL )
Cnf_Dat_t *pCnf = NULL;
Vec_Int_t *vClas = NULL;
Vec_Int_t *vLits = NULL;
char *pBuffer, *pToken;
FILE *pFile = fopen(pFileName, "rb");
if (pFile == NULL)
{
printf( "Cannot open file \"%s\" for writing.\n", pFileName );
printf("Cannot open file \"%s\" for writing.\n", pFileName);
return NULL;
}
pBuffer = ABC_ALLOC( char, MaxLine );
while ( fgets(pBuffer, MaxLine, pFile) != NULL )
pBuffer = ABC_ALLOC(char, MaxLine);
while (fgets(pBuffer, MaxLine, pFile) != NULL)
{
iLine++;
if ( pBuffer[0] == 'c' )
if (pBuffer[0] == 'c')
continue;
if ( pBuffer[0] == 'p' )
if (pBuffer[0] == 'p')
{
pToken = strtok( pBuffer+1, " \t" );
if ( strcmp(pToken, "cnf") )
pToken = strtok(pBuffer + 1, " \t");
if (strcmp(pToken, "cnf"))
{
printf( "Incorrect input file.\n" );
printf("Incorrect input file.\n");
goto finish;
}
pToken = strtok( NULL, " \t" );
nVars = atoi( pToken );
pToken = strtok( NULL, " \t" );
nClas = atoi( pToken );
if ( nVars <= 0 || nClas <= 0 )
pToken = strtok(NULL, " \t");
nVars = atoi(pToken);
pToken = strtok(NULL, " \t");
nClas = atoi(pToken);
if (nVars <= 0 || nClas <= 0)
{
printf( "Incorrect parameters.\n" );
printf("Incorrect parameters.\n");
goto finish;
}
// temp storage
vClas = Vec_IntAlloc( nClas+1 );
vLits = Vec_IntAlloc( nClas*8 );
vClas = Vec_IntAlloc(nClas + 1);
vLits = Vec_IntAlloc(nClas * 8);
continue;
}
pToken = strtok( pBuffer, " \t\r\n" );
if ( pToken == NULL )
pToken = strtok(pBuffer, " \t\r\n");
if (pToken == NULL)
continue;
Vec_IntPush( vClas, Vec_IntSize(vLits) );
while ( pToken )
Vec_IntPush(vClas, Vec_IntSize(vLits));
while (pToken)
{
Var = atoi( pToken );
if ( Var == 0 )
Var = atoi(pToken);
if (Var == 0)
break;
Lit = (Var > 0) ? Abc_Var2Lit(Var-1, 0) : Abc_Var2Lit(-Var-1, 1);
if ( Lit >= 2*nVars )
Lit = (Var > 0) ? Abc_Var2Lit(Var - 1, 0) : Abc_Var2Lit(-Var - 1, 1);
if (Lit >= 2 * nVars)
{
printf( "Literal %d is out-of-bound for %d variables.\n", Lit, nVars );
printf("Literal %d is out-of-bound for %d variables.\n", Lit, nVars);
goto finish;
}
Vec_IntPush( vLits, Lit );
pToken = strtok( NULL, " \t\r\n" );
Vec_IntPush(vLits, Lit);
pToken = strtok(NULL, " \t\r\n");
}
if ( Var != 0 )
if (Var != 0)
{
printf( "There is no zero-terminator in line %d.\n", iLine );
printf("There is no zero-terminator in line %d.\n", iLine);
goto finish;
}
}
// finalize
if ( Vec_IntSize(vClas) != nClas )
printf( "Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
if (Vec_IntSize(vClas) != nClas)
printf("Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas);
Vec_IntPush(vClas, Vec_IntSize(vLits));
// create
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->nVars = nVars;
pCnf->nClauses = Vec_IntSize(vClas)-1;
pCnf = ABC_CALLOC(Cnf_Dat_t, 1);
pCnf->nVars = nVars;
pCnf->nClauses = Vec_IntSize(vClas) - 1;
pCnf->nLiterals = Vec_IntSize(vLits);
pCnf->pClauses = ABC_ALLOC( int *, Vec_IntSize(vClas) );
pCnf->pClauses = ABC_ALLOC(int *, Vec_IntSize(vClas));
pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
Vec_IntForEachEntry( vClas, Entry, i )
Vec_IntForEachEntry(vClas, Entry, i)
pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
finish:
fclose( pFile );
Vec_IntFreeP( &vClas );
Vec_IntFreeP( &vLits );
ABC_FREE( pBuffer );
fclose(pFile);
Vec_IntFreeP(&vClas);
Vec_IntFreeP(&vLits);
ABC_FREE(pBuffer);
return pCnf;
}
@ -393,87 +596,224 @@ finish:
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int ** ppModel, int nPis )
int Cnf_DataSolveFromFile(char *pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int **ppModel, int nPis)
{
abctime clk = Abc_Clock();
Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
sat_solver * pSat;
Cnf_Dat_t *pCnf = Cnf_DataReadFromFile(pFileName);
sat_solver *pSat;
int i, status, RetValue = -1;
if ( pCnf == NULL )
if (pCnf == NULL)
return -1;
if ( fVerbose )
if (fVerbose)
{
printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
printf("CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals);
Abc_PrintTime(1, "Time", Abc_Clock() - clk);
}
// convert into SAT solver
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
if (pSat == NULL)
{
printf( "The problem is trivially UNSAT.\n" );
Cnf_DataFree( pCnf );
printf("The problem is trivially UNSAT.\n");
Cnf_DataFree(pCnf);
return 1;
}
if ( nLearnedStart )
if (nLearnedStart)
pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
if ( nLearnedDelta )
if (nLearnedDelta)
pSat->nLearntDelta = nLearnedDelta;
if ( nLearnedPerce )
if (nLearnedPerce)
pSat->nLearntRatio = nLearnedPerce;
if ( fVerbose )
if (fVerbose)
pSat->fVerbose = fVerbose;
//sat_solver_start_cardinality( pSat, 100 );
// sat_solver_start_cardinality( pSat, 100 );
// solve the miter
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
status = sat_solver_solve(pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0);
if (status == l_Undef)
RetValue = -1;
else if ( status == l_True )
else if (status == l_True)
RetValue = 0;
else if ( status == l_False )
else if (status == l_False)
RetValue = 1;
else
assert( 0 );
if ( fVerbose )
Sat_SolverPrintStats( stdout, pSat );
if ( RetValue == -1 )
Abc_Print( 1, "UNDECIDED " );
else if ( RetValue == 0 )
Abc_Print( 1, "SATISFIABLE " );
assert(0);
if (fVerbose)
Sat_SolverPrintStats(stdout, pSat);
if (RetValue == -1)
Abc_Print(1, "UNDECIDED ");
else if (RetValue == 0)
Abc_Print(1, "SATISFIABLE ");
else
Abc_Print( 1, "UNSATISFIABLE " );
//Abc_Print( -1, "\n" );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Abc_Print(1, "UNSATISFIABLE ");
// Abc_Print( -1, "\n" );
Abc_PrintTime(1, "Time", Abc_Clock() - clk);
// derive SAT assignment
if ( RetValue == 0 && nPis > 0 )
if (RetValue == 0 && nPis > 0)
{
*ppModel = ABC_ALLOC( int, nPis );
for ( i = 0; i < nPis; i++ )
(*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i );
*ppModel = ABC_ALLOC(int, nPis);
for (i = 0; i < nPis; i++)
(*ppModel)[i] = sat_solver_var_value(pSat, pCnf->nVars - nPis + i);
}
if ( RetValue == 0 && fShowPattern )
if (RetValue == 0 && fShowPattern)
{
for ( i = 0; i < pCnf->nVars; i++ )
printf( "%d", sat_solver_var_value(pSat,i) );
printf( "\n" );
for (i = 0; i < pCnf->nVars; i++)
printf("%d", sat_solver_var_value(pSat, i));
printf("\n");
}
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Cnf_DataFree(pCnf);
sat_solver_delete(pSat);
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_DataBestVar(Cnf_Dat_t *p, int *pSkip)
{
int *pNums = ABC_CALLOC(int, p->nVars);
int i, *pLit, NumMax = -1, iVarMax = -1;
for (i = 0; i < p->nClauses; i++)
for (pLit = p->pClauses[i]; pLit < p->pClauses[i + 1]; pLit++)
pNums[Abc_Lit2Var(*pLit)]++;
for (i = 0; i < p->nVars; i++)
if ((!pSkip || !pSkip[i]) && NumMax < pNums[i])
NumMax = pNums[i], iVarMax = i;
ABC_FREE(pNums);
return iVarMax;
}
void Cnf_Experiment1()
{
Cnf_Dat_t *pTemp, *p = Cnf_DataReadFromFile("../166b.cnf");
int i, *pSkip = ABC_CALLOC(int, p->nVars);
for (i = 0; i < 100; i++)
{
int iVar = Cnf_DataBestVar(p, pSkip);
char FileName[100];
sprintf(FileName, "cnf/%03d.cnf", i);
Cnf_DataWriteIntoFile(p, FileName, 0, NULL, NULL);
printf("Dumped file \"%s\".\n", FileName);
p = Cnf_DataDupCof(pTemp = p, Abc_Var2Lit(iVar, 0));
Cnf_DataFree(pTemp);
pSkip[iVar] = 1;
}
Cnf_DataFree(p);
ABC_FREE(pSkip);
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t *Cnf_GenRandLits(int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fVerbose)
{
Vec_Int_t *vLits = Vec_IntAlloc(nLits);
assert(iVarBeg < iVarEnd && nLits < iVarEnd - iVarBeg);
while (Vec_IntSize(vLits) < nLits)
{
int iVar = iVarBeg + (Abc_Random(0) ^ Rand) % (iVarEnd - iVarBeg);
assert(iVar >= iVarBeg && iVar < iVarEnd);
if (Vec_IntFind(vLits, Abc_Var2Lit(iVar, 0)) == -1 && Vec_IntFind(vLits, Abc_Var2Lit(iVar, 1)) == -1)
{
if (Value == 0)
Vec_IntPush(vLits, Abc_Var2Lit(iVar, 1));
else if (Value == 1)
Vec_IntPush(vLits, Abc_Var2Lit(iVar, 0));
else
Vec_IntPush(vLits, Abc_Var2Lit(iVar, Abc_Random(0) & 1));
}
}
Vec_IntSort(vLits, 0);
if ( fVerbose )
Vec_IntPrint(vLits);
fflush(stdout);
return vLits;
}
void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fPrepro, int fVerbose)
{
Cnf_Dat_t *p = Cnf_DataReadFromFile(pFileName); int k;
if (iVarEnd == ABC_INFINITY)
iVarEnd = p->nVars;
for (k = 0; k < nParts; k++)
{
Vec_Int_t *vLits = Cnf_GenRandLits(iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose);
Cnf_Dat_t *pCnf = Cnf_DataDupCofArray(p, vLits);
char FileName[100]; sprintf(FileName, "%02d.cnf", k);
if ( fPrepro ) {
char Command[1000];
sprintf(Command, "satelite --verbosity=0 -pre temp.cnf %s", FileName);
Cnf_DataWriteIntoFile(pCnf, "temp.cnf", 0, NULL, NULL);
if (system(Command) == -1) {
fprintf(stdout, "Command \"%s\" did not succeed. Preprocessing skipped.\n", Command);
Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
}
unlink("temp.cnf");
}
else
Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
Cnf_DataFree(pCnf);
Vec_IntFree(vLits);
}
Cnf_DataFree(p);
}
void Cnf_SplitCnfCleanup(int nParts)
{
char FileName[100]; int k;
for (k = 0; k < nParts; k++) {
sprintf(FileName, "%02d.cnf", k);
unlink(FileName);
}
}
void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose)
{
abctime clk = Abc_Clock();
Vec_Int_t *vSol = NULL;
int i, Rand = 0;
if ( nIters == 0 )
nIters = ABC_INFINITY;
Abc_Random(1);
for ( i = 0; i < Seed; i++ )
Abc_Random(0);
Rand = Abc_Random(0);
for (i = 0; i < nIters && !vSol; i++)
{
abctime clk2 = Abc_Clock();
Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fPrepro, fVerbose);
vSol = Cnf_RunSolver(nProcs, TimeOut, fVerbose);
Cnf_SplitCnfCleanup(nProcs);
if (fVerbose) {
printf( "Finished iteration %d. ", i);
Abc_PrintTime(0, "Time", Abc_Clock() - clk2);
}
}
printf("%solution is found. ", vSol ? "S" : "No s");
Abc_PrintTime(0, "Total time", Abc_Clock() - clk);
Vec_IntFreeP(&vSol);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

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