Skip to content
Projects
Groups
Snippets
Help
This project
Loading...
Sign in / Register
Toggle navigation
A
abc
Overview
Overview
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
lvzhengyang
abc
Commits
6f0d8088
Commit
6f0d8088
authored
Nov 20, 2018
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Various usability changes (second round).
parent
f3c5bab5
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
82 additions
and
2 deletions
+82
-2
src/base/abci/abc.c
+40
-1
src/base/main/mainReal.c
+39
-1
src/misc/util/abc_global.h
+3
-0
No files found.
src/base/abci/abc.c
View file @
6f0d8088
...
...
@@ -10992,6 +10992,11 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print
(
-
1
,
"Reachability analysis works only for AIGs (run
\"
strash
\"
).
\n
"
);
return
1
;
}
if
(
pAbc
->
fBatchMode
&&
(
pAbc
->
Status
==
0
||
pAbc
->
Status
==
1
)
)
{
Abc_Print
(
1
,
"The miters is already solved; skipping the command.
\n
"
);
return
0
;
}
pAbc
->
Status
=
Abc_NtkDarReach
(
pNtk
,
pPars
);
pAbc
->
nFrames
=
pPars
->
iFrame
;
Abc_FrameReplaceCex
(
pAbc
,
&
pNtk
->
pSeqModel
);
...
...
@@ -23901,12 +23906,16 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print
(
-
1
,
"Empty network.
\n
"
);
return
1
;
}
if
(
!
Abc_NtkIsStrash
(
pNtk
)
)
{
Abc_Print
(
-
1
,
"This command works only for structrally hashed networks. Run
\"
st
\"
.
\n
"
);
return
0
;
}
if
(
pAbc
->
fBatchMode
&&
(
pAbc
->
Status
==
0
||
pAbc
->
Status
==
1
)
)
{
Abc_Print
(
1
,
"The miters is already solved; skipping the command.
\n
"
);
return
0
;
}
// perform verification
pAbc
->
Status
=
Abc_NtkDarProve
(
pNtk
,
pSecPar
,
nBmcFramesMax
,
nBmcConfMax
);
...
...
@@ -25605,6 +25614,11 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print
(
-
1
,
"Does not work for combinational networks.
\n
"
);
return
0
;
}
if
(
pAbc
->
fBatchMode
&&
(
pAbc
->
Status
==
0
||
pAbc
->
Status
==
1
)
)
{
Abc_Print
(
1
,
"The miters is already solved; skipping the command.
\n
"
);
return
0
;
}
pAbc
->
Status
=
Abc_NtkDarBmc
(
pNtk
,
0
,
nFrames
,
nSizeMax
,
nNodeDelta
,
0
,
nBTLimit
,
nBTLimitAll
,
fRewrite
,
fNewAlgo
,
0
,
nCofFanLit
,
fVerbose
,
&
iFrames
,
fUseSatoko
);
pAbc
->
nFrames
=
iFrames
;
Abc_FrameReplaceCex
(
pAbc
,
&
pNtk
->
pSeqModel
);
...
...
@@ -25800,6 +25814,11 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print
(
-
1
,
"Does not work for combinational networks.
\n
"
);
return
0
;
}
if
(
pAbc
->
fBatchMode
&&
(
pAbc
->
Status
==
0
||
pAbc
->
Status
==
1
)
)
{
Abc_Print
(
1
,
"The miters is already solved; skipping the command.
\n
"
);
return
0
;
}
pAbc
->
Status
=
Abc_NtkDarBmc
(
pNtk
,
nStart
,
nFrames
,
nSizeMax
,
nNodeDelta
,
nTimeOut
,
nBTLimit
,
nBTLimitAll
,
fRewrite
,
fNewAlgo
,
fOrDecomp
,
0
,
fVerbose
,
&
iFrames
,
fUseSatoko
);
pAbc
->
nFrames
=
iFrames
;
Abc_FrameReplaceCex
(
pAbc
,
&
pNtk
->
pSeqModel
);
...
...
@@ -26054,6 +26073,11 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print
(
-
1
,
"Constraints have to be folded (use
\"
fold
\"
).
\n
"
);
return
0
;
}
if
(
pAbc
->
fBatchMode
&&
(
pAbc
->
Status
==
0
||
pAbc
->
Status
==
1
)
)
{
Abc_Print
(
1
,
"The miters is already solved; skipping the command.
\n
"
);
return
0
;
}
pPars
->
fUseBridge
=
pAbc
->
fBridgeMode
;
pAbc
->
Status
=
Abc_NtkDarBmc3
(
pNtk
,
pPars
,
fOrDecomp
);
pAbc
->
nFrames
=
pNtk
->
vSeqModelVec
?
-
1
:
pPars
->
iFrame
;
...
...
@@ -26260,6 +26284,11 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print
(
-
1
,
"Currently only works for structurally hashed circuits.
\n
"
);
return
0
;
}
if
(
pAbc
->
fBatchMode
&&
(
pAbc
->
Status
==
0
||
pAbc
->
Status
==
1
)
)
{
Abc_Print
(
1
,
"The miters is already solved; skipping the command.
\n
"
);
return
0
;
}
if
(
Abc_NtkLatchNum
(
pNtk
)
==
0
)
{
Abc_Print
(
-
1
,
"Does not work for combinational networks.
\n
"
);
...
...
@@ -27991,6 +28020,11 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print
(
-
2
,
"The current network is not an AIG (run
\"
strash
\"
).
\n
"
);
return
0
;
}
if
(
pAbc
->
fBatchMode
&&
(
pAbc
->
Status
==
0
||
pAbc
->
Status
==
1
)
)
{
Abc_Print
(
1
,
"The miters is already solved; skipping the command.
\n
"
);
return
0
;
}
if
(
Abc_NtkLatchNum
(
pNtk
)
==
0
)
{
pNtkFlop
=
Abc_NtkDup
(
pNtk
);
...
...
@@ -44473,6 +44507,11 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
*/
if
(
pAbc
->
fBatchMode
&&
(
pAbc
->
Status
==
0
||
pAbc
->
Status
==
1
)
)
{
Abc_Print
(
1
,
"The miters is already solved; skipping the command.
\n
"
);
return
0
;
}
if
(
pAbc
->
pGia
->
vGateClasses
==
NULL
)
{
Abc_Print
(
-
1
,
"Abstraction gate map is missing.
\n
"
);
src/base/main/mainReal.c
View file @
6f0d8088
...
...
@@ -44,6 +44,14 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
***********************************************************************/
#ifndef WIN32
#include <sys/time.h>
#include <sys/times.h>
#include <sys/resource.h>
#include <unistd.h>
#include <signal.h>
#include <malloc.h>
#endif
#include "base/abc/abc.h"
#include "mainInt.h"
...
...
@@ -62,6 +70,7 @@ static int TypeCheck( Abc_Frame_t * pAbc, const char * s);
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
unsigned
enable_dbg_outs
=
1
;
/**Function*************************************************************
...
...
@@ -115,8 +124,37 @@ int Abc_RealMain( int argc, char * argv[] )
sprintf
(
sWriteCmd
,
"write"
);
Extra_UtilGetoptReset
();
while
((
c
=
Extra_UtilGetopt
(
argc
,
argv
,
"c:q:C:Q:S:hf:F:o:st:T:xb"
))
!=
EOF
)
{
while
((
c
=
Extra_UtilGetopt
(
argc
,
argv
,
"
dm:l:
c:q:C:Q:S:hf:F:o:st:T:xb"
))
!=
EOF
)
{
switch
(
c
)
{
case
'd'
:
enable_dbg_outs
^=
1
;
break
;
case
'm'
:
#ifndef WIN32
int
maxMb
=
atoi
(
globalUtilOptarg
);
printf
(
"Limiting memory use to %d MB
\n
"
,
maxMb
);
struct
rlimit
limit
=
{
maxMb
*
(
1llu
<<
20
),
/* soft limit */
maxMb
*
(
1llu
<<
20
)
/* hard limit */
};
setrlimit
(
RLIMIT_AS
,
&
limit
);
#endif
break
;
case
'l'
:
#ifndef WIN32
int
maxTime
=
atoi
(
globalUtilOptarg
);
printf
(
"Limiting time to %d seconds
\n
"
,
maxTime
);
struct
rlimit
limit
=
{
maxTime
,
/* soft limit */
maxTime
/* hard limit */
};
setrlimit
(
RLIMIT_CPU
,
&
limit
);
#endif
break
;
case
'c'
:
if
(
Vec_StrSize
(
sCommandUsr
)
>
0
)
{
...
...
src/misc/util/abc_global.h
View file @
6f0d8088
...
...
@@ -357,6 +357,9 @@ static inline void Abc_Print( int level, const char * format, ... )
{
extern
ABC_DLL
int
Abc_FrameIsBridgeMode
();
va_list
args
;
extern
unsigned
enable_dbg_outs
;
if
(
!
enable_dbg_outs
)
return
;
if
(
!
Abc_FrameIsBridgeMode
()
){
if
(
level
==
ABC_ERROR
)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment