mirror of https://github.com/YosysHQ/abc.git
Merge pull request #524 from YosysHQ/upsteaming
Upsteaming Yosys changes
This commit is contained in:
commit
a082d1ba3a
|
|
@ -18,6 +18,7 @@
|
||||||
|
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
|
|
||||||
|
#include <inttypes.h>
|
||||||
#include "base/abc/abc.h"
|
#include "base/abc/abc.h"
|
||||||
#include "base/main/main.h"
|
#include "base/main/main.h"
|
||||||
#include "base/main/mainInt.h"
|
#include "base/main/mainInt.h"
|
||||||
|
|
@ -61457,7 +61458,7 @@ int Abc_CommandAbc9elSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) {
|
||||||
}
|
}
|
||||||
|
|
||||||
int Abc_CommandAbc9CatBtor( Abc_Frame_t * pAbc, int argc, char ** argv ) {
|
int Abc_CommandAbc9CatBtor( Abc_Frame_t * pAbc, int argc, char ** argv ) {
|
||||||
extern void Abc_BtorCat( char * pFileName, int fVerbose );
|
extern int32_t Abc_BtorCat( char * pFileName, int fVerbose );
|
||||||
|
|
||||||
int c, fVerbose = 0;
|
int c, fVerbose = 0;
|
||||||
char * pFileName;
|
char * pFileName;
|
||||||
|
|
@ -61480,9 +61481,7 @@ int Abc_CommandAbc9CatBtor( Abc_Frame_t * pAbc, int argc, char ** argv ) {
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
Abc_BtorCat( pFileName, fVerbose );
|
return Abc_BtorCat( pFileName, fVerbose );
|
||||||
|
|
||||||
return 0;
|
|
||||||
|
|
||||||
usage:
|
usage:
|
||||||
Abc_Print( -2, "usage: &catbtor [-v] <file>\n" );
|
Abc_Print( -2, "usage: &catbtor [-v] <file>\n" );
|
||||||
|
|
|
||||||
|
|
@ -26,12 +26,6 @@
|
||||||
ABC_NAMESPACE_IMPL_START
|
ABC_NAMESPACE_IMPL_START
|
||||||
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
|
||||||
/// DECLARATIONS ///
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
#define ABC_USE_HISTORY 1
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
/// FUNCTION DEFINITIONS ///
|
/// FUNCTION DEFINITIONS ///
|
||||||
////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
@ -102,7 +96,7 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command )
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
void Cmd_HistoryRead( Abc_Frame_t * p )
|
void Cmd_HistoryRead( Abc_Frame_t * p )
|
||||||
{
|
{
|
||||||
#if defined(ABC_USE_HISTORY)
|
#if !defined(ABC_NO_HISTORY)
|
||||||
char Buffer[ABC_MAX_STR];
|
char Buffer[ABC_MAX_STR];
|
||||||
FILE * pFile;
|
FILE * pFile;
|
||||||
assert( Vec_PtrSize(p->aHistory) == 0 );
|
assert( Vec_PtrSize(p->aHistory) == 0 );
|
||||||
|
|
@ -134,7 +128,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p )
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
|
void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
|
||||||
{
|
{
|
||||||
#if defined(ABC_USE_HISTORY)
|
#if !defined(ABC_NO_HISTORY)
|
||||||
FILE * pFile;
|
FILE * pFile;
|
||||||
char * pStr;
|
char * pStr;
|
||||||
int i;
|
int i;
|
||||||
|
|
@ -186,7 +180,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
|
||||||
***********************************************************************/
|
***********************************************************************/
|
||||||
void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit )
|
void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit )
|
||||||
{
|
{
|
||||||
#if defined(ABC_USE_HISTORY)
|
#if !defined(ABC_NO_HISTORY)
|
||||||
char * pStr;
|
char * pStr;
|
||||||
int i;
|
int i;
|
||||||
Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );
|
Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );
|
||||||
|
|
|
||||||
|
|
@ -34,6 +34,11 @@
|
||||||
#include <sys/stat.h>
|
#include <sys/stat.h>
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
// defined by gcc and clang when __int128 is available
|
||||||
|
#if defined(__SIZEOF_INT128__)
|
||||||
|
# define HAVE_INT_128
|
||||||
|
#endif
|
||||||
|
|
||||||
#ifdef _WIN32
|
#ifdef _WIN32
|
||||||
// Windows doesn't have __builtin_ctzll, implement it using portable algorithm
|
// Windows doesn't have __builtin_ctzll, implement it using portable algorithm
|
||||||
static inline int __builtin_ctzll(uint64_t x) {
|
static inline int __builtin_ctzll(uint64_t x) {
|
||||||
|
|
@ -187,8 +192,9 @@ static inline uint64_t u64_mask_n(int nBits) {
|
||||||
return (nBits >= 64) ? ~0ull : ((nBits <= 0) ? 0ull : ((1ull << nBits) - 1ull));
|
return (nBits >= 64) ? ~0ull : ((nBits <= 0) ? 0ull : ((1ull << nBits) - 1ull));
|
||||||
}
|
}
|
||||||
|
|
||||||
#ifdef _WIN32
|
#ifndef HAVE_INT_128
|
||||||
// Windows doesn't support __int128, so we limit to 32 variables on Windows
|
// Most 32 bit platforms and Windows doesn't support __int128, so we
|
||||||
|
// limit to 32 variables on those.
|
||||||
static void u128_to_dec(uint64_t x, char *buf, size_t cap) {
|
static void u128_to_dec(uint64_t x, char *buf, size_t cap) {
|
||||||
char tmp[64]; int n = 0;
|
char tmp[64]; int n = 0;
|
||||||
if (!x) { snprintf(buf, cap, "0"); return; }
|
if (!x) { snprintf(buf, cap, "0"); return; }
|
||||||
|
|
@ -397,10 +403,10 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2,
|
||||||
|
|
||||||
const uint64_t inMask = u64_mask_n(p1->nCis);
|
const uint64_t inMask = u64_mask_n(p1->nCis);
|
||||||
const uint64_t outMask = u64_mask_n(p1->nCos);
|
const uint64_t outMask = u64_mask_n(p1->nCos);
|
||||||
#ifdef _WIN32
|
#ifndef HAVE_INT_128
|
||||||
// Windows doesn't support __int128, limit to 32 variables
|
// No support for __int128, limit to 32 variables
|
||||||
if (nVars > 32) {
|
if (nVars > 32) {
|
||||||
fprintf(stderr, "Error: Windows build supports nVars<=32 (got nVars=%d)\n", nVars);
|
fprintf(stderr, "Error: This architecture build supports nVars<=32 (got nVars=%d)\n", nVars);
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
const uint64_t combs = ((uint64_t)1) << (unsigned)nVars;
|
const uint64_t combs = ((uint64_t)1) << (unsigned)nVars;
|
||||||
|
|
@ -420,7 +426,7 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2,
|
||||||
|
|
||||||
uint64_t inVec[BATCH], valid[NW];
|
uint64_t inVec[BATCH], valid[NW];
|
||||||
unsigned long long rounds = 0;
|
unsigned long long rounds = 0;
|
||||||
#ifdef _WIN32
|
#ifndef HAVE_INT_128
|
||||||
uint64_t patsDone = 0;
|
uint64_t patsDone = 0;
|
||||||
#else
|
#else
|
||||||
unsigned __int128 patsDone = 0;
|
unsigned __int128 patsDone = 0;
|
||||||
|
|
@ -428,7 +434,7 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2,
|
||||||
|
|
||||||
clock_t t0 = clock();
|
clock_t t0 = clock();
|
||||||
|
|
||||||
#ifdef _WIN32
|
#ifndef HAVE_INT_128
|
||||||
for (uint64_t base = 0; base < combs; base += BATCH) {
|
for (uint64_t base = 0; base < combs; base += BATCH) {
|
||||||
uint64_t remain = combs - base;
|
uint64_t remain = combs - base;
|
||||||
#else
|
#else
|
||||||
|
|
@ -535,10 +541,10 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin,
|
||||||
|
|
||||||
const uint64_t inMask = u64_mask_n(p1->nCis);
|
const uint64_t inMask = u64_mask_n(p1->nCis);
|
||||||
const uint64_t outMask = u64_mask_n(p1->nCos);
|
const uint64_t outMask = u64_mask_n(p1->nCos);
|
||||||
#ifdef _WIN32
|
#ifndef HAVE_INT_128
|
||||||
// Windows doesn't support __int128, limit to 32 variables
|
// No support for __int128, limit to 32 variables
|
||||||
if (nVars > 32) {
|
if (nVars > 32) {
|
||||||
fprintf(stderr, "Error: Windows build supports nVars<=32 (got nVars=%d)\n", nVars);
|
fprintf(stderr, "Error: This architecture build supports nVars<=32 (got nVars=%d)\n", nVars);
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
const uint64_t combs = ((uint64_t)1) << (unsigned)nVars;
|
const uint64_t combs = ((uint64_t)1) << (unsigned)nVars;
|
||||||
|
|
@ -565,7 +571,7 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin,
|
||||||
|
|
||||||
uint64_t inVec[BATCH], valid[NW];
|
uint64_t inVec[BATCH], valid[NW];
|
||||||
unsigned long long rounds = 0;
|
unsigned long long rounds = 0;
|
||||||
#ifdef _WIN32
|
#ifndef HAVE_INT_128
|
||||||
uint64_t patsDone = 0;
|
uint64_t patsDone = 0;
|
||||||
#else
|
#else
|
||||||
unsigned __int128 patsDone = 0;
|
unsigned __int128 patsDone = 0;
|
||||||
|
|
@ -573,7 +579,7 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin,
|
||||||
|
|
||||||
clock_t t0 = clock();
|
clock_t t0 = clock();
|
||||||
|
|
||||||
#ifdef _WIN32
|
#ifndef HAVE_INT_128
|
||||||
for (uint64_t base = 0; base < combs; base += BATCH) {
|
for (uint64_t base = 0; base < combs; base += BATCH) {
|
||||||
uint64_t remain = combs - base;
|
uint64_t remain = combs - base;
|
||||||
#else
|
#else
|
||||||
|
|
|
||||||
|
|
@ -1281,7 +1281,11 @@ static inline int run_external_solver_on_aig( Abc_Ntk_t * pAbcNtk, const string&
|
||||||
command = "timeout " + to_string(nRuntimeLimitSec) + " " + command;
|
command = "timeout " + to_string(nRuntimeLimitSec) + " " + command;
|
||||||
command += " > log.txt 2>&1";
|
command += " > log.txt 2>&1";
|
||||||
LOG(1) << "UFAR external solver: launching command instead of PDR: " << command;
|
LOG(1) << "UFAR external solver: launching command instead of PDR: " << command;
|
||||||
|
#ifdef __wasm
|
||||||
|
int res = -1;
|
||||||
|
#else
|
||||||
int res = system( command.c_str() );
|
int res = system( command.c_str() );
|
||||||
|
#endif
|
||||||
std::remove( pAigFile );
|
std::remove( pAigFile );
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -61,8 +61,10 @@ struct Cec_SproveTrace_t_;
|
||||||
static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
|
static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
|
||||||
static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
|
static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
|
||||||
static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
|
static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
|
||||||
|
#ifdef ABC_USE_PTHREADS
|
||||||
static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
|
static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
|
||||||
static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers );
|
static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers );
|
||||||
|
#endif
|
||||||
static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine );
|
static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine );
|
||||||
|
|
||||||
extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );
|
extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue