mirror of https://github.com/YosysHQ/abc.git
Version abc80130
This commit is contained in:
Alan Mishchenko
parent
6537f94188
commit
4d30a1e4f1
26
Makefile
26
Makefile
|
|
@ -6,20 +6,12 @@ CP := cp
|
|||
|
||||
PROG := abc
|
||||
|
||||
MODULES := src/base/abc src/base/abci src/base/cmd \
|
||||
src/base/io src/base/main src/base/ver \
|
||||
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
|
||||
src/bdd/parse src/bdd/reo src/bdd/cas \
|
||||
src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \
|
||||
src/misc/extra src/misc/mvc src/misc/st src/misc/util \
|
||||
src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
|
||||
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr \
|
||||
src/opt/sim src/opt/ret src/opt/res src/opt/lpk src/opt/fret \
|
||||
src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
|
||||
src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
|
||||
src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
|
||||
src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
|
||||
src/aig/bdc src/aig/bar src/aig/ntl src/aig/tim
|
||||
MODULES := src/base/abc src/base/abci src/base/abcs src/base/cmd src/base/io src/base/main \
|
||||
src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
|
||||
src/map/fpga src/map/mapper src/map/mio src/map/super \
|
||||
src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/vec \
|
||||
src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
|
||||
src/sat/asat src/sat/csat src/sat/msat src/sat/fraig
|
||||
|
||||
default: $(PROG)
|
||||
|
||||
|
|
@ -29,7 +21,7 @@ OPTFLAGS := -DNDEBUG -O3
|
|||
CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES))
|
||||
CXXFLAGS += $(CFLAGS)
|
||||
|
||||
LIBS := -ldl -rdynamic -lreadline -ltermcap
|
||||
LIBS :=
|
||||
SRC :=
|
||||
GARBAGE := core core.* *.stackdump ./tags $(PROG)
|
||||
|
||||
|
|
@ -67,10 +59,6 @@ tags:
|
|||
$(PROG): $(OBJ)
|
||||
$(LD) -o $@ $^ $(LIBS)
|
||||
|
||||
lib$(PROG).a: $(OBJ)
|
||||
ar rv $@ $?
|
||||
ranlib $@
|
||||
|
||||
docs:
|
||||
doxygen doxygen.conf
|
||||
|
||||
|
|
|
|||
89
abc.rc
89
abc.rc
|
|
@ -1,10 +1,9 @@
|
|||
# global parameters
|
||||
set check # checks intermediate networks
|
||||
#set check # checks intermediate networks
|
||||
#set checkfio # prints warnings when fanins/fanouts are duplicated
|
||||
set checkread # checks new networks after reading from file
|
||||
set backup # saves backup networks retrived by "undo" and "recall"
|
||||
set savesteps 1 # sets the maximum number of backup networks to save
|
||||
set progressbar # display the progress bar
|
||||
set savesteps 1 # sets the maximum number of backup networks to save
|
||||
|
||||
# program names for internal calls
|
||||
set dotwin dot.exe
|
||||
|
|
@ -15,10 +14,6 @@ set siswin sis.exe
|
|||
set sisunix sis
|
||||
set mvsiswin mvsis.exe
|
||||
set mvsisunix mvsis
|
||||
set capowin MetaPl-Capo10.1-Win32.exe
|
||||
set capounix MetaPl-Capo10.1
|
||||
set gnuplotwin wgnuplot.exe
|
||||
set gnuplotunix gnuplot
|
||||
|
||||
# standard aliases
|
||||
alias b balance
|
||||
|
|
@ -27,102 +22,48 @@ alias clp collapse
|
|||
alias esd ext_seq_dcs
|
||||
alias f fraig
|
||||
alias fs fraig_sweep
|
||||
alias fsto fraig_store
|
||||
alias fres fraig_restore
|
||||
alias ft fraig_trust
|
||||
alias lp lutpack
|
||||
alias pd print_dsd
|
||||
alias pex print_exdc -d
|
||||
alias mu renode -m
|
||||
alias pf print_factor
|
||||
alias pfan print_fanio
|
||||
alias pl print_level
|
||||
alias pio print_io
|
||||
alias pk print_kmap
|
||||
alias ps print_stats
|
||||
alias psu print_supp
|
||||
alias psy print_symm
|
||||
alias pun print_unate
|
||||
alias q quit
|
||||
alias r read
|
||||
alias r3 retime -M 3
|
||||
alias r3f retime -M 3 -f
|
||||
alias r3b retime -M 3 -b
|
||||
alias ren renode
|
||||
alias rh read_hie
|
||||
alias rl read_blif
|
||||
alias rb read_bench
|
||||
alias ret retime
|
||||
alias dret dretime
|
||||
alias rp read_pla
|
||||
alias rt read_truth
|
||||
alias rv read_verilog
|
||||
alias rvl read_verlib
|
||||
alias rsup read_super mcnc5_old.super
|
||||
alias rlib read_library
|
||||
alias rlibc read_library cadence.genlib
|
||||
alias rw rewrite
|
||||
alias rwz rewrite -z
|
||||
alias rf refactor
|
||||
alias rfz refactor -z
|
||||
alias re restructure
|
||||
alias rez restructure -z
|
||||
alias rs resub
|
||||
alias rsz resub -z
|
||||
alias sa set autoexec ps
|
||||
alias scl scleanup
|
||||
alias sif if -s
|
||||
alias so source -x
|
||||
alias st strash
|
||||
alias sw sweep
|
||||
alias ssw ssweep
|
||||
alias tr0 trace_start
|
||||
alias tr1 trace_check
|
||||
alias trt "r c.blif; st; tr0; b; tr1"
|
||||
alias u undo
|
||||
alias w write
|
||||
alias wa write_aiger
|
||||
alias wb write_bench
|
||||
alias wc write_cnf
|
||||
alias wh write_hie
|
||||
alias wb write_blif
|
||||
alias wl write_blif
|
||||
alias wp write_pla
|
||||
alias wv write_verilog
|
||||
|
||||
# standard scripts
|
||||
alias resyn "b; rw; rwz; b; rwz; b"
|
||||
alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
|
||||
alias resyn2a "b; rw; b; rw; rwz; b; rwz; b"
|
||||
alias resyn3 "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b"
|
||||
alias compress "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
|
||||
alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
|
||||
alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
|
||||
alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
|
||||
alias rwsat "st; rw -l; b -l; rw -l; rf -l"
|
||||
alias rwsat2 "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
|
||||
alias shake "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
|
||||
alias share "st; multi -m; fx; resyn2"
|
||||
alias cnf "st; ren -c; write_cnf"
|
||||
alias prove "st; ren -c; sat"
|
||||
alias opt "b; ren; b"
|
||||
alias share "b; ren; fx; b"
|
||||
alias sharem "b; ren -m; fx; b"
|
||||
alias sharedsd "b; ren; dsd -g; sw; fx; b"
|
||||
alias resyn "b; rw; rwz; b; rwz; b"
|
||||
alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
|
||||
alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore"
|
||||
|
||||
# resubstitution scripts for the IWLS paper
|
||||
alias src_rw "st; rw -l; rwz -l; rwz -l"
|
||||
alias src_rs "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l"
|
||||
alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l"
|
||||
alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
|
||||
alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
|
||||
|
||||
# experimental implementation of don't-cares
|
||||
alias resyn2rsdc "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
|
||||
alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
|
||||
|
||||
# temporaries
|
||||
alias reach "st; ps; compress2; ps; qrel; ps; compress2; ps; qreach -v; ps"
|
||||
alias chnew "st; haig_start; resyn2; haig_use"
|
||||
alias chnewrs "st; haig_start; resyn2rs; haig_use"
|
||||
alias stdsd "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
|
||||
alias trec "rec_start; r c.blif; st; rec_add; rec_use"
|
||||
alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
|
||||
alias bmc2 "frames -i -F 10; orpos; iprove"
|
||||
|
||||
alias t0 "r test/mc1.blif; st; test"
|
||||
alias t1 "r s27mc2.blif; st; test"
|
||||
alias t2 "r i/intel_001.aig; ps; indcut -v"
|
||||
alias scl scleanup
|
||||
alias ssw ssweep
|
||||
|
||||
|
|
|
|||
2844
abclib.dsp
2844
abclib.dsp
File diff suppressed because it is too large
Load Diff
29
abclib.dsw
29
abclib.dsw
|
|
@ -1,29 +0,0 @@
|
|||
Microsoft Developer Studio Workspace File, Format Version 6.00
|
||||
# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
|
||||
|
||||
###############################################################################
|
||||
|
||||
Project: "abclib"=.\abclib.dsp - Package Owner=<4>
|
||||
|
||||
Package=<5>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
Package=<4>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
###############################################################################
|
||||
|
||||
Global:
|
||||
|
||||
Package=<5>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
Package=<3>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
###############################################################################
|
||||
|
||||
102
abctestlib.dsp
102
abctestlib.dsp
|
|
@ -1,102 +0,0 @@
|
|||
# Microsoft Developer Studio Project File - Name="abctestlib" - Package Owner=<4>
|
||||
# Microsoft Developer Studio Generated Build File, Format Version 6.00
|
||||
# ** DO NOT EDIT **
|
||||
|
||||
# TARGTYPE "Win32 (x86) Console Application" 0x0103
|
||||
|
||||
CFG=abctestlib - Win32 Debug
|
||||
!MESSAGE This is not a valid makefile. To build this project using NMAKE,
|
||||
!MESSAGE use the Export Makefile command and run
|
||||
!MESSAGE
|
||||
!MESSAGE NMAKE /f "abctestlib.mak".
|
||||
!MESSAGE
|
||||
!MESSAGE You can specify a configuration when running NMAKE
|
||||
!MESSAGE by defining the macro CFG on the command line. For example:
|
||||
!MESSAGE
|
||||
!MESSAGE NMAKE /f "abctestlib.mak" CFG="abctestlib - Win32 Debug"
|
||||
!MESSAGE
|
||||
!MESSAGE Possible choices for configuration are:
|
||||
!MESSAGE
|
||||
!MESSAGE "abctestlib - Win32 Release" (based on "Win32 (x86) Console Application")
|
||||
!MESSAGE "abctestlib - Win32 Debug" (based on "Win32 (x86) Console Application")
|
||||
!MESSAGE
|
||||
|
||||
# Begin Project
|
||||
# PROP AllowPerConfigDependencies 0
|
||||
# PROP Scc_ProjName ""
|
||||
# PROP Scc_LocalPath ""
|
||||
CPP=cl.exe
|
||||
RSC=rc.exe
|
||||
|
||||
!IF "$(CFG)" == "abctestlib - Win32 Release"
|
||||
|
||||
# PROP BASE Use_MFC 0
|
||||
# PROP BASE Use_Debug_Libraries 0
|
||||
# PROP BASE Output_Dir "Release"
|
||||
# PROP BASE Intermediate_Dir "Release"
|
||||
# PROP BASE Target_Dir ""
|
||||
# PROP Use_MFC 0
|
||||
# PROP Use_Debug_Libraries 0
|
||||
# PROP Output_Dir "Release"
|
||||
# PROP Intermediate_Dir "Release"
|
||||
# PROP Ignore_Export_Lib 0
|
||||
# PROP Target_Dir ""
|
||||
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
|
||||
# ADD CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
|
||||
# ADD BASE RSC /l 0x409 /d "NDEBUG"
|
||||
# ADD RSC /l 0x409 /d "NDEBUG"
|
||||
BSC32=bscmake.exe
|
||||
# ADD BASE BSC32 /nologo
|
||||
# ADD BSC32 /nologo
|
||||
LINK32=link.exe
|
||||
# ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /machine:I386
|
||||
# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib C:\_projects\abc\abclib\abclib_release.lib /nologo /subsystem:console /machine:I386 /out:"_TEST/abctestlib.exe"
|
||||
|
||||
!ELSEIF "$(CFG)" == "abctestlib - Win32 Debug"
|
||||
|
||||
# PROP BASE Use_MFC 0
|
||||
# PROP BASE Use_Debug_Libraries 1
|
||||
# PROP BASE Output_Dir "Debug"
|
||||
# PROP BASE Intermediate_Dir "Debug"
|
||||
# PROP BASE Target_Dir ""
|
||||
# PROP Use_MFC 0
|
||||
# PROP Use_Debug_Libraries 1
|
||||
# PROP Output_Dir "Debug"
|
||||
# PROP Intermediate_Dir "Debug"
|
||||
# PROP Ignore_Export_Lib 0
|
||||
# PROP Target_Dir ""
|
||||
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
|
||||
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /FR /YX /FD /GZ /c
|
||||
# ADD BASE RSC /l 0x409 /d "_DEBUG"
|
||||
# ADD RSC /l 0x409 /d "_DEBUG"
|
||||
BSC32=bscmake.exe
|
||||
# ADD BASE BSC32 /nologo
|
||||
# ADD BSC32 /nologo
|
||||
LINK32=link.exe
|
||||
# ADD BASE LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /debug /machine:I386 /pdbtype:sept
|
||||
# ADD LINK32 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib C:\_projects\abc\abclib\abclib_debug.lib /nologo /subsystem:console /debug /machine:I386 /out:"_TEST/abctestlib.exe" /pdbtype:sept
|
||||
|
||||
!ENDIF
|
||||
|
||||
# Begin Target
|
||||
|
||||
# Name "abctestlib - Win32 Release"
|
||||
# Name "abctestlib - Win32 Debug"
|
||||
# Begin Group "Source Files"
|
||||
|
||||
# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\demo.c
|
||||
# End Source File
|
||||
# End Group
|
||||
# Begin Group "Header Files"
|
||||
|
||||
# PROP Default_Filter "h;hpp;hxx;hm;inl"
|
||||
# End Group
|
||||
# Begin Group "Resource Files"
|
||||
|
||||
# PROP Default_Filter "ico;cur;bmp;dlg;rc2;rct;bin;rgs;gif;jpg;jpeg;jpe"
|
||||
# End Group
|
||||
# End Target
|
||||
# End Project
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
Microsoft Developer Studio Workspace File, Format Version 6.00
|
||||
# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
|
||||
|
||||
###############################################################################
|
||||
|
||||
Project: "abctestlib"=.\abctestlib.dsp - Package Owner=<4>
|
||||
|
||||
Package=<5>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
Package=<4>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
###############################################################################
|
||||
|
||||
Global:
|
||||
|
||||
Package=<5>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
Package=<3>
|
||||
{{{
|
||||
}}}
|
||||
|
||||
###############################################################################
|
||||
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
Copyright (c) The Regents of the University of California. All rights reserved.
|
||||
|
||||
Permission is hereby granted, without written agreement and without license or
|
||||
royalty fees, to use, copy, modify, and distribute this software and its
|
||||
documentation for any purpose, provided that the above copyright notice and
|
||||
the following two paragraphs appear in all copies of this software.
|
||||
|
||||
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
|
||||
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
|
||||
THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
|
||||
CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
|
||||
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
|
||||
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
|
||||
A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
|
||||
AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
|
||||
SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
|
||||
|
||||
181
demo.c
181
demo.c
|
|
@ -1,181 +0,0 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [demo.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [ABC as a static library.]
|
||||
|
||||
Synopsis [A demo program illustrating the use of ABC as a static library.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: demo.c,v 1.00 2005/11/14 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include <stdio.h>
|
||||
#include <time.h>
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// procedures to start and stop the ABC framework
|
||||
// (should be called before and after the ABC procedures are called)
|
||||
extern void Abc_Start();
|
||||
extern void Abc_Stop();
|
||||
|
||||
// procedures to get the ABC framework and execute commands in it
|
||||
extern void * Abc_FrameGetGlobalFrame();
|
||||
extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [The main() procedure.]
|
||||
|
||||
Description [This procedure compiles into a stand-alone program for
|
||||
DAG-aware rewriting of the AIGs. A BLIF or PLA file to be considered
|
||||
for rewriting should be given as a command-line argument. Implementation
|
||||
of the rewriting is inspired by the paper: Per Bjesse, Arne Boralv,
|
||||
"DAG-aware circuit compression for formal verification", Proc. ICCAD 2004.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int main( int argc, char * argv[] )
|
||||
{
|
||||
// parameters
|
||||
int fUseResyn2 = 0;
|
||||
int fPrintStats = 1;
|
||||
int fVerify = 1;
|
||||
// variables
|
||||
void * pAbc;
|
||||
char * pFileName;
|
||||
char Command[1000];
|
||||
int clkRead, clkResyn, clkVer, clk;
|
||||
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// get the input file name
|
||||
if ( argc != 2 )
|
||||
{
|
||||
printf( "Wrong number of command-line arguments.\n" );
|
||||
return 1;
|
||||
}
|
||||
pFileName = argv[1];
|
||||
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// start the ABC framework
|
||||
Abc_Start();
|
||||
pAbc = Abc_FrameGetGlobalFrame();
|
||||
|
||||
clk = clock();
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// read the file
|
||||
sprintf( Command, "read %s", pFileName );
|
||||
if ( Cmd_CommandExecute( pAbc, Command ) )
|
||||
{
|
||||
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
|
||||
return 1;
|
||||
}
|
||||
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// balance
|
||||
sprintf( Command, "balance" );
|
||||
if ( Cmd_CommandExecute( pAbc, Command ) )
|
||||
{
|
||||
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
|
||||
return 1;
|
||||
}
|
||||
clkRead = clock() - clk;
|
||||
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// print stats
|
||||
if ( fPrintStats )
|
||||
{
|
||||
sprintf( Command, "print_stats" );
|
||||
if ( Cmd_CommandExecute( pAbc, Command ) )
|
||||
{
|
||||
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
clk = clock();
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// synthesize
|
||||
if ( fUseResyn2 )
|
||||
{
|
||||
sprintf( Command, "balance; rewrite -l; refactor -l; balance; rewrite -l; rewrite -lz; balance; refactor -lz; rewrite -lz; balance" );
|
||||
if ( Cmd_CommandExecute( pAbc, Command ) )
|
||||
{
|
||||
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
sprintf( Command, "balance; rewrite -l; rewrite -lz; balance; rewrite -lz; balance" );
|
||||
if ( Cmd_CommandExecute( pAbc, Command ) )
|
||||
{
|
||||
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
clkResyn = clock() - clk;
|
||||
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// print stats
|
||||
if ( fPrintStats )
|
||||
{
|
||||
sprintf( Command, "print_stats" );
|
||||
if ( Cmd_CommandExecute( pAbc, Command ) )
|
||||
{
|
||||
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// write the result in blif
|
||||
sprintf( Command, "write_blif result.blif" );
|
||||
if ( Cmd_CommandExecute( pAbc, Command ) )
|
||||
{
|
||||
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
|
||||
return 1;
|
||||
}
|
||||
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// perform verification
|
||||
clk = clock();
|
||||
if ( fVerify )
|
||||
{
|
||||
sprintf( Command, "cec %s result.blif", pFileName );
|
||||
if ( Cmd_CommandExecute( pAbc, Command ) )
|
||||
{
|
||||
fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
clkVer = clock() - clk;
|
||||
|
||||
printf( "Reading = %6.2f sec ", (float)(clkRead)/(float)(CLOCKS_PER_SEC) );
|
||||
printf( "Rewriting = %6.2f sec ", (float)(clkResyn)/(float)(CLOCKS_PER_SEC) );
|
||||
printf( "Verification = %6.2f sec\n", (float)(clkVer)/(float)(CLOCKS_PER_SEC) );
|
||||
|
||||
//////////////////////////////////////////////////////////////////////////
|
||||
// stop the ABC framework
|
||||
Abc_Stop();
|
||||
return 0;
|
||||
}
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
26
readme
26
readme
|
|
@ -1,26 +0,0 @@
|
|||
Often the code comes directly from a Windows computer.
|
||||
The following steps may be needed to compile it on UNIX:
|
||||
|
||||
>> dos2unix Makefile Makefile
|
||||
>> dos2unix depends.sh depends.sh
|
||||
>> chmod 755 depends.sh
|
||||
>> make // on Solaris, try "gmake"
|
||||
|
||||
If compiling as a static library, it is necessary to uncomment
|
||||
#define _LIB in "src/abc/main/main.c"
|
||||
|
||||
Several things to try if it does not compile on your platform:
|
||||
- Try running all code (not only Makefile and depends.sh) through dos2unix
|
||||
- Try the following actions:
|
||||
(a) Remove flags from the libs line (LIBS :=) in Makefile
|
||||
(b) Remove "src\base\main\libSupport.c" from "src\base\main\module.make"
|
||||
(c) Comment calls to Libs_Init() and Libs_End() in "src\base\main\mainInit.c"
|
||||
- Try linking with gcc (rather than g++)
|
||||
For this replace "LD := g++" with "LD := gcc -lm" in Makefile
|
||||
- If your Linux distributin does not have "readline", you may have problems
|
||||
compiling ABC with gcc. Please try installing this library from
|
||||
http://tiswww.case.edu/php/chet/readline/rltop.html
|
||||
|
||||
|
||||
Finally, run regression test:
|
||||
abc>>> so regtest.script
|
||||
119
regtest.script
119
regtest.script
|
|
@ -1,18 +1,103 @@
|
|||
r examples/apex4.pla; resyn; if; cec; ps; clp; resyn; map; cec; ps
|
||||
r examples/C2670.blif; st; w 1.aig; cec 1.aig
|
||||
r examples/C2670.blif; st; short_names; w 1.bench; cec 1.bench
|
||||
r examples/C2670.blif; st; short_names; ren -s; w 1.eqn; cec 1.eqn
|
||||
r examples/C2670.blif; resyn2; if -K 8; cec; ps; u; map; cec; ps
|
||||
r examples/frg2.blif; dsd; muxes; cec; ps; clp; share; resyn; map; cec; ps
|
||||
r examples/frg2.blif; bdd; muxes; cec; ps; clp; st; ren -b; muxes; cec; ps
|
||||
r examples/i10.blif; resyn2; fpga; cec; ps; u; map; cec; ps
|
||||
r examples/i10.blif; choice; fpga; cec; ps; u; map; cec; ps
|
||||
r examples/pj1.blif; st; if; cec; ps; u; map; cec; ps
|
||||
r examples/s38417.blif; comb; w 1.blif; resyn; if; cec 1.blif; ps
|
||||
r examples/s38417.blif; resyn; if; cec; ps; u; map; cec; ps
|
||||
r examples/s38584.bench; resyn; ren -s; fx; if; cec; ps; u; map; cec; ps
|
||||
r examples/s444.blif; b; esd -v; print_exdc; dsd; cec; ps
|
||||
r examples/s444.blif; double; frames -F 5; w 1.blif; ffpga -K 8; cec 1.blif
|
||||
r examples/s5378.blif; frames -F 5; cycle; w 1.blif; ps; ret; ps; sec 1.blif
|
||||
r examples/s6669.blif; cycle; w 1.blif; ps; ret -M 3; resyn; ps; sec 1.blif
|
||||
r examples/apex4.pla
|
||||
resyn
|
||||
sharem
|
||||
fpga
|
||||
cec
|
||||
ps
|
||||
|
||||
clp
|
||||
share
|
||||
resyn
|
||||
map
|
||||
cec
|
||||
ps
|
||||
|
||||
r examples/C2670.blif
|
||||
resyn
|
||||
fpga
|
||||
cec
|
||||
ps
|
||||
|
||||
u
|
||||
map
|
||||
cec
|
||||
ps
|
||||
|
||||
r examples/frg2.blif
|
||||
dsd
|
||||
muxes
|
||||
cec
|
||||
clp
|
||||
share
|
||||
resyn
|
||||
map
|
||||
cec
|
||||
ps
|
||||
|
||||
r examples/pj1.blif
|
||||
resyn
|
||||
fpga
|
||||
cec
|
||||
ps
|
||||
|
||||
u
|
||||
map
|
||||
cec
|
||||
ps
|
||||
|
||||
r examples/s38584.bench
|
||||
resyn
|
||||
fpga
|
||||
cec
|
||||
ps
|
||||
|
||||
u
|
||||
map
|
||||
cec
|
||||
ps
|
||||
|
||||
r examples/ac.v
|
||||
resyn
|
||||
fpga
|
||||
cec
|
||||
ps
|
||||
|
||||
u
|
||||
map
|
||||
cec
|
||||
ps
|
||||
|
||||
r examples/s444.blif
|
||||
b
|
||||
esd -v
|
||||
dsd
|
||||
cec
|
||||
ps
|
||||
|
||||
r examples/i10.blif
|
||||
fpga
|
||||
cec
|
||||
ps
|
||||
u
|
||||
map
|
||||
cec
|
||||
ps
|
||||
|
||||
r examples/i10.blif
|
||||
b
|
||||
fraig_store
|
||||
resyn
|
||||
fraig_store
|
||||
resyn2
|
||||
fraig_store
|
||||
fraig_restore
|
||||
fpga
|
||||
cec
|
||||
ps
|
||||
|
||||
u
|
||||
map
|
||||
cec
|
||||
ps
|
||||
|
||||
time
|
||||
|
|
|
|||
|
|
@ -1,75 +1,110 @@
|
|||
UC Berkeley, ABC 1.01 (compiled Dec 25 2006 17:15:00)
|
||||
UC Berkeley, ABC 1.01 (compiled Sep 5 2005 23:36:08)
|
||||
abc 01> so regtest.script
|
||||
abc - > r examples/apex4.pla; resyn; if; cec; ps; clp; resyn; map; cec; ps
|
||||
Networks are equivalent.
|
||||
examples/apex4: i/o = 9/ 19 lat = 0 nd = 1172 aig = 4365 lev = 7
|
||||
The shared BDD size is 917 nodes. BDD construction time = 0.04 sec
|
||||
abc - > r examples/apex4.pla
|
||||
abc - > resyn
|
||||
abc - > sharem
|
||||
abc - > fpga
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
examples/apex4.pla: i/o = 9/ 19 lat = 0 nd = 784 cube = 1985 lev = 5
|
||||
abc - >
|
||||
abc - > clp
|
||||
The shared BDD size is 917 nodes.
|
||||
abc - > share
|
||||
abc - > resyn
|
||||
abc - > map
|
||||
A simple supergate library is derived from gate library "mcnc_temp.genlib".
|
||||
Loaded 20 unique 5-input supergates from "mcnc_temp.super". Time = 0.02 sec
|
||||
Networks are equivalent.
|
||||
examples/apex4: i/o = 9/ 19 lat = 0 nd = 1734 aig = 2576 lev = 12
|
||||
abc - > r examples/C2670.blif; st; w 1.aig; cec 1.aig
|
||||
Networks are equivalent after structural hashing.
|
||||
abc - > r examples/C2670.blif; st; short_names; w 1.bench; cec 1.bench
|
||||
Networks are equivalent after structural hashing.
|
||||
abc - > r examples/C2670.blif; st; short_names; ren -s; w 1.eqn; cec 1.eqn
|
||||
Networks are equivalent.
|
||||
abc - > r examples/C2670.blif; resyn2; if -K 8; cec; ps; u; map; cec; ps
|
||||
Networks are equivalent.
|
||||
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 120 aig = 1056 lev = 4
|
||||
Networks are equivalent.
|
||||
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 467 aig = 651 lev = 14
|
||||
abc - > r examples/frg2.blif; dsd; muxes; cec; ps; clp; share; resyn; map; cec; ps
|
||||
Networks are equivalent.
|
||||
frg2 : i/o = 143/ 139 lat = 0 nd = 1648 aig = 2268 lev = 18
|
||||
The shared BDD size is 1672 nodes. BDD construction time = 0.14 sec
|
||||
Networks are equivalent.
|
||||
frg2 : i/o = 143/ 139 lat = 0 nd = 533 aig = 778 lev = 8
|
||||
abc - > r examples/frg2.blif; bdd; muxes; cec; ps; clp; st; ren -b; muxes; cec; ps
|
||||
Networks are equivalent.
|
||||
frg2 : i/o = 143/ 139 lat = 0 nd = 2868 aig = 4221 lev = 38
|
||||
The shared BDD size is 1684 nodes. BDD construction time = 0.14 sec
|
||||
Networks are equivalent.
|
||||
frg2 : i/o = 143/ 139 lat = 0 nd = 2331 aig = 3180 lev = 20
|
||||
abc - > r examples/i10.blif; resyn2; fpga; cec; ps; u; map; cec; ps
|
||||
Networks are equivalent.
|
||||
i10 : i/o = 257/ 224 lat = 0 nd = 808 aig = 2630 lev = 12
|
||||
Networks are equivalent.
|
||||
i10 : i/o = 257/ 224 lat = 0 nd = 1555 aig = 1980 lev = 24
|
||||
abc - > r examples/i10.blif; choice; fpga; cec; ps; u; map; cec; ps
|
||||
Currently stored 3 networks with 5801 nodes will be fraiged.
|
||||
Total fraiging time = 0.39 sec
|
||||
Performing FPGA mapping with choices.
|
||||
Networks are equivalent.
|
||||
i10 : i/o = 257/ 224 lat = 0 nd = 798 aig = 2543 lev = 12
|
||||
Performing mapping with choices.
|
||||
Networks are equivalent.
|
||||
i10 : i/o = 257/ 224 lat = 0 nd = 1463 aig = 1993 lev = 23
|
||||
abc - > r examples/pj1.blif; st; if; cec; ps; u; map; cec; ps
|
||||
Networks are equivalent after structural hashing.
|
||||
exCombCkt : i/o = 1769/1063 lat = 0 nd = 5984 aig = 23156 lev = 52
|
||||
Networks are equivalent.
|
||||
exCombCkt : i/o = 1769/1063 lat = 0 nd = 11474 aig = 16032 lev = 80
|
||||
abc - > r examples/s38417.blif; comb; w 1.blif; resyn; if; cec 1.blif; ps
|
||||
examples/s38417.blif (line 14): Skipping directive ".wire_load_slope".
|
||||
Networks are equivalent.
|
||||
s38417 : i/o = 1664/1742 lat = 0 nd = 3479 aig = 10120 lev = 9
|
||||
abc - > r examples/s38417.blif; resyn; if; cec; ps; u; map; cec; ps
|
||||
examples/s38417.blif (line 14): Skipping directive ".wire_load_slope".
|
||||
examples/s38417.blif (line 14): Skipping directive ".wire_load_slope".
|
||||
Networks are equivalent.
|
||||
s38417 : i/o = 28/ 106 lat = 1636 nd = 3479 aig = 10120 lev = 9
|
||||
examples/s38417.blif (line 14): Skipping directive ".wire_load_slope".
|
||||
Networks are equivalent.
|
||||
s38417 : i/o = 28/ 106 lat = 1636 nd = 7189 aig = 8689 lev = 17
|
||||
abc - > r examples/s38584.bench; resyn; ren -s; fx; if; cec; ps; u; map; cec; ps
|
||||
The network was strashed and balanced before FPGA mapping.
|
||||
Networks are equivalent.
|
||||
examples/s38584: i/o = 12/ 278 lat = 1452 nd = 4266 aig = 12569 lev = 10
|
||||
The network was strashed and balanced before mapping.
|
||||
Networks are equivalent.
|
||||
examples/s38584: i/o = 12/ 278 lat = 1452 nd = 8135 aig = 10674 lev = 18
|
||||
abc - > r examples/s444.blif; b; esd -v; print_exdc; dsd; cec; ps
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
examples/apex4.pla: i/o = 9/ 19 lat = 0 nd = 1816 area = 4599.00 delay = 11.50 lev = 11
|
||||
abc - >
|
||||
abc - > r examples/C2670.blif
|
||||
abc - > resyn
|
||||
abc - > fpga
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 169 cube = 482 lev = 6
|
||||
abc - >
|
||||
abc - > u
|
||||
abc - > map
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
C2670.iscas : i/o = 233/ 140 lat = 0 nd = 465 area = 1142.00 delay = 15.50 lev = 14
|
||||
abc - >
|
||||
abc - > r examples/frg2.blif
|
||||
abc - > dsd
|
||||
abc - > muxes
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > clp
|
||||
The shared BDD size is 1111 nodes.
|
||||
abc - > share
|
||||
abc - > resyn
|
||||
abc - > map
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
frg2 : i/o = 143/ 139 lat = 0 nd = 540 area = 1360.00 delay = 10.10 lev = 9
|
||||
abc - >
|
||||
abc - > r examples/pj1.blif
|
||||
abc - > resyn
|
||||
abc - > fpga
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
exCombCkt : i/o = 1769/1063 lat = 0 nd = 4730 cube = 10662 lev = 12
|
||||
abc - >
|
||||
abc - > u
|
||||
abc - > map
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
exCombCkt : i/o = 1769/1063 lat = 0 nd = 10396 area = 25170.00 delay = 29.20 lev = 27
|
||||
abc - >
|
||||
abc - > r examples/s38584.bench
|
||||
abc - > resyn
|
||||
The network has 26 self-feeding latches.
|
||||
abc - > fpga
|
||||
abc - > cec
|
||||
The network has 26 self-feeding latches.
|
||||
The network has 26 self-feeding latches.
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
examples/s38584.bench: i/o = 12/ 278 lat = 1452 nd = 3239 cube = 6769 lev = 7
|
||||
abc - >
|
||||
abc - > u
|
||||
abc - > map
|
||||
The network has 26 self-feeding latches.
|
||||
abc - > cec
|
||||
The network has 26 self-feeding latches.
|
||||
The network has 26 self-feeding latches.
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
examples/s38584.bench: i/o = 12/ 278 lat = 1452 nd = 8522 area = 19305.00 delay = 20.60 lev = 17
|
||||
abc - >
|
||||
abc - > r examples/ac.v
|
||||
abc - > resyn
|
||||
abc - > fpga
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
ac97_ctrl : i/o = 84/ 48 lat = 2199 nd = 3652 cube = 9391 lev = 3
|
||||
abc - >
|
||||
abc - > u
|
||||
abc - > map
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
ac97_ctrl : i/o = 84/ 48 lat = 2199 nd = 8337 area = 19861.00 delay = 8.10 lev = 8
|
||||
abc - >
|
||||
abc - > r examples/s444.blif
|
||||
abc - > b
|
||||
abc - > esd -v
|
||||
The shared BDD size is 181 nodes.
|
||||
BDD nodes in the transition relation before reordering 557.
|
||||
BDD nodes in the transition relation after reordering 456.
|
||||
|
|
@ -77,20 +112,54 @@ Reachability analysis completed in 151 iterations.
|
|||
The number of minterms in the reachable state set = 8865.
|
||||
BDD nodes in the unreachable states before reordering 124.
|
||||
BDD nodes in the unreachable states after reordering 113.
|
||||
EXDC network statistics:
|
||||
exdc : i/o = 21/ 21 lat = 0 nd = 21 cube = 86 lev = 2
|
||||
Networks are equivalent.
|
||||
s444 : i/o = 3/ 6 lat = 21 nd = 82 aig = 176 lev = 7
|
||||
abc - > r examples/s444.blif; double; frames -F 5; w 1.blif; ffpga -K 8; cec 1.blif
|
||||
Networks are equivalent after structural hashing.
|
||||
abc - > r examples/s5378.blif; frames -F 5; cycle; w 1.blif; ps; ret; ps; sec 1.blif
|
||||
s5378_5_frames: i/o = 175/ 245 lat = 164 and = 6629 (exor = 115) lev = 59
|
||||
s5378_5_frames: i/o = 175/ 245 lat = 182 nd = 6957 cube = 6956 lev = 50
|
||||
Networks are equivalent after framing.
|
||||
abc - > r examples/s6669.blif; cycle; w 1.blif; ps; ret -M 3; resyn; ps; sec 1.blif
|
||||
s6669 : i/o = 83/ 55 lat = 239 nd = 3080 cube = 3080 lev = 93
|
||||
s6669 : i/o = 83/ 55 lat = 183 and = 1915 (exor = 371) lev = 97
|
||||
abc - > dsd
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > time
|
||||
elapse: 44.07 seconds, total: 44.07 seconds
|
||||
abc 150>
|
||||
abc - > ps
|
||||
iscas\s444.bench: i/o = 3/ 6 lat = 21 nd = 81 cube = 119 lev = 7
|
||||
abc - >
|
||||
abc - > r examples/i10.blif
|
||||
abc - > fpga
|
||||
The network was strashed and balanced before FPGA mapping.
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
i10 : i/o = 257/ 224 lat = 0 nd = 741 cube = 1616 lev = 11
|
||||
abc - > u
|
||||
abc - > map
|
||||
The network was strashed and balanced before mapping.
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
i10 : i/o = 257/ 224 lat = 0 nd = 1659 area = 4215.00 delay = 30.80 lev = 27
|
||||
abc - >
|
||||
abc - > r examples/i10.blif
|
||||
abc - > b
|
||||
abc - > fraig_store
|
||||
The number of AIG nodes added to storage = 2425.
|
||||
abc - > resyn
|
||||
abc - > fraig_store
|
||||
The number of AIG nodes added to storage = 1678.
|
||||
abc - > resyn2
|
||||
abc - > fraig_store
|
||||
The number of AIG nodes added to storage = 1323.
|
||||
abc - > fraig_restore
|
||||
Currently stored 3 networks with 5426 nodes will be fraiged.
|
||||
abc - > fpga
|
||||
Performing FPGA mapping with choices.
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
i10 : i/o = 257/ 224 lat = 0 nd = 674 cube = 1498 lev = 10
|
||||
abc - >
|
||||
abc - > u
|
||||
abc - > map
|
||||
Performing mapping with choices.
|
||||
abc - > cec
|
||||
Networks are equivalent after fraiging.
|
||||
abc - > ps
|
||||
i10 : i/o = 257/ 224 lat = 0 nd = 1505 area = 3561.00 delay = 25.00 lev = 22
|
||||
abc - >
|
||||
abc 109> time
|
||||
elapse: 77.52 seconds, total: 77.52 seconds
|
||||
abc 109>
|
||||
|
|
@ -35,7 +35,7 @@ extern "C" {
|
|||
#include <assert.h>
|
||||
#include <time.h>
|
||||
|
||||
#include "vec.h"
|
||||
#include "vec2.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
|
|
@ -19,7 +19,7 @@
|
|||
***********************************************************************/
|
||||
|
||||
#include "aig.h"
|
||||
#include "tim.h"
|
||||
//#include "tim.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -277,8 +277,8 @@ void Aig_ManStop( Aig_Man_t * p )
|
|||
if ( p->time1 ) { PRT( "time1", p->time1 ); }
|
||||
if ( p->time2 ) { PRT( "time2", p->time2 ); }
|
||||
// delete timing
|
||||
if ( p->pManTime )
|
||||
Tim_ManStop( p->pManTime );
|
||||
// if ( p->pManTime )
|
||||
// Tim_ManStop( p->pManTime );
|
||||
// delete fanout
|
||||
if ( p->pFanData )
|
||||
Aig_ManFanoutStop( p );
|
||||
|
|
@ -3,7 +3,6 @@ SRC += src/aig/aig/aigCheck.c \
|
|||
src/aig/aig/aigFanout.c \
|
||||
src/aig/aig/aigFrames.c \
|
||||
src/aig/aig/aigHaig.c \
|
||||
src/aig/aig/aigInter.c \
|
||||
src/aig/aig/aigMan.c \
|
||||
src/aig/aig/aigMem.c \
|
||||
src/aig/aig/aigMffc.c \
|
||||
|
|
@ -16,7 +15,6 @@ SRC += src/aig/aig/aigCheck.c \
|
|||
src/aig/aig/aigRetF.c \
|
||||
src/aig/aig/aigScl.c \
|
||||
src/aig/aig/aigSeq.c \
|
||||
src/aig/aig/aigShow.c \
|
||||
src/aig/aig/aigTable.c \
|
||||
src/aig/aig/aigTiming.c \
|
||||
src/aig/aig/aigTruth.c \
|
||||
|
|
@ -1,6 +1,5 @@
|
|||
SRC += src/sat/bsat/satMem.c \
|
||||
src/sat/bsat/satInter.c \
|
||||
src/sat/bsat/satInterA.c \
|
||||
src/sat/bsat/satSolver.c \
|
||||
src/sat/bsat/satStore.c \
|
||||
src/sat/bsat/satTrace.c \
|
||||
|
|
@ -35,7 +35,7 @@ extern "C" {
|
|||
#include <assert.h>
|
||||
#include <time.h>
|
||||
|
||||
#include "vec.h"
|
||||
#include "vec2.h"
|
||||
#include "aig.h"
|
||||
#include "darInt.h"
|
||||
|
||||
|
|
@ -361,8 +361,10 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
|
|||
Number = 1;
|
||||
if ( nOutputs )
|
||||
{
|
||||
assert( nOutputs == Aig_ManRegNum(p) );
|
||||
Aig_ManForEachLiSeq( p, pObj, i )
|
||||
// assert( nOutputs == Aig_ManRegNum(p) );
|
||||
// Aig_ManForEachLiSeq( p, pObj, i )
|
||||
// pCnf->pVarNums[pObj->Id] = Number++;
|
||||
Aig_ManForEachPo( p, pObj, i )
|
||||
pCnf->pVarNums[pObj->Id] = Number++;
|
||||
}
|
||||
// assign variables to the internal nodes
|
||||
|
|
@ -36,7 +36,7 @@ extern "C" {
|
|||
#include <time.h>
|
||||
|
||||
//#include "bar.h"
|
||||
#include "vec.h"
|
||||
#include "vec2.h"
|
||||
#include "aig.h"
|
||||
#include "dar.h"
|
||||
|
||||
|
|
@ -18,8 +18,8 @@
|
|||
|
||||
***********************************************************************/
|
||||
|
||||
#include "darInt.h"
|
||||
#include "kit.h"
|
||||
#include "darInt.h"
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -35,7 +35,7 @@ extern "C" {
|
|||
#include <assert.h>
|
||||
#include <time.h>
|
||||
|
||||
#include "vec.h"
|
||||
#include "vec2.h"
|
||||
#include "aig.h"
|
||||
#include "dar.h"
|
||||
#include "satSolver.h"
|
||||
|
|
@ -38,6 +38,7 @@ struct Clu_Man_t_
|
|||
int nCutsMax; // the maximum number of cuts to compute at a node
|
||||
int nBatches; // the number of clause batches to use
|
||||
int fStepUp; // increase cut size for each batch
|
||||
int fTarget; // tries to prove the property
|
||||
int fVerbose;
|
||||
int fVeryVerbose;
|
||||
// internal parameters
|
||||
|
|
@ -60,6 +61,9 @@ struct Clu_Man_t_
|
|||
Vec_Int_t * vClauses;
|
||||
Vec_Int_t * vCosts;
|
||||
int nClauses;
|
||||
int nCuts;
|
||||
int nOneHots;
|
||||
int nOneHotsProven;
|
||||
// clauses proven
|
||||
Vec_Int_t * vLitsProven;
|
||||
Vec_Int_t * vClausesProven;
|
||||
|
|
@ -283,9 +287,11 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
|
|||
***********************************************************************/
|
||||
void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t * pCut, int * pScores )
|
||||
{
|
||||
unsigned * pSims[16];
|
||||
int iMint, i, k, b, nMints;
|
||||
unsigned Matrix[32];
|
||||
unsigned * pSims[16], uWord;
|
||||
int iMint, i, j, k, b, nMints, nSeries;
|
||||
int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
|
||||
|
||||
// compute parameters
|
||||
assert( pCut->nFanins > 1 && pCut->nFanins < 17 );
|
||||
assert( nWordsForSim % 8 == 0 );
|
||||
|
|
@ -295,16 +301,36 @@ void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t
|
|||
// add combinational patterns
|
||||
nMints = (1 << pCut->nFanins);
|
||||
memset( pScores, 0, sizeof(int) * nMints );
|
||||
// go through the simulation patterns
|
||||
for ( i = 0; i < nWordsForSim; i++ )
|
||||
for ( k = 0; k < 32; k++ )
|
||||
|
||||
if ( pCut->nLeafMax == 4 )
|
||||
{
|
||||
// convert the simulation patterns
|
||||
nSeries = nWordsForSim / 8;
|
||||
for ( i = 0; i < nSeries; i++ )
|
||||
{
|
||||
iMint = 0;
|
||||
for ( b = 0; b < (int)pCut->nFanins; b++ )
|
||||
if ( pSims[b][i] & (1 << k) )
|
||||
iMint |= (1 << b);
|
||||
pScores[iMint]++;
|
||||
memset( Matrix, 0, sizeof(unsigned) * 32 );
|
||||
for ( k = 0; k < 8; k++ )
|
||||
for ( j = 0; j < (int)pCut->nFanins; j++ )
|
||||
Matrix[31-(k*4+j)] = pSims[j][i*8+k];
|
||||
transpose32a( Matrix );
|
||||
for ( k = 0; k < 32; k++ )
|
||||
for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
|
||||
pScores[uWord & 0xF]++;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// go through the simulation patterns
|
||||
for ( i = 0; i < nWordsForSim; i++ )
|
||||
for ( k = 0; k < 32; k++ )
|
||||
{
|
||||
iMint = 0;
|
||||
for ( b = 0; b < (int)pCut->nFanins; b++ )
|
||||
if ( pSims[b][i] & (1 << k) )
|
||||
iMint |= (1 << b);
|
||||
pScores[iMint]++;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -538,7 +564,9 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
|
|||
}
|
||||
pSeq->nWordsPref = 0;
|
||||
if ( p->fVerbose )
|
||||
printf( "Collected %d constants and %d implications.\n", nCountConst, nCountImps );
|
||||
printf( "Collected %d register constants and %d one-hotness implications.\n", nCountConst, nCountImps );
|
||||
p->nOneHots = nCountConst + nCountImps;
|
||||
p->nOneHotsProven = 0;
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
|
@ -566,7 +594,7 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
|
|||
clk = clock();
|
||||
srand( 0xAABBAABB );
|
||||
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
|
||||
if ( pSeq->fNonConstOut )
|
||||
if ( p->fTarget && pSeq->fNonConstOut )
|
||||
{
|
||||
printf( "Property failed after sequential simulation!\n" );
|
||||
Fra_SmlStop( pSeq );
|
||||
|
|
@ -688,7 +716,7 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
|
|||
clk = clock();
|
||||
srand( 0xAABBAABB );
|
||||
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
|
||||
if ( pSeq->fNonConstOut )
|
||||
if ( p->fTarget && pSeq->fNonConstOut )
|
||||
{
|
||||
printf( "Property failed after sequential simulation!\n" );
|
||||
Fra_SmlStop( pSeq );
|
||||
|
|
@ -696,7 +724,7 @@ clk = clock();
|
|||
}
|
||||
if ( p->fVerbose )
|
||||
{
|
||||
PRT( "Sim-seq", clock() - clk );
|
||||
//PRT( "Sim-seq", clock() - clk );
|
||||
}
|
||||
|
||||
// perform combinational simulation
|
||||
|
|
@ -705,7 +733,7 @@ clk = clock();
|
|||
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
|
||||
if ( p->fVerbose )
|
||||
{
|
||||
PRT( "Sim-cmb", clock() - clk );
|
||||
//PRT( "Sim-cmb", clock() - clk );
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -715,7 +743,7 @@ clk = clock();
|
|||
Fra_ClausCollectLatchClauses( p, pSeq );
|
||||
if ( p->fVerbose )
|
||||
{
|
||||
PRT( "Lat-cla", clock() - clk );
|
||||
//PRT( "Lat-cla", clock() - clk );
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -726,7 +754,7 @@ clk = clock();
|
|||
pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
|
||||
if ( p->fVerbose )
|
||||
{
|
||||
PRT( "Cuts ", clock() - clk );
|
||||
//PRT( "Cuts ", clock() - clk );
|
||||
}
|
||||
|
||||
// collect combinational info for each cut
|
||||
|
|
@ -750,17 +778,17 @@ clk = clock();
|
|||
}
|
||||
Fra_SmlStop( pSeq );
|
||||
Fra_SmlStop( pComb );
|
||||
p->nCuts = nCuts;
|
||||
// Aig_MmFixedStop( pMemCuts, 0 );
|
||||
Aig_ManCutStop( pManCut );
|
||||
p->pAig->pManCuts = NULL;
|
||||
if ( p->fVerbose )
|
||||
{
|
||||
PRT( "Infosim", clock() - clk );
|
||||
}
|
||||
|
||||
if ( p->fVerbose )
|
||||
printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n",
|
||||
{
|
||||
printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n",
|
||||
Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
|
||||
PRT( "Processing sim-info to find candidate clauses (unoptimized)", clock() - clk );
|
||||
}
|
||||
|
||||
// filter out clauses that are contained in the already proven clauses
|
||||
assert( p->nClauses == 0 );
|
||||
|
|
@ -1168,17 +1196,20 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
|
|||
}
|
||||
|
||||
// check if the property holds
|
||||
if ( Fra_ClausRunSat0( p ) )
|
||||
if ( p->fTarget )
|
||||
{
|
||||
if ( p->fVerbose )
|
||||
printf( " Property holds. " );
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( p->fVerbose )
|
||||
printf( " Property fails. " );
|
||||
// return -2;
|
||||
p->fFail = 1;
|
||||
if ( Fra_ClausRunSat0( p ) )
|
||||
{
|
||||
if ( p->fVerbose )
|
||||
printf( " Property holds. " );
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( p->fVerbose )
|
||||
printf( " Property fails. " );
|
||||
// return -2;
|
||||
p->fFail = 1;
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
|
|
@ -1305,7 +1336,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fVerbose, int fVeryVerbose )
|
||||
Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose )
|
||||
{
|
||||
Clu_Man_t * p;
|
||||
p = ALLOC( Clu_Man_t, 1 );
|
||||
|
|
@ -1319,6 +1350,7 @@ Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClaus
|
|||
p->nCutsMax = nCutsMax;
|
||||
p->nBatches = nBatches;
|
||||
p->fStepUp = fStepUp;
|
||||
p->fTarget = fTarget;
|
||||
p->fVerbose = fVerbose;
|
||||
p->fVeryVerbose = fVeryVerbose;
|
||||
p->nSimWords = 512;//1024;//64;
|
||||
|
|
@ -1396,9 +1428,12 @@ void Fra_ClausAddToStorage( Clu_Man_t * p )
|
|||
Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) );
|
||||
Beg = End;
|
||||
Counter++;
|
||||
|
||||
if ( i < p->nOneHots )
|
||||
p->nOneHotsProven++;
|
||||
}
|
||||
if ( p->fVerbose )
|
||||
printf( "Added to storage %d proved clauses\n", Counter );
|
||||
printf( "Added to storage %d proved clauses (including %d one-hot clauses)\n", Counter, p->nOneHotsProven );
|
||||
|
||||
Vec_IntClear( p->vClauses );
|
||||
Vec_IntClear( p->vLits );
|
||||
|
|
@ -1419,25 +1454,160 @@ void Fra_ClausAddToStorage( Clu_Man_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
|
||||
void Fra_ClausPrintIndClauses( Clu_Man_t * p )
|
||||
{
|
||||
int Counters[9] = {0};
|
||||
int * pStart;
|
||||
int Beg, End, i;
|
||||
Beg = 0;
|
||||
pStart = Vec_IntArray( p->vLitsProven );
|
||||
Vec_IntForEachEntry( p->vClausesProven, End, i )
|
||||
{
|
||||
if ( End - Beg >= 8 )
|
||||
Counters[8]++;
|
||||
else
|
||||
Counters[End - Beg]++;
|
||||
//printf( "%d ", End-Beg );
|
||||
Beg = End;
|
||||
}
|
||||
printf( "SUMMARY: Total proved clauses = %d. ", Vec_IntSize(p->vClausesProven) );
|
||||
printf( "Clause per lit: " );
|
||||
for ( i = 0; i < 8; i++ )
|
||||
if ( Counters[i] )
|
||||
printf( "%d=%d ", i, Counters[i] );
|
||||
if ( Counters[8] )
|
||||
printf( ">7=%d ", Counters[8] );
|
||||
printf( "\n" );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Checks if the clause holds using the given simulation info.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Fra_ClausEstimateCoverageOne( Fra_Sml_t * pSim, int * pLits, int nLits, int * pVar2Id, unsigned * pResult )
|
||||
{
|
||||
unsigned * pSims[16];
|
||||
int iVar, i, w;
|
||||
for ( i = 0; i < nLits; i++ )
|
||||
{
|
||||
iVar = lit_var(pLits[i]);
|
||||
pSims[i] = Fra_ObjSim( pSim, pVar2Id[iVar] );
|
||||
}
|
||||
for ( w = 0; w < pSim->nWordsTotal; w++ )
|
||||
{
|
||||
pResult[w] = ~(unsigned)0;
|
||||
for ( i = 0; i < nLits; i++ )
|
||||
pResult[w] &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Estimates the coverage of state space by clauses.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Fra_ClausEstimateCoverage( Clu_Man_t * p )
|
||||
{
|
||||
int nCombSimWords = (1<<11);
|
||||
Fra_Sml_t * pComb;
|
||||
unsigned * pResultTot, * pResultOne;
|
||||
int nCovered, Beg, End, i, w;
|
||||
int * pStart, * pVar2Id;
|
||||
int clk = clock();
|
||||
// simulate the circuit with nCombSimWords * 32 = 64K patterns
|
||||
srand( 0xAABBAABB );
|
||||
pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords );
|
||||
// create mapping from SAT vars to node IDs
|
||||
pVar2Id = ALLOC( int, p->pCnf->nVars );
|
||||
memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars );
|
||||
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
|
||||
if ( p->pCnf->pVarNums[i] >= 0 )
|
||||
{
|
||||
assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
|
||||
pVar2Id[ p->pCnf->pVarNums[i] ] = i;
|
||||
}
|
||||
// get storage for one assignment and all assignments
|
||||
assert( Aig_ManPoNum(p->pAig) > 2 );
|
||||
pResultOne = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 0)->Id );
|
||||
pResultTot = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 1)->Id );
|
||||
// start the OR of don't-cares
|
||||
for ( w = 0; w < nCombSimWords; w++ )
|
||||
pResultTot[w] = 0;
|
||||
// check clauses
|
||||
Beg = 0;
|
||||
pStart = Vec_IntArray( p->vLitsProven );
|
||||
Vec_IntForEachEntry( p->vClausesProven, End, i )
|
||||
{
|
||||
Fra_ClausEstimateCoverageOne( pComb, pStart + Beg, End-Beg, pVar2Id, pResultOne );
|
||||
Beg = End;
|
||||
for ( w = 0; w < nCombSimWords; w++ )
|
||||
pResultTot[w] |= pResultOne[w];
|
||||
}
|
||||
// count the total number of patterns contained in the don't-care
|
||||
nCovered = 0;
|
||||
for ( w = 0; w < nCombSimWords; w++ )
|
||||
nCovered += Aig_WordCountOnes( pResultTot[w] );
|
||||
Fra_SmlStop( pComb );
|
||||
free( pVar2Id );
|
||||
// print the result
|
||||
printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) );
|
||||
printf( "(%d out of %d patterns) ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 );
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Converts AIG into the SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
|
||||
{
|
||||
Clu_Man_t * p;
|
||||
int clk, clkTotal = clock();
|
||||
int clk, clkTotal = clock(), clkInd;
|
||||
int b, Iter, Counter, nPrefOld;
|
||||
|
||||
assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
|
||||
int nClausesBeg = 0;
|
||||
|
||||
// create the manager
|
||||
p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fVerbose, fVeryVerbose );
|
||||
p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fTarget, fVerbose, fVeryVerbose );
|
||||
if ( p->fVerbose )
|
||||
{
|
||||
printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize );
|
||||
printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" );
|
||||
//PRT( "Sim-seq", clock() - clk );
|
||||
}
|
||||
|
||||
assert( !p->fTarget || Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
|
||||
|
||||
clk = clock();
|
||||
// derive CNF
|
||||
p->pAig->nRegs++;
|
||||
if ( p->fTarget )
|
||||
p->pAig->nRegs++;
|
||||
p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
|
||||
p->pAig->nRegs--;
|
||||
if ( p->fTarget )
|
||||
p->pAig->nRegs--;
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "CNF ", clock() - clk );
|
||||
//PRT( "CNF ", clock() - clk );
|
||||
}
|
||||
|
||||
// check BMC
|
||||
|
|
@ -1449,7 +1619,7 @@ clk = clock();
|
|||
Fra_ClausFree( p );
|
||||
return 1;
|
||||
}
|
||||
if ( !Fra_ClausRunBmc( p ) )
|
||||
if ( p->fTarget && !Fra_ClausRunBmc( p ) )
|
||||
{
|
||||
printf( "Problem fails the base case after %d frame expansion.\n", p->nPref + p->nFrames );
|
||||
Fra_ClausFree( p );
|
||||
|
|
@ -1457,7 +1627,7 @@ clk = clock();
|
|||
}
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "SAT-bmc", clock() - clk );
|
||||
//PRT( "SAT-bmc", clock() - clk );
|
||||
}
|
||||
|
||||
// start the SAT solver
|
||||
|
|
@ -1475,12 +1645,12 @@ clk = clock();
|
|||
{
|
||||
// if ( fVerbose )
|
||||
printf( "*** BATCH %d: ", b+1 );
|
||||
if ( b && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
|
||||
if ( b && p->nLutSize < 12 && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
|
||||
p->nLutSize++;
|
||||
printf( "Using %d-cuts.\n", p->nLutSize );
|
||||
|
||||
// try solving without additional clauses
|
||||
if ( Fra_ClausRunSat( p ) )
|
||||
if ( p->fTarget && Fra_ClausRunSat( p ) )
|
||||
{
|
||||
printf( "Problem is inductive without strengthening.\n" );
|
||||
Fra_ClausFree( p );
|
||||
|
|
@ -1488,7 +1658,7 @@ clk = clock();
|
|||
}
|
||||
if ( fVerbose )
|
||||
{
|
||||
PRT( "SAT-ind", clock() - clk );
|
||||
// PRT( "SAT-ind", clock() - clk );
|
||||
}
|
||||
|
||||
// collect the candidate inductive clauses using 4-cuts
|
||||
|
|
@ -1498,6 +1668,7 @@ clk = clock();
|
|||
Fra_ClausProcessClauses2( p, fRefs );
|
||||
p->nPref = nPrefOld;
|
||||
p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
|
||||
nClausesBeg = p->nClauses;
|
||||
|
||||
//PRT( "Clauses", clock() - clk );
|
||||
|
||||
|
|
@ -1510,14 +1681,14 @@ clk = clock();
|
|||
p->nClauses -= Counter;
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "BMC disproved %d clauses.\n", Counter );
|
||||
PRT( "Cla-bmc", clock() - clk );
|
||||
printf( "BMC disproved %d clauses. ", Counter );
|
||||
PRT( "Time", clock() - clk );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// prove clauses inductively
|
||||
clk = clock();
|
||||
clkInd = clk = clock();
|
||||
Counter = 1;
|
||||
for ( Iter = 0; Counter > 0; Iter++ )
|
||||
{
|
||||
|
|
@ -1534,21 +1705,55 @@ clk = clock();
|
|||
}
|
||||
clk = clock();
|
||||
}
|
||||
if ( Counter == -1 )
|
||||
printf( "Fra_Claus(): Internal error. " );
|
||||
else if ( p->fFail )
|
||||
printf( "Property FAILS during refinement. " );
|
||||
if ( p->fTarget )
|
||||
{
|
||||
if ( Counter == -1 )
|
||||
printf( "Fra_Claus(): Internal error. " );
|
||||
else if ( p->fFail )
|
||||
printf( "Property FAILS during refinement. " );
|
||||
else
|
||||
printf( "Property HOLDS inductively after strengthening. " );
|
||||
PRT( "Time ", clock() - clkTotal );
|
||||
if ( !p->fFail )
|
||||
break;
|
||||
}
|
||||
else
|
||||
printf( "Property HOLDS inductively after strengthening. " );
|
||||
PRT( "Time ", clock() - clkTotal );
|
||||
|
||||
if ( !p->fFail )
|
||||
break;
|
||||
{
|
||||
printf( "Finished proving inductive clauses. " );
|
||||
PRT( "Time ", clock() - clkTotal );
|
||||
}
|
||||
|
||||
// add proved clauses to storage
|
||||
Fra_ClausAddToStorage( p );
|
||||
}
|
||||
|
||||
if ( !p->fTarget && p->fVerbose )
|
||||
{
|
||||
Fra_ClausPrintIndClauses( p );
|
||||
Fra_ClausEstimateCoverage( p );
|
||||
}
|
||||
/*
|
||||
// print the statistic into a file
|
||||
{
|
||||
FILE * pTable;
|
||||
assert( p->nBatches == 1 );
|
||||
pTable = fopen( "stats.txt", "a+" );
|
||||
fprintf( pTable, "%s ", pAig->pName );
|
||||
fprintf( pTable, "%d ", Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig) );
|
||||
fprintf( pTable, "%d ", Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig) );
|
||||
fprintf( pTable, "%d ", Aig_ManRegNum(pAig) );
|
||||
fprintf( pTable, "%d ", Aig_ManNodeNum(pAig) );
|
||||
fprintf( pTable, "%d ", p->nCuts );
|
||||
fprintf( pTable, "%d ", nClausesBeg );
|
||||
fprintf( pTable, "%d ", p->nClauses );
|
||||
fprintf( pTable, "%d ", Iter );
|
||||
fprintf( pTable, "%.2f ", (float)(clkInd-clkTotal)/(float)(CLOCKS_PER_SEC) );
|
||||
fprintf( pTable, "%.2f ", (float)(clock()-clkInd)/(float)(CLOCKS_PER_SEC) );
|
||||
fprintf( pTable, "%.2f ", (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC) );
|
||||
fprintf( pTable, "\n" );
|
||||
fclose( pTable );
|
||||
}
|
||||
*/
|
||||
// clean the manager
|
||||
Fra_ClausFree( p );
|
||||
return 1;
|
||||
|
|
@ -35,7 +35,7 @@ extern "C" {
|
|||
#include <assert.h>
|
||||
#include <time.h>
|
||||
|
||||
#include "vec.h"
|
||||
#include "vec2.h"
|
||||
//#include "bar.h"
|
||||
#include "aig.h"
|
||||
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue