Version abc80130_2

This commit is contained in:
Alan Mishchenko 2008-01-30 20:01:00 -08:00
parent 4d30a1e4f1
commit 0c6505a26a
798 changed files with 156804 additions and 18465 deletions

View File

@ -6,22 +6,30 @@ CP := cp
PROG := abc
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
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
default: $(PROG)
OPTFLAGS := -DNDEBUG -O3
#OPTFLAGS := -g -O
#OPTFLAGS := -DNDEBUG -O3
OPTFLAGS := -g -O
CFLAGS += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES))
CXXFLAGS += $(CFLAGS)
LIBS :=
LIBS := -ldl -rdynamic -lreadline -ltermcap
SRC :=
GARBAGE := core core.* *.stackdump ./tags $(PROG)
@ -59,6 +67,10 @@ tags:
$(PROG): $(OBJ)
$(LD) -o $@ $^ $(LIBS)
lib$(PROG).a: $(OBJ)
ar rv $@ $?
ranlib $@
docs:
doxygen doxygen.conf

1658
abc.dsp

File diff suppressed because it is too large Load Diff

89
abc.rc
View File

@ -1,9 +1,10 @@
# 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 savesteps 1 # sets the maximum number of backup networks to save
set progressbar # display the progress bar
# program names for internal calls
set dotwin dot.exe
@ -14,6 +15,10 @@ 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
@ -22,48 +27,102 @@ 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 mu renode -m
alias lp lutpack
alias pd print_dsd
alias pex print_exdc -d
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 wb write_blif
alias w write
alias wa write_aiger
alias wb write_bench
alias wc write_cnf
alias wh write_hie
alias wl write_blif
alias wp write_pla
alias wv write_verilog
# standard scripts
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"
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 scl scleanup
alias ssw ssweep
# 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"

2844
abclib.dsp Normal file

File diff suppressed because it is too large Load Diff

29
abclib.dsw Normal file
View File

@ -0,0 +1,29 @@
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 Normal file
View File

@ -0,0 +1,102 @@
# 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

29
abctestlib.dsw Normal file
View File

@ -0,0 +1,29 @@
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>
{{{
}}}
###############################################################################

18
copyright.txt Normal file
View File

@ -0,0 +1,18 @@
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 Normal file
View File

@ -0,0 +1,181 @@
/**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 Normal file
View File

@ -0,0 +1,26 @@
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

View File

@ -1,103 +1,18 @@
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
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
time

View File

@ -1,110 +1,75 @@
UC Berkeley, ABC 1.01 (compiled Sep 5 2005 23:36:08)
UC Berkeley, ABC 1.01 (compiled Dec 25 2006 17:15:00)
abc 01> so regtest.script
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
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
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
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
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
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.
@ -112,54 +77,20 @@ 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.
abc - > dsd
abc - > cec
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
Networks are equivalent after fraiging.
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>
abc - > time
elapse: 44.07 seconds, total: 44.07 seconds
abc 150>

View File

@ -1,121 +0,0 @@
/**CFile****************************************************************
FileName [vec.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resizable arrays.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: vec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __VEC_H__
#define __VEC_H__
#ifdef __cplusplus
extern "C" {
#endif
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#pragma warning(disable : 4152) // warning C4152: nonstandard extension, function/data pointer conversion in expression
#pragma warning(disable : 4244) // warning C4244: '+=' : conversion from 'int ' to 'unsigned short ', possible loss of data
#pragma warning(disable : 4514) // warning C4514: 'Vec_StrPop' : unreferenced inline function has been removed
#pragma warning(disable : 4710) // warning C4710: function 'Vec_PtrGrow' not inlined
#endif
#ifndef SINT64
#define SINT64
#ifdef _WIN32
typedef signed __int64 sint64; // compatible with MS VS 6.0
#else
typedef long long sint64;
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
// this include should be the first one in the list
// it is used to catch memory leaks on Windows
#include "leaks.h"
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifndef ABS
#define ABS(a) ((a) < 0 ? -(a) : (a))
#endif
#ifndef MAX
#define MAX(a,b) ((a) > (b) ? (a) : (b))
#endif
#ifndef MIN
#define MIN(a,b) ((a) < (b) ? (a) : (b))
#endif
#ifndef ALLOC
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#endif
#ifndef FREE
#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
#endif
#ifndef REALLOC
#define REALLOC(type, obj, num) \
((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
((type *) malloc(sizeof(type) * (num))))
#endif
#ifndef PRT
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
#ifndef PRTP
#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)
#endif
#include "vecInt.h"
#include "vecFlt.h"
#include "vecStr.h"
#include "vecPtr.h"
#include "vecVec.h"
#include "vecAtt.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -1,834 +0,0 @@
/**CFile****************************************************************
FileName [vecInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resizable arrays.]
Synopsis [Resizable arrays of integers.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: vecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __VEC_INT_H__
#define __VEC_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Vec_Int_t_ Vec_Int_t;
struct Vec_Int_t_
{
int nCap;
int nSize;
int * pArray;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define Vec_IntForEachEntry( vVec, Entry, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
#define Vec_IntForEachEntryStart( vVec, Entry, i, Start ) \
for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
#define Vec_IntForEachEntryStartStop( vVec, Entry, i, Start, Stop ) \
for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
#define Vec_IntForEachEntryReverse( vVec, pEntry, i ) \
for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates a vector with the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntAlloc( int nCap )
{
Vec_Int_t * p;
p = ALLOC( Vec_Int_t, 1 );
if ( nCap > 0 && nCap < 16 )
nCap = 16;
p->nSize = 0;
p->nCap = nCap;
p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
return p;
}
/**Function*************************************************************
Synopsis [Allocates a vector with the given size and cleans it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntStart( int nSize )
{
Vec_Int_t * p;
p = Vec_IntAlloc( nSize );
p->nSize = nSize;
memset( p->pArray, 0, sizeof(int) * nSize );
return p;
}
/**Function*************************************************************
Synopsis [Allocates a vector with the given size and cleans it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntStartNatural( int nSize )
{
Vec_Int_t * p;
int i;
p = Vec_IntAlloc( nSize );
p->nSize = nSize;
for ( i = 0; i < nSize; i++ )
p->pArray[i] = i;
return p;
}
/**Function*************************************************************
Synopsis [Creates the vector from an integer array of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntAllocArray( int * pArray, int nSize )
{
Vec_Int_t * p;
p = ALLOC( Vec_Int_t, 1 );
p->nSize = nSize;
p->nCap = nSize;
p->pArray = pArray;
return p;
}
/**Function*************************************************************
Synopsis [Creates the vector from an integer array of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntAllocArrayCopy( int * pArray, int nSize )
{
Vec_Int_t * p;
p = ALLOC( Vec_Int_t, 1 );
p->nSize = nSize;
p->nCap = nSize;
p->pArray = ALLOC( int, nSize );
memcpy( p->pArray, pArray, sizeof(int) * nSize );
return p;
}
/**Function*************************************************************
Synopsis [Duplicates the integer array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec )
{
Vec_Int_t * p;
p = ALLOC( Vec_Int_t, 1 );
p->nSize = pVec->nSize;
p->nCap = pVec->nSize;
p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
return p;
}
/**Function*************************************************************
Synopsis [Transfers the array into another vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
{
Vec_Int_t * p;
p = ALLOC( Vec_Int_t, 1 );
p->nSize = pVec->nSize;
p->nCap = pVec->nCap;
p->pArray = pVec->pArray;
pVec->nSize = 0;
pVec->nCap = 0;
pVec->pArray = NULL;
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntFree( Vec_Int_t * p )
{
FREE( p->pArray );
FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int * Vec_IntReleaseArray( Vec_Int_t * p )
{
int * pArray = p->pArray;
p->nCap = 0;
p->nSize = 0;
p->pArray = NULL;
return pArray;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int * Vec_IntArray( Vec_Int_t * p )
{
return p->pArray;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntSize( Vec_Int_t * p )
{
return p->nSize;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntEntry( Vec_Int_t * p, int i )
{
assert( i >= 0 && i < p->nSize );
return p->pArray[i];
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry )
{
assert( i >= 0 && i < p->nSize );
p->pArray[i] = Entry;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntAddToEntry( Vec_Int_t * p, int i, int Addition )
{
assert( i >= 0 && i < p->nSize );
p->pArray[i] += Addition;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntEntryLast( Vec_Int_t * p )
{
assert( p->nSize > 0 );
return p->pArray[p->nSize-1];
}
/**Function*************************************************************
Synopsis [Resizes the vector to the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
{
if ( p->nCap >= nCapMin )
return;
p->pArray = REALLOC( int, p->pArray, nCapMin );
assert( p->pArray );
p->nCap = nCapMin;
}
/**Function*************************************************************
Synopsis [Fills the vector with given number of entries.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Entry )
{
int i;
Vec_IntGrow( p, nSize );
for ( i = 0; i < nSize; i++ )
p->pArray[i] = Entry;
p->nSize = nSize;
}
/**Function*************************************************************
Synopsis [Fills the vector with given number of entries.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
{
int i;
if ( p->nSize >= nSize )
return;
Vec_IntGrow( p, nSize );
for ( i = p->nSize; i < nSize; i++ )
p->pArray[i] = Entry;
p->nSize = nSize;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew )
{
assert( p->nSize >= nSizeNew );
p->nSize = nSizeNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntClear( Vec_Int_t * p )
{
p->nSize = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
{
if ( p->nSize == p->nCap )
{
if ( p->nCap < 16 )
Vec_IntGrow( p, 16 );
else
Vec_IntGrow( p, 2 * p->nCap );
}
p->pArray[p->nSize++] = Entry;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntPushFirst( Vec_Int_t * p, int Entry )
{
int i;
if ( p->nSize == p->nCap )
{
if ( p->nCap < 16 )
Vec_IntGrow( p, 16 );
else
Vec_IntGrow( p, 2 * p->nCap );
}
p->nSize++;
for ( i = p->nSize - 1; i >= 1; i-- )
p->pArray[i] = p->pArray[i-1];
p->pArray[0] = Entry;
}
/**Function*************************************************************
Synopsis [Inserts the entry while preserving the increasing order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
{
int i;
if ( p->nSize == p->nCap )
{
if ( p->nCap < 16 )
Vec_IntGrow( p, 16 );
else
Vec_IntGrow( p, 2 * p->nCap );
}
p->nSize++;
for ( i = p->nSize-2; i >= 0; i-- )
if ( p->pArray[i] > Entry )
p->pArray[i+1] = p->pArray[i];
else
break;
p->pArray[i+1] = Entry;
}
/**Function*************************************************************
Synopsis [Inserts the entry while preserving the increasing order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry )
{
int i;
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
return 1;
Vec_IntPushOrder( p, Entry );
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
{
int i;
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
return 1;
Vec_IntPush( p, Entry );
return 0;
}
/**Function*************************************************************
Synopsis [Returns the pointer to the next nWords entries in the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords )
{
if ( nWords == 0 )
return NULL;
assert( nWords > 0 );
p->nSize += nWords;
if ( p->nSize > p->nCap )
{
// Vec_IntGrow( p, 2 * p->nSize );
return NULL;
}
return ((unsigned *)p->pArray) + p->nSize - nWords;
}
/**Function*************************************************************
Synopsis [Returns the last entry and removes it from the list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntPop( Vec_Int_t * p )
{
assert( p->nSize > 0 );
return p->pArray[--p->nSize];
}
/**Function*************************************************************
Synopsis [Find entry.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntFind( Vec_Int_t * p, int Entry )
{
int i;
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
return i;
return -1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
{
int i;
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
break;
if ( i == p->nSize )
return 0;
assert( i < p->nSize );
for ( i++; i < p->nSize; i++ )
p->pArray[i-1] = p->pArray[i];
p->nSize--;
return 1;
}
/**Function*************************************************************
Synopsis [Comparison procedure for two integers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntSortCompare1( int * pp1, int * pp2 )
{
// for some reason commenting out lines (as shown) led to crashing of the release version
if ( *pp1 < *pp2 )
return -1;
if ( *pp1 > *pp2 ) //
return 1;
return 0; //
}
/**Function*************************************************************
Synopsis [Comparison procedure for two integers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntSortCompare2( int * pp1, int * pp2 )
{
// for some reason commenting out lines (as shown) led to crashing of the release version
if ( *pp1 > *pp2 )
return -1;
if ( *pp1 < *pp2 ) //
return 1;
return 0; //
}
/**Function*************************************************************
Synopsis [Sorting the entries by their integer value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntSort( Vec_Int_t * p, int fReverse )
{
if ( fReverse )
qsort( (void *)p->pArray, p->nSize, sizeof(int),
(int (*)(const void *, const void *)) Vec_IntSortCompare2 );
else
qsort( (void *)p->pArray, p->nSize, sizeof(int),
(int (*)(const void *, const void *)) Vec_IntSortCompare1 );
}
/**Function*************************************************************
Synopsis [Comparison procedure for two integers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntSortCompareUnsigned( unsigned * pp1, unsigned * pp2 )
{
if ( *pp1 < *pp2 )
return -1;
if ( *pp1 > *pp2 )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Sorting the entries by their integer value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntSortUnsigned( Vec_Int_t * p )
{
qsort( (void *)p->pArray, p->nSize, sizeof(int),
(int (*)(const void *, const void *)) Vec_IntSortCompareUnsigned );
}
/**Function*************************************************************
Synopsis [Returns the number of common entries.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntTwoCountCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
{
int * pBeg1 = vArr1->pArray;
int * pBeg2 = vArr2->pArray;
int * pEnd1 = vArr1->pArray + vArr1->nSize;
int * pEnd2 = vArr2->pArray + vArr2->nSize;
int Counter = 0;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( *pBeg1 == *pBeg2 )
pBeg1++, pBeg2++, Counter++;
else if ( *pBeg1 < *pBeg2 )
pBeg1++;
else
pBeg2++;
}
return Counter;
}
/**Function*************************************************************
Synopsis [Returns the result of merging the two vectors.]
Description [Assumes that the vectors are sorted in the increasing order.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Int_t * Vec_IntTwoMerge( Vec_Int_t * vArr1, Vec_Int_t * vArr2 )
{
Vec_Int_t * vArr = Vec_IntAlloc( vArr1->nSize + vArr2->nSize );
int * pBeg = vArr->pArray;
int * pBeg1 = vArr1->pArray;
int * pBeg2 = vArr2->pArray;
int * pEnd1 = vArr1->pArray + vArr1->nSize;
int * pEnd2 = vArr2->pArray + vArr2->nSize;
while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
{
if ( *pBeg1 == *pBeg2 )
*pBeg++ = *pBeg1++, pBeg2++;
else if ( *pBeg1 < *pBeg2 )
*pBeg++ = *pBeg1++;
else
*pBeg++ = *pBeg2++;
}
while ( pBeg1 < pEnd1 )
*pBeg++ = *pBeg1++;
while ( pBeg2 < pEnd2 )
*pBeg++ = *pBeg2++;
vArr->nSize = pBeg - vArr->pArray;
assert( vArr->nSize <= vArr->nCap );
assert( vArr->nSize >= vArr1->nSize );
assert( vArr->nSize >= vArr2->nSize );
return vArr;
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -1,812 +0,0 @@
/**CFile****************************************************************
FileName [vecPtr.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resizable arrays.]
Synopsis [Resizable arrays of generic pointers.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: vecPtr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __VEC_PTR_H__
#define __VEC_PTR_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Vec_Ptr_t_ Vec_Ptr_t;
struct Vec_Ptr_t_
{
int nCap;
int nSize;
void ** pArray;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// iterators through entries
#define Vec_PtrForEachEntry( vVec, pEntry, i ) \
for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
#define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start ) \
for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
#define Vec_PtrForEachEntryStop( vVec, pEntry, i, Stop ) \
for ( i = 0; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
#define Vec_PtrForEachEntryStartStop( vVec, pEntry, i, Start, Stop ) \
for ( i = Start; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
#define Vec_PtrForEachEntryReverse( vVec, pEntry, i ) \
for ( i = Vec_PtrSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i-- )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates a vector with the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAlloc( int nCap )
{
Vec_Ptr_t * p;
p = ALLOC( Vec_Ptr_t, 1 );
if ( nCap > 0 && nCap < 8 )
nCap = 8;
p->nSize = 0;
p->nCap = nCap;
p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
return p;
}
/**Function*************************************************************
Synopsis [Allocates a vector with the given size and cleans it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrStart( int nSize )
{
Vec_Ptr_t * p;
p = Vec_PtrAlloc( nSize );
p->nSize = nSize;
memset( p->pArray, 0, sizeof(void *) * nSize );
return p;
}
/**Function*************************************************************
Synopsis [Creates the vector from an integer array of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAllocArray( void ** pArray, int nSize )
{
Vec_Ptr_t * p;
p = ALLOC( Vec_Ptr_t, 1 );
p->nSize = nSize;
p->nCap = nSize;
p->pArray = pArray;
return p;
}
/**Function*************************************************************
Synopsis [Creates the vector from an integer array of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
{
Vec_Ptr_t * p;
p = ALLOC( Vec_Ptr_t, 1 );
p->nSize = nSize;
p->nCap = nSize;
p->pArray = ALLOC( void *, nSize );
memcpy( p->pArray, pArray, sizeof(void *) * nSize );
return p;
}
/**Function*************************************************************
Synopsis [Duplicates the integer array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrDup( Vec_Ptr_t * pVec )
{
Vec_Ptr_t * p;
p = ALLOC( Vec_Ptr_t, 1 );
p->nSize = pVec->nSize;
p->nCap = pVec->nCap;
p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
memcpy( p->pArray, pVec->pArray, sizeof(void *) * pVec->nSize );
return p;
}
/**Function*************************************************************
Synopsis [Transfers the array into another vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrDupArray( Vec_Ptr_t * pVec )
{
Vec_Ptr_t * p;
p = ALLOC( Vec_Ptr_t, 1 );
p->nSize = pVec->nSize;
p->nCap = pVec->nCap;
p->pArray = pVec->pArray;
pVec->nSize = 0;
pVec->nCap = 0;
pVec->pArray = NULL;
return p;
}
/**Function*************************************************************
Synopsis [Frees the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrFree( Vec_Ptr_t * p )
{
FREE( p->pArray );
FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void ** Vec_PtrReleaseArray( Vec_Ptr_t * p )
{
void ** pArray = p->pArray;
p->nCap = 0;
p->nSize = 0;
p->pArray = NULL;
return pArray;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void ** Vec_PtrArray( Vec_Ptr_t * p )
{
return p->pArray;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_PtrSize( Vec_Ptr_t * p )
{
return p->nSize;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
{
assert( i >= 0 && i < p->nSize );
return p->pArray[i];
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void ** Vec_PtrEntryP( Vec_Ptr_t * p, int i )
{
assert( i >= 0 && i < p->nSize );
return p->pArray + i;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrWriteEntry( Vec_Ptr_t * p, int i, void * Entry )
{
assert( i >= 0 && i < p->nSize );
p->pArray[i] = Entry;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void * Vec_PtrEntryLast( Vec_Ptr_t * p )
{
assert( p->nSize > 0 );
return p->pArray[p->nSize-1];
}
/**Function*************************************************************
Synopsis [Resizes the vector to the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrGrow( Vec_Ptr_t * p, int nCapMin )
{
if ( p->nCap >= nCapMin )
return;
p->pArray = REALLOC( void *, p->pArray, nCapMin );
p->nCap = nCapMin;
}
/**Function*************************************************************
Synopsis [Fills the vector with given number of entries.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrFill( Vec_Ptr_t * p, int nSize, void * Entry )
{
int i;
Vec_PtrGrow( p, nSize );
for ( i = 0; i < nSize; i++ )
p->pArray[i] = Entry;
p->nSize = nSize;
}
/**Function*************************************************************
Synopsis [Fills the vector with given number of entries.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
{
int i;
if ( p->nSize >= nSize )
return;
assert( p->nSize < nSize );
if ( 2 * p->nSize > nSize )
Vec_PtrGrow( p, 2 * nSize );
else
Vec_PtrGrow( p, nSize );
for ( i = p->nSize; i < nSize; i++ )
p->pArray[i] = Entry;
p->nSize = nSize;
}
/**Function*************************************************************
Synopsis [Returns the entry even if the place not exist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void * Vec_PtrGetEntry( Vec_Ptr_t * p, int i )
{
Vec_PtrFillExtra( p, i + 1, NULL );
return Vec_PtrEntry( p, i );
}
/**Function*************************************************************
Synopsis [Inserts the entry even if the place does not exist.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrSetEntry( Vec_Ptr_t * p, int i, void * Entry )
{
Vec_PtrFillExtra( p, i + 1, NULL );
Vec_PtrWriteEntry( p, i, Entry );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrShrink( Vec_Ptr_t * p, int nSizeNew )
{
assert( p->nSize >= nSizeNew );
p->nSize = nSizeNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrClear( Vec_Ptr_t * p )
{
p->nSize = 0;
}
/**Function*************************************************************
Synopsis [Copies the interger array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrCopy( Vec_Ptr_t * pDest, Vec_Ptr_t * pSour )
{
pDest->nSize = 0;
Vec_PtrGrow( pDest, pSour->nSize );
memcpy( pDest->pArray, pSour->pArray, sizeof(void *) * pSour->nSize );
pDest->nSize = pSour->nSize;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrPush( Vec_Ptr_t * p, void * Entry )
{
if ( p->nSize == p->nCap )
{
if ( p->nCap < 16 )
Vec_PtrGrow( p, 16 );
else
Vec_PtrGrow( p, 2 * p->nCap );
}
p->pArray[p->nSize++] = Entry;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_PtrPushUnique( Vec_Ptr_t * p, void * Entry )
{
int i;
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
return 1;
Vec_PtrPush( p, Entry );
return 0;
}
/**Function*************************************************************
Synopsis [Returns the last entry and removes it from the list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void * Vec_PtrPop( Vec_Ptr_t * p )
{
assert( p->nSize > 0 );
return p->pArray[--p->nSize];
}
/**Function*************************************************************
Synopsis [Find entry.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_PtrFind( Vec_Ptr_t * p, void * Entry )
{
int i;
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
return i;
return -1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry )
{
int i;
// delete assuming that it is closer to the end
for ( i = p->nSize - 1; i >= 0; i-- )
if ( p->pArray[i] == Entry )
break;
assert( i >= 0 );
/*
// delete assuming that it is closer to the beginning
for ( i = 0; i < p->nSize; i++ )
if ( p->pArray[i] == Entry )
break;
assert( i < p->nSize );
*/
for ( i++; i < p->nSize; i++ )
p->pArray[i-1] = p->pArray[i];
p->nSize--;
}
/**Function*************************************************************
Synopsis [Moves the first nItems to the end.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrReorder( Vec_Ptr_t * p, int nItems )
{
assert( nItems < p->nSize );
Vec_PtrGrow( p, nItems + p->nSize );
memmove( (char **)p->pArray + p->nSize, p->pArray, nItems * sizeof(void*) );
memmove( p->pArray, (char **)p->pArray + nItems, p->nSize * sizeof(void*) );
}
/**Function*************************************************************
Synopsis [Sorting the entries by their integer value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
{
if ( p->nSize < 2 )
return;
qsort( (void *)p->pArray, p->nSize, sizeof(void *),
(int (*)(const void *, const void *)) Vec_PtrSortCompare );
}
/**Function*************************************************************
Synopsis [Sorting the entries by their integer value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
{
int i, k;
if ( p->nSize < 2 )
return;
qsort( (void *)p->pArray, p->nSize, sizeof(void *),
(int (*)(const void *, const void *)) Vec_PtrSortCompare );
for ( i = k = 1; i < p->nSize; i++ )
if ( p->pArray[i] != p->pArray[i-1] )
p->pArray[k++] = p->pArray[i];
p->nSize = k;
}
/**Function*************************************************************
Synopsis [Allocates the array of simulation info.]
Description [Allocates the array containing given number of entries,
each of which contains given number of unsigned words of simulation data.
The resulting array can be freed using regular procedure Vec_PtrFree().
It is the responsibility of the user to ensure this array is never grown.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
{
void ** pMemory;
unsigned * pInfo;
int i;
pMemory = (void **)ALLOC( char, (sizeof(void *) + sizeof(unsigned) * nWords) * nEntries );
pInfo = (unsigned *)(pMemory + nEntries);
for ( i = 0; i < nEntries; i++ )
pMemory[i] = pInfo + i * nWords;
return Vec_PtrAllocArray( pMemory, nEntries );
}
/**Function*************************************************************
Synopsis [Cleans simulation info of each entry beginning with iWord.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrCleanSimInfo( Vec_Ptr_t * vInfo, int iWord, int nWords )
{
int i;
for ( i = 0; i < vInfo->nSize; i++ )
memset( (char*)Vec_PtrEntry(vInfo,i) + 4*iWord, 0, 4*(nWords-iWord) );
}
/**Function*************************************************************
Synopsis [Resizes the array of simulation info.]
Description [Doubles the number of objects for which siminfo is allocated.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrDoubleSimInfo( Vec_Ptr_t * vInfo )
{
Vec_Ptr_t * vInfoNew;
int nWords;
assert( Vec_PtrSize(vInfo) > 1 );
// get the new array
nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
vInfoNew = Vec_PtrAllocSimInfo( 2*Vec_PtrSize(vInfo), nWords );
// copy the simulation info
memcpy( Vec_PtrEntry(vInfoNew,0), Vec_PtrEntry(vInfo,0), Vec_PtrSize(vInfo) * nWords * 4 );
// replace the array
free( vInfo->pArray );
vInfo->pArray = vInfoNew->pArray;
vInfo->nSize *= 2;
vInfo->nCap *= 2;
// free the old array
vInfoNew->pArray = NULL;
free( vInfoNew );
}
/**Function*************************************************************
Synopsis [Resizes the array of simulation info.]
Description [Doubles the number of simulation patterns stored for each object.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_PtrReallocSimInfo( Vec_Ptr_t * vInfo )
{
Vec_Ptr_t * vInfoNew;
int nWords, i;
assert( Vec_PtrSize(vInfo) > 1 );
// get the new array
nWords = (unsigned *)Vec_PtrEntry(vInfo,1) - (unsigned *)Vec_PtrEntry(vInfo,0);
vInfoNew = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), 2*nWords );
// copy the simulation info
for ( i = 0; i < vInfo->nSize; i++ )
memcpy( Vec_PtrEntry(vInfoNew,i), Vec_PtrEntry(vInfo,i), nWords * 4 );
// replace the array
free( vInfo->pArray );
vInfo->pArray = vInfoNew->pArray;
// free the old array
vInfoNew->pArray = NULL;
free( vInfoNew );
}
/**Function*************************************************************
Synopsis [Allocates the array of truth tables for the given number of vars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Ptr_t * Vec_PtrAllocTruthTables( int nVars )
{
Vec_Ptr_t * p;
unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
unsigned * pTruth;
int i, k, nWords;
nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
p = Vec_PtrAllocSimInfo( nVars, nWords );
for ( i = 0; i < nVars; i++ )
{
pTruth = (unsigned *)p->pArray[i];
if ( i < 5 )
{
for ( k = 0; k < nWords; k++ )
pTruth[k] = Masks[i];
}
else
{
for ( k = 0; k < nWords; k++ )
if ( k & (1 << (i-5)) )
pTruth[k] = ~(unsigned)0;
else
pTruth[k] = 0;
}
}
return p;
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -1,583 +0,0 @@
/**CFile****************************************************************
FileName [vecStr.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resizable arrays.]
Synopsis [Resizable arrays of characters.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: vecStr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __VEC_STR_H__
#define __VEC_STR_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Vec_Str_t_ Vec_Str_t;
struct Vec_Str_t_
{
int nCap;
int nSize;
char * pArray;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define Vec_StrForEachEntry( vVec, Entry, i ) \
for ( i = 0; (i < Vec_StrSize(vVec)) && (((Entry) = Vec_StrEntry(vVec, i)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates a vector with the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Str_t * Vec_StrAlloc( int nCap )
{
Vec_Str_t * p;
p = ALLOC( Vec_Str_t, 1 );
if ( nCap > 0 && nCap < 16 )
nCap = 16;
p->nSize = 0;
p->nCap = nCap;
p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
return p;
}
/**Function*************************************************************
Synopsis [Allocates a vector with the given size and cleans it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Str_t * Vec_StrStart( int nSize )
{
Vec_Str_t * p;
p = Vec_StrAlloc( nSize );
p->nSize = nSize;
memset( p->pArray, 0, sizeof(char) * nSize );
return p;
}
/**Function*************************************************************
Synopsis [Creates the vector from an integer array of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Str_t * Vec_StrAllocArray( char * pArray, int nSize )
{
Vec_Str_t * p;
p = ALLOC( Vec_Str_t, 1 );
p->nSize = nSize;
p->nCap = nSize;
p->pArray = pArray;
return p;
}
/**Function*************************************************************
Synopsis [Creates the vector from an integer array of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Str_t * Vec_StrAllocArrayCopy( char * pArray, int nSize )
{
Vec_Str_t * p;
p = ALLOC( Vec_Str_t, 1 );
p->nSize = nSize;
p->nCap = nSize;
p->pArray = ALLOC( char, nSize );
memcpy( p->pArray, pArray, sizeof(char) * nSize );
return p;
}
/**Function*************************************************************
Synopsis [Duplicates the integer array.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Str_t * Vec_StrDup( Vec_Str_t * pVec )
{
Vec_Str_t * p;
p = ALLOC( Vec_Str_t, 1 );
p->nSize = pVec->nSize;
p->nCap = pVec->nCap;
p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
memcpy( p->pArray, pVec->pArray, sizeof(char) * pVec->nSize );
return p;
}
/**Function*************************************************************
Synopsis [Transfers the array into another vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Str_t * Vec_StrDupArray( Vec_Str_t * pVec )
{
Vec_Str_t * p;
p = ALLOC( Vec_Str_t, 1 );
p->nSize = pVec->nSize;
p->nCap = pVec->nCap;
p->pArray = pVec->pArray;
pVec->nSize = 0;
pVec->nCap = 0;
pVec->pArray = NULL;
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrFree( Vec_Str_t * p )
{
FREE( p->pArray );
FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline char * Vec_StrReleaseArray( Vec_Str_t * p )
{
char * pArray = p->pArray;
p->nCap = 0;
p->nSize = 0;
p->pArray = NULL;
return pArray;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline char * Vec_StrArray( Vec_Str_t * p )
{
return p->pArray;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_StrSize( Vec_Str_t * p )
{
return p->nSize;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline char Vec_StrEntry( Vec_Str_t * p, int i )
{
assert( i >= 0 && i < p->nSize );
return p->pArray[i];
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrWriteEntry( Vec_Str_t * p, int i, char Entry )
{
assert( i >= 0 && i < p->nSize );
p->pArray[i] = Entry;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline char Vec_StrEntryLast( Vec_Str_t * p )
{
assert( p->nSize > 0 );
return p->pArray[p->nSize-1];
}
/**Function*************************************************************
Synopsis [Resizes the vector to the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin )
{
if ( p->nCap >= nCapMin )
return;
p->pArray = REALLOC( char, p->pArray, 2 * nCapMin );
p->nCap = 2 * nCapMin;
}
/**Function*************************************************************
Synopsis [Fills the vector with given number of entries.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrFill( Vec_Str_t * p, int nSize, char Entry )
{
int i;
Vec_StrGrow( p, nSize );
p->nSize = nSize;
for ( i = 0; i < p->nSize; i++ )
p->pArray[i] = Entry;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrShrink( Vec_Str_t * p, int nSizeNew )
{
assert( p->nSize >= nSizeNew );
p->nSize = nSizeNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrClear( Vec_Str_t * p )
{
p->nSize = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
{
if ( p->nSize == p->nCap )
{
if ( p->nCap < 16 )
Vec_StrGrow( p, 16 );
else
Vec_StrGrow( p, 2 * p->nCap );
}
p->pArray[p->nSize++] = Entry;
}
/**Function********************************************************************
Synopsis [Finds the smallest integer larger of equal than the logarithm.]
Description [Returns [Log10(Num)].]
SideEffects []
SeeAlso []
******************************************************************************/
static inline int Vec_StrBase10Log( unsigned Num )
{
int Res;
assert( Num >= 0 );
if ( Num == 0 ) return 0;
if ( Num == 1 ) return 1;
for ( Res = 0, Num--; Num; Num /= 10, Res++ );
return Res;
} /* end of Extra_Base2Log */
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrPrintNum( Vec_Str_t * p, int Num )
{
int i, nDigits;
if ( Num < 0 )
{
Vec_StrPush( p, '-' );
Num = -Num;
}
if ( Num < 10 )
{
Vec_StrPush( p, (char)('0' + Num) );
return;
}
nDigits = Vec_StrBase10Log( Num );
Vec_StrGrow( p, p->nSize + nDigits );
for ( i = nDigits - 1; i >= 0; i-- )
{
Vec_StrWriteEntry( p, p->nSize + i, (char)('0' + Num % 10) );
Num /= 10;
}
assert( Num == 0 );
p->nSize += nDigits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrPrintStr( Vec_Str_t * p, char * pStr )
{
int i, Length = strlen(pStr);
for ( i = 0; i < Length; i++ )
Vec_StrPush( p, pStr[i] );
}
/**Function*************************************************************
Synopsis [Appends the string to the char vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrAppend( Vec_Str_t * p, char * pString )
{
int i, nLength = strlen(pString);
Vec_StrGrow( p, p->nSize + nLength );
for ( i = 0; i < nLength; i++ )
p->pArray[p->nSize + i] = pString[i];
p->nSize += nLength;
}
/**Function*************************************************************
Synopsis [Returns the last entry and removes it from the list.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline char Vec_StrPop( Vec_Str_t * p )
{
assert( p->nSize > 0 );
return p->pArray[--p->nSize];
}
/**Function*************************************************************
Synopsis [Comparison procedure for two clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_StrSortCompare1( char * pp1, char * pp2 )
{
// for some reason commenting out lines (as shown) led to crashing of the release version
if ( *pp1 < *pp2 )
return -1;
if ( *pp1 > *pp2 ) //
return 1;
return 0; //
}
/**Function*************************************************************
Synopsis [Comparison procedure for two clauses.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_StrSortCompare2( char * pp1, char * pp2 )
{
// for some reason commenting out lines (as shown) led to crashing of the release version
if ( *pp1 > *pp2 )
return -1;
if ( *pp1 < *pp2 ) //
return 1;
return 0; //
}
/**Function*************************************************************
Synopsis [Sorting the entries by their integer value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
{
if ( fReverse )
qsort( (void *)p->pArray, p->nSize, sizeof(char),
(int (*)(const void *, const void *)) Vec_StrSortCompare2 );
else
qsort( (void *)p->pArray, p->nSize, sizeof(char),
(int (*)(const void *, const void *)) Vec_StrSortCompare1 );
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -1,356 +0,0 @@
/**CFile****************************************************************
FileName [vecVec.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resizable arrays.]
Synopsis [Resizable vector of resizable vectors.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: vecVec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __VEC_VEC_H__
#define __VEC_VEC_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Vec_Vec_t_ Vec_Vec_t;
struct Vec_Vec_t_
{
int nCap;
int nSize;
void ** pArray;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// iterators through levels
#define Vec_VecForEachLevel( vGlob, vVec, i ) \
for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart ) \
for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \
for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
#define Vec_VecForEachLevelReverse( vGlob, vVec, i ) \
for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
#define Vec_VecForEachLevelReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \
for ( i = LevelStart; (i >= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
// iteratores through entries
#define Vec_VecForEachEntry( vGlob, pEntry, i, k ) \
for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \
Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k )
#define Vec_VecForEachEntryLevel( vGlob, pEntry, i, Level ) \
Vec_PtrForEachEntry( Vec_VecEntry(vGlob, Level), pEntry, i )
#define Vec_VecForEachEntryStart( vGlob, pEntry, i, k, LevelStart ) \
for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ ) \
Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k )
#define Vec_VecForEachEntryStartStop( vGlob, pEntry, i, k, LevelStart, LevelStop ) \
for ( i = LevelStart; i <= LevelStop; i++ ) \
Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k )
#define Vec_VecForEachEntryReverse( vGlob, pEntry, i, k ) \
for ( i = 0; i < Vec_VecSize(vGlob); i++ ) \
Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k )
#define Vec_VecForEachEntryReverseReverse( vGlob, pEntry, i, k ) \
for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- ) \
Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k )
#define Vec_VecForEachEntryReverseStart( vGlob, pEntry, i, k, LevelStart ) \
for ( i = LevelStart; i >= 0; i-- ) \
Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates a vector with the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Vec_t * Vec_VecAlloc( int nCap )
{
Vec_Vec_t * p;
p = ALLOC( Vec_Vec_t, 1 );
if ( nCap > 0 && nCap < 8 )
nCap = 8;
p->nSize = 0;
p->nCap = nCap;
p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
return p;
}
/**Function*************************************************************
Synopsis [Allocates a vector with the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Vec_Vec_t * Vec_VecStart( int nSize )
{
Vec_Vec_t * p;
int i;
p = Vec_VecAlloc( nSize );
for ( i = 0; i < nSize; i++ )
p->pArray[i] = Vec_PtrAlloc( 0 );
p->nSize = nSize;
return p;
}
/**Function*************************************************************
Synopsis [Allocates a vector with the given capacity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecExpand( Vec_Vec_t * p, int Level )
{
int i;
if ( p->nSize >= Level + 1 )
return;
Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
for ( i = p->nSize; i <= Level; i++ )
p->pArray[i] = Vec_PtrAlloc( 0 );
p->nSize = Level + 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_VecSize( Vec_Vec_t * p )
{
return p->nSize;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void * Vec_VecEntry( Vec_Vec_t * p, int i )
{
assert( i >= 0 && i < p->nSize );
return p->pArray[i];
}
/**Function*************************************************************
Synopsis [Frees the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecFree( Vec_Vec_t * p )
{
Vec_Ptr_t * vVec;
int i;
Vec_VecForEachLevel( p, vVec, i )
Vec_PtrFree( vVec );
Vec_PtrFree( (Vec_Ptr_t *)p );
}
/**Function*************************************************************
Synopsis [Frees the vector of vectors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_VecSizeSize( Vec_Vec_t * p )
{
Vec_Ptr_t * vVec;
int i, Counter = 0;
Vec_VecForEachLevel( p, vVec, i )
Counter += vVec->nSize;
return Counter;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecClear( Vec_Vec_t * p )
{
Vec_Ptr_t * vVec;
int i;
Vec_VecForEachLevel( p, vVec, i )
Vec_PtrClear( vVec );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
{
if ( p->nSize < Level + 1 )
{
int i;
Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
for ( i = p->nSize; i < Level + 1; i++ )
p->pArray[i] = Vec_PtrAlloc( 0 );
p->nSize = Level + 1;
}
Vec_PtrPush( (Vec_Ptr_t*)p->pArray[Level], Entry );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
{
if ( p->nSize < Level + 1 )
Vec_VecPush( p, Level, Entry );
else
Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
}
/**Function*************************************************************
Synopsis [Comparison procedure for two arrays.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_VecSortCompare1( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 )
{
if ( Vec_PtrSize(*pp1) < Vec_PtrSize(*pp2) )
return -1;
if ( Vec_PtrSize(*pp1) > Vec_PtrSize(*pp2) )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Comparison procedure for two integers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_VecSortCompare2( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 )
{
if ( Vec_PtrSize(*pp1) > Vec_PtrSize(*pp2) )
return -1;
if ( Vec_PtrSize(*pp1) < Vec_PtrSize(*pp2) )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Sorting the entries by their integer value.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_VecSort( Vec_Vec_t * p, int fReverse )
{
if ( fReverse )
qsort( (void *)p->pArray, p->nSize, sizeof(void *),
(int (*)(const void *, const void *)) Vec_VecSortCompare2 );
else
qsort( (void *)p->pArray, p->nSize, sizeof(void *),
(int (*)(const void *, const void *)) Vec_VecSortCompare1 );
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -35,7 +35,7 @@ extern "C" {
#include <assert.h>
#include <time.h>
#include "vec2.h"
#include "vec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///

View File

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

View File

@ -1,8 +1,10 @@
SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigCuts.c \
src/aig/aig/aigDfs.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 \
@ -15,6 +17,7 @@ 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 \

177
src/aig/bar/bar.c Normal file
View File

@ -0,0 +1,177 @@
/**CFile****************************************************************
FileName [bar.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [extra]
Synopsis [Progress bar.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bar.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
struct Bar_Progress_t_
{
int nItemsNext; // the number of items for the next update of the progress bar
int nItemsTotal; // the total number of items
int posTotal; // the total number of positions
int posCur; // the current position
FILE * pFile; // the output stream
};
static void Bar_ProgressShow( Bar_Progress_t * p, char * pString );
static void Bar_ProgressClean( Bar_Progress_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the progress bar.]
Description [The first parameter is the output stream (pFile), where
the progress is printed. The current printing position should be the
first one on the given line. The second parameters is the total
number of items that correspond to 100% position of the progress bar.]
SideEffects []
SeeAlso []
***********************************************************************/
Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal )
{
Bar_Progress_t * p;
// extern int Abc_FrameShowProgress( void * p );
// extern void * Abc_FrameGetGlobalFrame();
// if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
p = (Bar_Progress_t *) malloc(sizeof(Bar_Progress_t));
memset( p, 0, sizeof(Bar_Progress_t) );
p->pFile = pFile;
p->nItemsTotal = nItemsTotal;
p->posTotal = 78;
p->posCur = 1;
p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal);
Bar_ProgressShow( p, NULL );
return p;
}
/**Function*************************************************************
Synopsis [Updates the progress bar.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bar_ProgressUpdate_int( Bar_Progress_t * p, int nItemsCur, char * pString )
{
if ( p == NULL ) return;
if ( nItemsCur < p->nItemsNext )
return;
if ( nItemsCur >= p->nItemsTotal )
{
p->posCur = 78;
p->nItemsNext = 0x7FFFFFFF;
}
else
{
p->posCur += 7;
p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal);
}
Bar_ProgressShow( p, pString );
}
/**Function*************************************************************
Synopsis [Stops the progress bar.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bar_ProgressStop( Bar_Progress_t * p )
{
if ( p == NULL ) return;
Bar_ProgressClean( p );
free( p );
}
/**Function*************************************************************
Synopsis [Prints the progress bar of the given size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bar_ProgressShow( Bar_Progress_t * p, char * pString )
{
int i;
if ( p == NULL ) return;
if ( pString )
fprintf( p->pFile, "%s ", pString );
for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ )
fprintf( p->pFile, "-" );
if ( i == p->posCur )
fprintf( p->pFile, ">" );
for ( i++ ; i <= p->posTotal; i++ )
fprintf( p->pFile, " " );
fprintf( p->pFile, "\r" );
fflush( stdout );
}
/**Function*************************************************************
Synopsis [Cleans the progress bar before quitting.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bar_ProgressClean( Bar_Progress_t * p )
{
int i;
if ( p == NULL ) return;
for ( i = 0; i <= p->posTotal; i++ )
fprintf( p->pFile, " " );
fprintf( p->pFile, "\r" );
fflush( stdout );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

74
src/aig/bar/bar.h Normal file
View File

@ -0,0 +1,74 @@
/**CFile****************************************************************
FileName [bar.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Progress bar.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bar.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __BAR_H__
#define __BAR_H__
#ifdef __cplusplus
extern "C" {
#endif
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define BAR_PROGRESS_USE 1
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Bar_Progress_t_ Bar_Progress_t;
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== bar.c ==========================================================*/
extern Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal );
extern void Bar_ProgressStop( Bar_Progress_t * p );
extern void Bar_ProgressUpdate_int( Bar_Progress_t * p, int nItemsCur, char * pString );
static inline void Bar_ProgressUpdate( Bar_Progress_t * p, int nItemsCur, char * pString ) {
if ( BAR_PROGRESS_USE && p && (nItemsCur < *((int*)p)) ) return; Bar_ProgressUpdate_int(p, nItemsCur, pString); }
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/aig/bar/module.make Normal file
View File

@ -0,0 +1 @@
SRC += src/aig/bar/bar.c

73
src/aig/bdc/bdc.h Normal file
View File

@ -0,0 +1,73 @@
/**CFile****************************************************************
FileName [bdc.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdc.h,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __BDC_H__
#define __BDC_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Bdc_Man_t_ Bdc_Man_t;
typedef struct Bdc_Par_t_ Bdc_Par_t;
struct Bdc_Par_t_
{
// general parameters
int nVarsMax; // the maximum support
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== bdcCore.c ==========================================================*/
extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
extern void Bdc_ManFree( Bdc_Man_t * p );
extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesLimit );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

189
src/aig/bdc/bdcCore.c Normal file
View File

@ -0,0 +1,189 @@
/**CFile****************************************************************
FileName [bdcCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [The gateway to bi-decomposition.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdcCore.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocate resynthesis manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
{
Bdc_Man_t * p;
unsigned * pData;
int i, k, nBits;
p = ALLOC( Bdc_Man_t, 1 );
memset( p, 0, sizeof(Bdc_Man_t) );
assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
p->pPars = pPars;
p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
p->nDivsLimit = 200;
p->nNodesLimit = 0; // will be set later
// memory
p->vMemory = Vec_IntStart( 1 << 16 );
// internal nodes
p->nNodesAlloc = 512;
p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
// set up hash table
p->nTableSize = (1 << p->pPars->nVarsMax);
p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
p->vSpots = Vec_IntAlloc( 256 );
// truth tables
p->vTruths = Vec_PtrAllocSimInfo( pPars->nVarsMax + 5, p->nWords );
// set elementary truth tables
nBits = (1 << pPars->nVarsMax);
Kit_TruthFill( Vec_PtrEntry(p->vTruths, 0), p->nVars );
for ( k = 0; k < pPars->nVarsMax; k++ )
{
pData = Vec_PtrEntry( p->vTruths, k+1 );
Kit_TruthClear( pData, p->nVars );
for ( i = 0; i < nBits; i++ )
if ( i & (1 << k) )
pData[i>>5] |= (1 << (i&31));
}
p->puTemp1 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 1 );
p->puTemp2 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 2 );
p->puTemp3 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 3 );
p->puTemp4 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 4 );
// start the internal ISFs
p->pIsfOL = &p->IsfOL; Bdc_IsfStart( p, p->pIsfOL );
p->pIsfOR = &p->IsfOR; Bdc_IsfStart( p, p->pIsfOR );
p->pIsfAL = &p->IsfAL; Bdc_IsfStart( p, p->pIsfAL );
p->pIsfAR = &p->IsfAR; Bdc_IsfStart( p, p->pIsfAR );
return p;
}
/**Function*************************************************************
Synopsis [Deallocate resynthesis manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_ManFree( Bdc_Man_t * p )
{
Vec_IntFree( p->vMemory );
Vec_IntFree( p->vSpots );
Vec_PtrFree( p->vTruths );
free( p->pNodes );
free( p->pTable );
free( p );
}
/**Function*************************************************************
Synopsis [Clears the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
{
unsigned * puTruth;
Bdc_Fun_t * pNode;
int i;
Bdc_TableClear( p );
Vec_IntClear( p->vMemory );
// add constant 1 and elementary vars
p->nNodes = p->nNodesNew = 0;
for ( i = 0; i <= p->pPars->nVarsMax; i++ )
{
pNode = Bdc_FunNew( p );
pNode->Type = BDC_TYPE_PI;
pNode->puFunc = Vec_PtrEntry( p->vTruths, i );
pNode->uSupp = i? (1 << (i-1)) : 0;
Bdc_TableAdd( p, pNode );
}
// add the divisors
Vec_PtrForEachEntry( vDivs, puTruth, i )
{
pNode = Bdc_FunNew( p );
pNode->Type = BDC_TYPE_PI;
pNode->puFunc = puTruth;
pNode->uSupp = Kit_TruthSupport( puTruth, p->nVars );
Bdc_TableAdd( p, pNode );
if ( i == p->nDivsLimit )
break;
}
}
/**Function*************************************************************
Synopsis [Performs decomposition of one function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
{
Bdc_Isf_t Isf, * pIsf = &Isf;
// set current manager parameters
p->nVars = nVars;
p->nWords = Kit_TruthWordNum( nVars );
Bdc_ManPrepare( p, vDivs );
p->nNodesLimit = (p->nNodes + nNodesMax < p->nNodesAlloc)? p->nNodes + nNodesMax : p->nNodesAlloc;
// copy the function
Bdc_IsfStart( p, pIsf );
Bdc_IsfClean( pIsf );
pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars );
Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
// call decomposition
Bdc_SuppMinimize( p, pIsf );
p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
if ( p->pRoot == NULL )
return -1;
return p->nNodesNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

461
src/aig/bdc/bdcDec.c Normal file
View File

@ -0,0 +1,461 @@
/**CFile****************************************************************
FileName [bdcDec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [Decomposition procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdcDec.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR );
static int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs one step of bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
Bdc_Fun_t * pFunc;
Bdc_Isf_t IsfL, * pIsfL = &IsfL;
Bdc_Isf_t IsfB, * pIsfR = &IsfB;
// check computed results
if ( pFunc = Bdc_TableLookup( p, pIsf ) )
return pFunc;
// decide on the decomposition type
pFunc = Bdc_FunNew( p );
if ( pFunc == NULL )
return NULL;
pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
// decompose the left branch
pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfL );
if ( pFunc->pFan0 == NULL )
return NULL;
// decompose the right branch
if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc->pFan0->puFunc, pFunc->Type ) )
{
p->nNodes--;
return pFunc->pFan0;
}
pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfL );
if ( pFunc->pFan1 == NULL )
return NULL;
// compute the function of node
pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords);
if ( pFunc->Type == BDC_TYPE_AND )
Kit_TruthAnd( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
else if ( pFunc->Type == BDC_TYPE_OR )
Kit_TruthOr( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
else
assert( 0 );
// verify correctness
assert( Bdc_TableCheckContainment(p, pIsf, pFunc->puFunc) );
// convert from OR to AND
if ( pFunc->Type == BDC_TYPE_OR )
{
pFunc->Type = BDC_TYPE_AND;
pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
pFunc = Bdc_Not(pFunc);
}
Bdc_TableAdd( p, Bdc_Regular(pFunc) );
return pFunc;
}
/**Function*************************************************************
Synopsis [Updates the ISF of the right after the left was decompoosed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type )
{
if ( Type == BDC_TYPE_OR )
{
// Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes );
// Right.R = bdd_exist( R, setRightRes );
// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Cudd_Not(CompSpecF), pL->V ); Cudd_Ref( pR->Q );
// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
// assert( pR->R != b0 );
// return (int)( pR->Q == b0 );
Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp );
Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp );
assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
}
else if ( Type == BDC_TYPE_AND )
{
// Right.R = bdd_appex( R, CompSpecLeftF, bddop_and, setRightRes );
// Right.Q = bdd_exist( Q, setRightRes );
// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
// pR->R = Cudd_bddAndAbstract( dd, pF->R, CompSpecF, pL->V ); Cudd_Ref( pR->R );
// pR->Q = Cudd_bddExistAbstract( dd, pF->Q, pL->V ); Cudd_Ref( pR->Q );
// assert( pR->Q != b0 );
// return (int)( pR->R == b0 );
Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp );
Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp );
assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
}
return 0;
}
/**Function*************************************************************
Synopsis [Checks existence of OR-bidecomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Bdc_DecomposeGetCost( Bdc_Man_t * p, int nLeftVars, int nRightVars )
{
assert( nLeftVars > 0 );
assert( nRightVars > 0 );
// compute the decomposition coefficient
if ( nLeftVars >= nRightVars )
return BDC_SCALE * (p->nVars * nRightVars + nLeftVars);
else // if ( nLeftVars < nRightVars )
return BDC_SCALE * (p->nVars * nLeftVars + nRightVars);
}
/**Function*************************************************************
Synopsis [Checks existence of weak OR-bidecomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
char pVars[16];
int v, nVars, Beg, End;
assert( pIsfL->uSupp == 0 );
assert( pIsfR->uSupp == 0 );
// fill in the variables
nVars = 0;
for ( v = 0; v < p->nVars; v++ )
if ( pIsf->uSupp & (1 << v) )
pVars[nVars++] = v;
// try variable pairs
for ( Beg = 0; Beg < nVars; Beg++ )
{
Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pVars[Beg] );
for ( End = nVars - 1; End > Beg; End-- )
{
Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] );
if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) )
{
pIsfL->uSupp = (1 << Beg);
pIsfR->uSupp = (1 << End);
pIsfL->Var = Beg;
pIsfR->Var = End;
return 1;
}
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Checks existence of weak OR-bidecomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
int v, VarCost, VarBest, Cost, VarCostBest = 0;
for ( v = 0; v < p->nVars; v++ )
{
Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
// if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse )
// Exist = Cudd_bddExistAbstract( dd, pF->R, Var ); Cudd_Ref( Exist );
// if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 )
if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) )
{
// measure the cost of this variable
// VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube );
// Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var ); Cudd_Ref( Univ );
// VarCost = Kit_TruthCountOnes( Univ, p->nVars );
// Cudd_RecursiveDeref( dd, Univ );
Kit_TruthForallNew( p->puTemp2, pIsf->puOn, p->nVars, v );
VarCost = Kit_TruthCountOnes( p->puTemp2, p->nVars );
if ( VarCost == 0 )
VarCost = 1;
if ( VarCostBest < VarCost )
{
VarCostBest = VarCost;
VarBest = v;
}
}
}
// derive the components for weak-bi-decomposition if the variable is found
if ( VarCostBest )
{
// funQLeftRes = Q & bdd_exist( R, setRightORweak );
// Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest ); Cudd_Ref( Temp );
// pL->Q = Cudd_bddAnd( dd, pF->Q, Temp ); Cudd_Ref( pL->Q );
// Cudd_RecursiveDeref( dd, Temp );
Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, VarBest );
Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
// pL->R = pF->R; Cudd_Ref( pL->R );
// pL->V = VarBest; Cudd_Ref( pL->V );
Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars );
pIsfL->Var = VarBest;
// assert( pL->Q != b0 );
// assert( pL->R != b0 );
// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
// express cost in percents of the covered boolean space
Cost = VarCostBest * BDC_SCALE / (1<<p->nVars);
if ( Cost == 0 )
Cost = 1;
return Cost;
}
return 0;
}
/**Function*************************************************************
Synopsis [Checks existence of OR-bidecomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
unsigned uSuppRem;
int v, nLeftVars = 1, nRightVars = 1;
// clean the var sets
Bdc_IsfClean( pIsfL );
Bdc_IsfClean( pIsfR );
// find initial variable sets
if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) )
return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR );
// prequantify the variables in the offset
Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->Var );
Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->Var );
// go through the remaining variables
uSuppRem = pIsf->uSupp & ~pIsfL->uSupp & ~pIsfR->uSupp;
assert( Kit_WordCountOnes(uSuppRem) > 0 );
for ( v = 0; v < p->nVars; v++ )
{
if ( (uSuppRem & (1 << v)) == 0 )
continue;
// prequantify this variable
Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v );
Kit_TruthExistNew( p->puTemp4, p->puTemp2, p->nVars, v );
if ( nLeftVars < nRightVars )
{
// if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
// if ( VerifyORCondition( dd, pF->Q, pF->R, pL->V, pR->V, VarNew ) )
if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
{
// pL->V &= VarNew;
pIsfL->uSupp |= (1 << v);
nLeftVars++;
}
// else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
{
// pR->V &= VarNew;
pIsfR->uSupp |= (1 << v);
nRightVars++;
}
}
else
{
// if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
{
// pR->V &= VarNew;
pIsfR->uSupp |= (1 << v);
nRightVars++;
}
// else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
{
// pL->V &= VarNew;
pIsfL->uSupp |= (1 << v);
nLeftVars++;
}
}
}
// derive the functions Q and R for the left branch
// pL->Q = bdd_appex( pF->Q, bdd_exist( pF->R, pL->V ), bddop_and, pR->V );
// pL->R = bdd_exist( pF->R, pR->V );
// Temp = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( Temp );
// pL->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pR->V ); Cudd_Ref( pL->Q );
// Cudd_RecursiveDeref( dd, Temp );
// pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( pL->R );
Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uSupp );
Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars );
// derive the functions Q and R for the right branch
// Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( Temp );
// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q );
// Cudd_RecursiveDeref( dd, Temp );
// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
/*
Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars );
Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp );
Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars );
*/
// assert( pL->Q != b0 );
// assert( pL->R != b0 );
// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars );
}
/**Function*************************************************************
Synopsis [Performs one step of bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
int CostOr, CostAnd, CostOrL, CostOrR, CostAndL, CostAndR;
Bdc_IsfClean( p->pIsfOL );
Bdc_IsfClean( p->pIsfOR );
Bdc_IsfClean( p->pIsfAL );
Bdc_IsfClean( p->pIsfAR );
// perform OR decomposition
CostOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
// perform AND decomposition
Bdc_IsfNot( pIsf );
CostAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
Bdc_IsfNot( pIsf );
Bdc_IsfNot( p->pIsfAL );
Bdc_IsfNot( p->pIsfAR );
// check the hash table
Bdc_SuppMinimize( p, p->pIsfOL );
CostOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
Bdc_SuppMinimize( p, p->pIsfOR );
CostOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
Bdc_SuppMinimize( p, p->pIsfAL );
CostAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
Bdc_SuppMinimize( p, p->pIsfAR );
CostAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
// check if there is any reuse for the components
if ( CostOrL + CostOrR < CostAndL + CostAndR )
{
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
if ( CostOrL + CostOrR > CostAndL + CostAndR )
{
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
}
// compare the two-component costs
if ( CostOr < CostAnd )
{
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
return BDC_TYPE_AND;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

150
src/aig/bdc/bdcInt.h Normal file
View File

@ -0,0 +1,150 @@
/**CFile****************************************************************
FileName [bdcInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 15, 2007.]
Revision [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __BDC_INT_H__
#define __BDC_INT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "kit.h"
#include "bdc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define BDC_SCALE 100 // value used to compute the cost
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// network types
typedef enum {
BDC_TYPE_NONE = 0, // 0: unknown
BDC_TYPE_CONST1, // 1: constant 1
BDC_TYPE_PI, // 2: primary input
BDC_TYPE_AND, // 4: AND-gate
BDC_TYPE_OR, // 5: OR-gate (temporary)
BDC_TYPE_XOR, // 6: XOR-gate
BDC_TYPE_MUX, // 7: MUX-gate
BDC_TYPE_OTHER // 8: unused
} Bdc_Type_t;
typedef struct Bdc_Fun_t_ Bdc_Fun_t;
struct Bdc_Fun_t_
{
int Type; // Const1, PI, AND, XOR, MUX
Bdc_Fun_t * pFan0; // fanin of the given node
Bdc_Fun_t * pFan1; // fanin of the given node
Bdc_Fun_t * pFan2; // fanin of the given node
unsigned uSupp; // bit mask of current support
unsigned * puFunc; // the function of the node
Bdc_Fun_t * pNext; // next function with same support
void * pCopy; // the copy field
};
typedef struct Bdc_Isf_t_ Bdc_Isf_t;
struct Bdc_Isf_t_
{
int Var; // the first variable assigned
unsigned uSupp; // the current support
unsigned * puOn; // on-set
unsigned * puOff; // off-set
};
struct Bdc_Man_t_
{
// external parameters
Bdc_Par_t * pPars; // parameter set
int nVars; // the number of variables
int nWords; // the number of words
int nNodesLimit; // the limit on the number of new nodes
int nDivsLimit; // the limit on the number of divisors
// internal nodes
Bdc_Fun_t * pNodes; // storage for decomposition nodes
int nNodes; // the number of nodes used
int nNodesNew; // the number of nodes used
int nNodesAlloc; // the number of nodes allocated
Bdc_Fun_t * pRoot; // the root node
// resub candidates
Bdc_Fun_t ** pTable; // hash table of candidates
int nTableSize; // hash table size (1 << nVarsMax)
Vec_Int_t * vSpots; // the occupied spots in the table
// elementary truth tables
Vec_Ptr_t * vTruths; // for const 1 and elementary variables
unsigned * puTemp1; // temporary truth table
unsigned * puTemp2; // temporary truth table
unsigned * puTemp3; // temporary truth table
unsigned * puTemp4; // temporary truth table
// temporary ISFs
Bdc_Isf_t * pIsfOL, IsfOL;
Bdc_Isf_t * pIsfOR, IsfOR;
Bdc_Isf_t * pIsfAL, IsfAL;
Bdc_Isf_t * pIsfAR, IsfAR;
// internal memory manager
Vec_Int_t * vMemory; // memory for internal truth tables
};
// working with complemented attributes of objects
static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((unsigned long)p & (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; }
static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); }
static inline void Bdc_IsfClean( Bdc_Isf_t * p ) { p->uSupp = 0; p->Var = 0; }
static inline void Bdc_IsfCopy( Bdc_Isf_t * p, Bdc_Isf_t * q ) { Bdc_Isf_t T = *p; *p = *q; *q = T; }
static inline void Bdc_IsfNot( Bdc_Isf_t * p ) { unsigned * puT = p->puOn; p->puOn = p->puOff; p->puOff = puT; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== bdcDec.c ==========================================================*/
extern Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
/*=== bdcTable.c ==========================================================*/
extern Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc );
extern void Bdc_TableClear( Bdc_Man_t * p );
extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

140
src/aig/bdc/bdcTable.c Normal file
View File

@ -0,0 +1,140 @@
/**CFile****************************************************************
FileName [bdcTable.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [Hash table for intermediate nodes.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdcTable.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Minimizes the support of the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
int v;
// go through the support variables
for ( v = 0; v < p->nVars; v++ )
{
if ( (pIsf->uSupp & (1 << v)) == 0 )
continue;
Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
continue;
// remove the variable
Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
pIsf->uSupp &= ~(1 << v);
}
}
/**Function*************************************************************
Synopsis [Checks containment of the function in the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth )
{
return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) &&
Kit_TruthIsDisjoint( pIsf->puOff, puTruth, p->nVars );
}
/**Function*************************************************************
Synopsis [Adds the new entry to the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
Bdc_Fun_t * pFunc;
for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
return pFunc;
return NULL;
}
/**Function*************************************************************
Synopsis [Adds the new entry to the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc )
{
if ( p->pTable[pFunc->uSupp] == NULL )
Vec_IntPush( p->vSpots, pFunc->uSupp );
pFunc->pNext = p->pTable[pFunc->uSupp];
p->pTable[pFunc->uSupp] = pFunc;
}
/**Function*************************************************************
Synopsis [Adds the new entry to the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_TableClear( Bdc_Man_t * p )
{
int Spot, i;
Vec_IntForEachEntry( p->vSpots, Spot, i )
p->pTable[Spot] = NULL;
Vec_IntClear( p->vSpots );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

49
src/aig/bdc/bdc_.c Normal file
View File

@ -0,0 +1,49 @@
/**CFile****************************************************************
FileName [bdc_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/bdc/module.make Normal file
View File

@ -0,0 +1,4 @@
SRC += src/aig/bdc/bdcCore.c \
src/aig/bdc/bdcDec.c \
src/aig/bdc/bdcTable.c

View File

@ -35,7 +35,7 @@ extern "C" {
#include <assert.h>
#include <time.h>
#include "vec2.h"
#include "vec.h"
#include "aig.h"
#include "darInt.h"

65
src/aig/csw/csw.h Normal file
View File

@ -0,0 +1,65 @@
/**CFile****************************************************************
FileName [csw.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cut sweeping.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 11, 2007.]
Revision [$Id: csw.h,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CSW_H__
#define __CSW_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cnfCore.c ========================================================*/
extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

94
src/aig/csw/cswCore.c Normal file
View File

@ -0,0 +1,94 @@
/**CFile****************************************************************
FileName [cswCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cut sweeping.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 11, 2007.]
Revision [$Id: cswCore.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose )
{
Csw_Man_t * p;
Aig_Man_t * pRes;
Aig_Obj_t * pObj, * pObjNew, * pObjRes;
int i, clk;
clk = clock();
// start the manager
p = Csw_ManStart( pAig, nCutsMax, nLeafMax, fVerbose );
// set elementary cuts at the PIs
Aig_ManForEachPi( p->pManRes, pObj, i )
{
Csw_ObjPrepareCuts( p, pObj, 1 );
Csw_ObjAddRefs( p, pObj, Aig_ManPi(p->pManAig,i)->nRefs );
}
// process the nodes
Aig_ManForEachNode( pAig, pObj, i )
{
// create the new node
pObjNew = Aig_And( p->pManRes, Csw_ObjChild0Equiv(p, pObj), Csw_ObjChild1Equiv(p, pObj) );
// check if this node can be represented using another node
// pObjRes = Csw_ObjSweep( p, Aig_Regular(pObjNew), pObj->nRefs > 1 );
// pObjRes = Aig_NotCond( pObjRes, Aig_IsComplement(pObjNew) );
// try recursively if resubsitution is used
do {
pObjRes = Csw_ObjSweep( p, Aig_Regular(pObjNew), pObj->nRefs > 1 );
pObjRes = Aig_NotCond( pObjRes, Aig_IsComplement(pObjNew) );
pObjNew = pObjRes;
} while ( Csw_ObjCuts(p, Aig_Regular(pObjNew)) == NULL && !Aig_ObjIsConst1(Aig_Regular(pObjNew)) );
// save the resulting node
Csw_ObjSetEquiv( p, pObj, pObjRes );
// add to the reference counter
Csw_ObjAddRefs( p, Aig_Regular(pObjRes), pObj->nRefs );
}
// add the POs
Aig_ManForEachPo( pAig, pObj, i )
Aig_ObjCreatePo( p->pManRes, Csw_ObjChild0Equiv(p, pObj) );
// remove dangling nodes
Aig_ManCleanup( p->pManRes );
// return the resulting manager
p->timeTotal = clock() - clk;
p->timeOther = p->timeTotal - p->timeCuts - p->timeHash;
pRes = p->pManRes;
Csw_ManStop( p );
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

602
src/aig/csw/cswCut.c Normal file
View File

@ -0,0 +1,602 @@
/**CFile****************************************************************
FileName [cswCut.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cut sweeping.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 11, 2007.]
Revision [$Id: cswCut.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Compute the cost of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Csw_CutFindCost( Csw_Man_t * p, Csw_Cut_t * pCut )
{
Aig_Obj_t * pLeaf;
int i, Cost = 0;
assert( pCut->nFanins > 0 );
Csw_CutForEachLeaf( p->pManRes, pCut, pLeaf, i )
{
// Cost += pLeaf->nRefs;
Cost += Csw_ObjRefs( p, pLeaf );
// printf( "%d ", pLeaf->nRefs );
}
//printf( "\n" );
return Cost * 100 / pCut->nFanins;
}
/**Function*************************************************************
Synopsis [Compute the cost of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline float Csw_CutFindCost2( Csw_Man_t * p, Csw_Cut_t * pCut )
{
Aig_Obj_t * pLeaf;
float Cost = 0.0;
int i;
assert( pCut->nFanins > 0 );
Csw_CutForEachLeaf( p->pManRes, pCut, pLeaf, i )
Cost += (float)1.0/pLeaf->nRefs;
return 1/Cost;
}
/**Function*************************************************************
Synopsis [Returns the next free cut to use.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Csw_Cut_t * Csw_CutFindFree( Csw_Man_t * p, Aig_Obj_t * pObj )
{
Csw_Cut_t * pCut, * pCutMax;
int i;
pCutMax = NULL;
Csw_ObjForEachCut( p, pObj, pCut, i )
{
if ( pCut->nFanins == 0 )
return pCut;
if ( pCutMax == NULL || pCutMax->Cost < pCut->Cost )
pCutMax = pCut;
}
assert( pCutMax != NULL );
pCutMax->nFanins = 0;
return pCutMax;
}
/**Function*************************************************************
Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Cut_TruthPhase( Csw_Cut_t * pCut, Csw_Cut_t * pCut1 )
{
unsigned uPhase = 0;
int i, k;
for ( i = k = 0; i < pCut->nFanins; i++ )
{
if ( k == pCut1->nFanins )
break;
if ( pCut->pFanins[i] < pCut1->pFanins[k] )
continue;
assert( pCut->pFanins[i] == pCut1->pFanins[k] );
uPhase |= (1 << i);
k++;
}
return uPhase;
}
/**Function*************************************************************
Synopsis [Performs truth table computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Csw_CutComputeTruth( Csw_Man_t * p, Csw_Cut_t * pCut, Csw_Cut_t * pCut0, Csw_Cut_t * pCut1, int fCompl0, int fCompl1 )
{
// permute the first table
if ( fCompl0 )
Kit_TruthNot( p->puTemp[0], Csw_CutTruth(pCut0), p->nLeafMax );
else
Kit_TruthCopy( p->puTemp[0], Csw_CutTruth(pCut0), p->nLeafMax );
Kit_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nFanins, p->nLeafMax, Cut_TruthPhase(pCut, pCut0), 0 );
// permute the second table
if ( fCompl1 )
Kit_TruthNot( p->puTemp[1], Csw_CutTruth(pCut1), p->nLeafMax );
else
Kit_TruthCopy( p->puTemp[1], Csw_CutTruth(pCut1), p->nLeafMax );
Kit_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nFanins, p->nLeafMax, Cut_TruthPhase(pCut, pCut1), 0 );
// produce the resulting table
Kit_TruthAnd( Csw_CutTruth(pCut), p->puTemp[2], p->puTemp[3], p->nLeafMax );
// assert( pCut->nFanins >= Kit_TruthSupportSize( Csw_CutTruth(pCut), p->nLeafMax ) );
return Csw_CutTruth(pCut);
}
/**Function*************************************************************
Synopsis [Performs support minimization for the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Csw_CutSupportMinimize( Csw_Man_t * p, Csw_Cut_t * pCut )
{
unsigned * pTruth;
int uSupp, nFansNew, i, k;
// get truth table
pTruth = Csw_CutTruth( pCut );
// get support
uSupp = Kit_TruthSupport( pTruth, p->nLeafMax );
// get the new support size
nFansNew = Kit_WordCountOnes( uSupp );
// check if there are redundant variables
if ( nFansNew == pCut->nFanins )
return nFansNew;
assert( nFansNew < pCut->nFanins );
// minimize support
Kit_TruthShrink( p->puTemp[0], pTruth, nFansNew, p->nLeafMax, uSupp, 1 );
for ( i = k = 0; i < pCut->nFanins; i++ )
if ( uSupp & (1 << i) )
pCut->pFanins[k++] = pCut->pFanins[i];
assert( k == nFansNew );
pCut->nFanins = nFansNew;
// assert( nFansNew == Kit_TruthSupportSize( pTruth, p->nLeafMax ) );
//Extra_PrintBinary( stdout, pTruth, (1<<p->nLeafMax) ); printf( "\n" );
return nFansNew;
}
/**Function*************************************************************
Synopsis [Returns 1 if pDom is contained in pCut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Csw_CutCheckDominance( Csw_Cut_t * pDom, Csw_Cut_t * pCut )
{
int i, k;
for ( i = 0; i < (int)pDom->nFanins; i++ )
{
for ( k = 0; k < (int)pCut->nFanins; k++ )
if ( pDom->pFanins[i] == pCut->pFanins[k] )
break;
if ( k == (int)pCut->nFanins ) // node i in pDom is not contained in pCut
return 0;
}
// every node in pDom is contained in pCut
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if the cut is contained.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Csw_CutFilter( Csw_Man_t * p, Aig_Obj_t * pObj, Csw_Cut_t * pCut )
{
Csw_Cut_t * pTemp;
int i;
// go through the cuts of the node
Csw_ObjForEachCut( p, pObj, pTemp, i )
{
if ( pTemp->nFanins < 2 )
continue;
if ( pTemp == pCut )
continue;
if ( pTemp->nFanins > pCut->nFanins )
{
// skip the non-contained cuts
if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
continue;
// check containment seriously
if ( Csw_CutCheckDominance( pCut, pTemp ) )
{
// remove contained cut
pTemp->nFanins = 0;
}
}
else
{
// skip the non-contained cuts
if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
continue;
// check containment seriously
if ( Csw_CutCheckDominance( pTemp, pCut ) )
{
// remove the given
pCut->nFanins = 0;
return 1;
}
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Merges two cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Csw_CutMergeOrdered( Csw_Man_t * p, Csw_Cut_t * pC0, Csw_Cut_t * pC1, Csw_Cut_t * pC )
{
int i, k, c;
assert( pC0->nFanins >= pC1->nFanins );
// the case of the largest cut sizes
if ( pC0->nFanins == p->nLeafMax && pC1->nFanins == p->nLeafMax )
{
for ( i = 0; i < pC0->nFanins; i++ )
if ( pC0->pFanins[i] != pC1->pFanins[i] )
return 0;
for ( i = 0; i < pC0->nFanins; i++ )
pC->pFanins[i] = pC0->pFanins[i];
pC->nFanins = pC0->nFanins;
return 1;
}
// the case when one of the cuts is the largest
if ( pC0->nFanins == p->nLeafMax )
{
for ( i = 0; i < pC1->nFanins; i++ )
{
for ( k = pC0->nFanins - 1; k >= 0; k-- )
if ( pC0->pFanins[k] == pC1->pFanins[i] )
break;
if ( k == -1 ) // did not find
return 0;
}
for ( i = 0; i < pC0->nFanins; i++ )
pC->pFanins[i] = pC0->pFanins[i];
pC->nFanins = pC0->nFanins;
return 1;
}
// compare two cuts with different numbers
i = k = 0;
for ( c = 0; c < p->nLeafMax; c++ )
{
if ( k == pC1->nFanins )
{
if ( i == pC0->nFanins )
{
pC->nFanins = c;
return 1;
}
pC->pFanins[c] = pC0->pFanins[i++];
continue;
}
if ( i == pC0->nFanins )
{
if ( k == pC1->nFanins )
{
pC->nFanins = c;
return 1;
}
pC->pFanins[c] = pC1->pFanins[k++];
continue;
}
if ( pC0->pFanins[i] < pC1->pFanins[k] )
{
pC->pFanins[c] = pC0->pFanins[i++];
continue;
}
if ( pC0->pFanins[i] > pC1->pFanins[k] )
{
pC->pFanins[c] = pC1->pFanins[k++];
continue;
}
pC->pFanins[c] = pC0->pFanins[i++];
k++;
}
if ( i < pC0->nFanins || k < pC1->nFanins )
return 0;
pC->nFanins = c;
return 1;
}
/**Function*************************************************************
Synopsis [Prepares the object for FPGA mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Csw_CutMerge( Csw_Man_t * p, Csw_Cut_t * pCut0, Csw_Cut_t * pCut1, Csw_Cut_t * pCut )
{
assert( p->nLeafMax > 0 );
// merge the nodes
if ( pCut0->nFanins < pCut1->nFanins )
{
if ( !Csw_CutMergeOrdered( p, pCut1, pCut0, pCut ) )
return 0;
}
else
{
if ( !Csw_CutMergeOrdered( p, pCut0, pCut1, pCut ) )
return 0;
}
pCut->uSign = pCut0->uSign | pCut1->uSign;
return 1;
}
/**Function*************************************************************
Synopsis [Consider cut with more than 2 fanins having 2 true variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Csw_ObjTwoVarCut( Csw_Man_t * p, Csw_Cut_t * pCut )
{
Aig_Obj_t * pRes, * pIn0, * pIn1;
int nVars, uTruth, fCompl = 0;
assert( pCut->nFanins > 2 );
// minimize support of this cut
nVars = Csw_CutSupportMinimize( p, pCut );
assert( nVars == 2 );
// get the fanins
pIn0 = Aig_ManObj( p->pManRes, pCut->pFanins[0] );
pIn1 = Aig_ManObj( p->pManRes, pCut->pFanins[1] );
// derive the truth table
uTruth = 0xF & *Csw_CutTruth(pCut);
if ( uTruth == 14 || uTruth == 13 || uTruth == 11 || uTruth == 7 )
{
uTruth = 0xF & ~uTruth;
fCompl = 1;
}
// compute the result
pRes = NULL;
if ( uTruth == 1 ) // 0001 // 1110 14
pRes = Aig_And( p->pManRes, Aig_Not(pIn0), Aig_Not(pIn1) );
if ( uTruth == 2 ) // 0010 // 1101 13
pRes = Aig_And( p->pManRes, pIn0 , Aig_Not(pIn1) );
if ( uTruth == 4 ) // 0100 // 1011 11
pRes = Aig_And( p->pManRes, Aig_Not(pIn0), pIn1 );
if ( uTruth == 8 ) // 1000 // 0111 7
pRes = Aig_And( p->pManRes, pIn0 , pIn1 );
if ( pRes )
pRes = Aig_NotCond( pRes, fCompl );
return pRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv )
{
Csw_Cut_t * pCutSet, * pCut;
int i;
// create the cutset of the node
pCutSet = (Csw_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
Csw_ObjSetCuts( p, pObj, pCutSet );
Csw_ObjForEachCut( p, pObj, pCut, i )
{
pCut->nFanins = 0;
pCut->iNode = pObj->Id;
pCut->nCutSize = p->nCutSize;
pCut->nLeafMax = p->nLeafMax;
}
// add unit cut if needed
if ( fTriv )
{
pCut = pCutSet;
pCut->Cost = 0;
pCut->iNode = pObj->Id;
pCut->nFanins = 1;
pCut->pFanins[0] = pObj->Id;
pCut->uSign = Aig_ObjCutSign( pObj->Id );
memset( Csw_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords );
}
return pCutSet;
}
/**Function*************************************************************
Synopsis [Derives cuts for one node and sweeps this node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv )
{
int fUseResub = 1;
Csw_Cut_t * pCut0, * pCut1, * pCut, * pCutSet;
Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
Aig_Obj_t * pObjNew;
unsigned * pTruth;
int i, k, nVars, nFanins, iVar, clk;
assert( !Aig_IsComplement(pObj) );
if ( !Aig_ObjIsNode(pObj) )
return pObj;
if ( Csw_ObjCuts(p, pObj) )
return pObj;
// the node is not processed yet
assert( Csw_ObjCuts(p, pObj) == NULL );
assert( Aig_ObjIsNode(pObj) );
// set up the first cut
pCutSet = Csw_ObjPrepareCuts( p, pObj, fTriv );
// compute pair-wise cut combinations while checking table
Csw_ObjForEachCut( p, pFanin0, pCut0, i )
if ( pCut0->nFanins > 0 )
Csw_ObjForEachCut( p, pFanin1, pCut1, k )
if ( pCut1->nFanins > 0 )
{
// make sure K-feasible cut exists
if ( Kit_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->nLeafMax )
continue;
// get the next cut of this node
pCut = Csw_CutFindFree( p, pObj );
clk = clock();
// assemble the new cut
if ( !Csw_CutMerge( p, pCut0, pCut1, pCut ) )
{
assert( pCut->nFanins == 0 );
continue;
}
// check containment
if ( Csw_CutFilter( p, pObj, pCut ) )
{
assert( pCut->nFanins == 0 );
continue;
}
// create its truth table
pTruth = Csw_CutComputeTruth( p, pCut, pCut0, pCut1, Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
// support minimize the truth table
nFanins = pCut->nFanins;
// nVars = Csw_CutSupportMinimize( p, pCut ); // leads to quality degradation
nVars = Kit_TruthSupportSize( pTruth, p->nLeafMax );
p->timeCuts += clock() - clk;
// check for trivial truth tables
if ( nVars == 0 )
{
p->nNodesTriv0++;
return Aig_NotCond( Aig_ManConst1(p->pManRes), !(pTruth[0] & 1) );
}
if ( nVars == 1 )
{
p->nNodesTriv1++;
iVar = Kit_WordFindFirstBit( Kit_TruthSupport(pTruth, p->nLeafMax) );
assert( iVar < pCut->nFanins );
return Aig_NotCond( Aig_ManObj(p->pManRes, pCut->pFanins[iVar]), (pTruth[0] & 1) );
}
if ( nVars == 2 && nFanins > 2 && fUseResub )
{
if ( pObjNew = Csw_ObjTwoVarCut( p, pCut ) )
{
p->nNodesTriv2++;
return pObjNew;
}
}
// check if an equivalent node with the same cut exists
clk = clock();
pObjNew = pCut->nFanins > 2 ? Csw_TableCutLookup( p, pCut ) : NULL;
p->timeHash += clock() - clk;
if ( pObjNew )
{
p->nNodesCuts++;
return pObjNew;
}
// assign the cost
pCut->Cost = Csw_CutFindCost( p, pCut );
assert( pCut->nFanins > 0 );
assert( pCut->Cost > 0 );
}
p->nNodesTried++;
// load the resulting cuts into the table
clk = clock();
Csw_ObjForEachCut( p, pObj, pCut, i )
{
if ( pCut->nFanins > 2 )
{
assert( pCut->Cost > 0 );
Csw_TableCutInsert( p, pCut );
}
}
p->timeHash += clock() - clk;
// return the node if could not replace it
return pObj;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

157
src/aig/csw/cswInt.h Normal file
View File

@ -0,0 +1,157 @@
/**CFile****************************************************************
FileName [cswInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cut sweeping.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 11, 2007.]
Revision [$Id: cswInt.h,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CSW_INT_H__
#define __CSW_INT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "aig.h"
#include "dar.h"
#include "kit.h"
#include "csw.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Csw_Man_t_ Csw_Man_t;
typedef struct Csw_Cut_t_ Csw_Cut_t;
// the cut used to represent node in the AIG
struct Csw_Cut_t_
{
Csw_Cut_t * pNext; // the next cut in the table
int Cost; // the cost of the cut
// float Cost; // the cost of the cut
unsigned uSign; // cut signature
int iNode; // the node, for which it is the cut
short nCutSize; // the number of bytes in the cut
char nLeafMax; // the maximum number of fanins
char nFanins; // the current number of fanins
int pFanins[0]; // the fanins (followed by the truth table)
};
// the CNF computation manager
struct Csw_Man_t_
{
// AIG manager
Aig_Man_t * pManAig; // the input AIG manager
Aig_Man_t * pManRes; // the output AIG manager
Aig_Obj_t ** pEquiv; // the equivalent nodes in the resulting manager
Csw_Cut_t ** pCuts; // the cuts for each node in the output manager
int * pnRefs; // the number of references of each new node
// hash table for cuts
Csw_Cut_t ** pTable; // the table composed of cuts
int nTableSize; // the size of hash table
// parameters
int nCutsMax; // the max number of cuts at the node
int nLeafMax; // the max number of leaves of a cut
int fVerbose; // enables verbose output
// internal variables
int nCutSize; // the number of bytes needed to store one cut
int nTruthWords; // the number of truth table words
Aig_MmFixed_t * pMemCuts; // memory manager for cuts
unsigned * puTemp[4]; // used for the truth table computation
// statistics
int nNodesTriv0; // the number of trivial nodes
int nNodesTriv1; // the number of trivial nodes
int nNodesTriv2; // the number of trivial nodes
int nNodesCuts; // the number of rewritten nodes
int nNodesTried; // the number of nodes tried
int timeCuts; // time to compute the cut and its truth table
int timeHash; // time for hashing cuts
int timeOther; // other time
int timeTotal; // total time
};
static inline int Csw_CutLeaveNum( Csw_Cut_t * pCut ) { return pCut->nFanins; }
static inline int * Csw_CutLeaves( Csw_Cut_t * pCut ) { return pCut->pFanins; }
static inline unsigned * Csw_CutTruth( Csw_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nLeafMax); }
static inline Csw_Cut_t * Csw_CutNext( Csw_Cut_t * pCut ) { return (Csw_Cut_t *)(((char *)pCut) + pCut->nCutSize); }
static inline int Csw_ObjRefs( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pnRefs[pObj->Id]; }
static inline void Csw_ObjAddRefs( Csw_Man_t * p, Aig_Obj_t * pObj, int nRefs ) { p->pnRefs[pObj->Id] += nRefs; }
static inline Csw_Cut_t * Csw_ObjCuts( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pCuts[pObj->Id]; }
static inline void Csw_ObjSetCuts( Csw_Man_t * p, Aig_Obj_t * pObj, Csw_Cut_t * pCuts ) { p->pCuts[pObj->Id] = pCuts; }
static inline Aig_Obj_t * Csw_ObjEquiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquiv[pObj->Id]; }
static inline void Csw_ObjSetEquiv( Csw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEquiv ) { p->pEquiv[pObj->Id] = pEquiv; }
static inline Aig_Obj_t * Csw_ObjChild0Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Csw_ObjChild1Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
// iterator over cuts of the node
#define Csw_ObjForEachCut( p, pObj, pCut, i ) \
for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(pCut) )
// iterator over leaves of the cut
#define Csw_CutForEachLeaf( p, pCut, pLeaf, i ) \
for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cnfCut.c ========================================================*/
extern Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv );
extern Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv );
/*=== cnfMan.c ========================================================*/
extern Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose );
extern void Csw_ManStop( Csw_Man_t * p );
/*=== cnfTable.c ========================================================*/
extern int Csw_TableCountCuts( Csw_Man_t * p );
extern void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut );
extern Aig_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

125
src/aig/csw/cswMan.c Normal file
View File

@ -0,0 +1,125 @@
/**CFile****************************************************************
FileName [cswMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cut sweeping.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 11, 2007.]
Revision [$Id: cswMan.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the cut sweeping manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose )
{
Csw_Man_t * p;
Aig_Obj_t * pObj;
int i;
assert( nCutsMax >= 2 );
assert( nLeafMax <= 16 );
// allocate the fraiging manager
p = ALLOC( Csw_Man_t, 1 );
memset( p, 0, sizeof(Csw_Man_t) );
p->nCutsMax = nCutsMax;
p->nLeafMax = nLeafMax;
p->fVerbose = fVerbose;
p->pManAig = pMan;
// create the new manager
p->pManRes = Aig_ManStartFrom( pMan );
assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManRes) );
// allocate room for cuts and equivalent nodes
p->pnRefs = ALLOC( int, Aig_ManObjNumMax(pMan) );
p->pEquiv = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pMan) );
p->pCuts = ALLOC( Csw_Cut_t *, Aig_ManObjNumMax(pMan) );
memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) );
memset( p->pnRefs, 0, sizeof(int) * Aig_ManObjNumMax(pMan) );
// allocate memory manager
p->nTruthWords = Aig_TruthWordNum(nLeafMax);
p->nCutSize = sizeof(Csw_Cut_t) + sizeof(int) * nLeafMax + sizeof(unsigned) * p->nTruthWords;
p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
// allocate hash table for cuts
p->nTableSize = Aig_PrimeCudd( Aig_ManNodeNum(pMan) * p->nCutsMax / 2 );
p->pTable = ALLOC( Csw_Cut_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
// set the pointers to the available fraig nodes
Csw_ObjSetEquiv( p, Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManRes) );
Aig_ManForEachPi( p->pManAig, pObj, i )
Csw_ObjSetEquiv( p, pObj, Aig_ManPi(p->pManRes, i) );
// room for temporary truth tables
p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
return p;
}
/**Function*************************************************************
Synopsis [Stops the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Csw_ManStop( Csw_Man_t * p )
{
if ( p->fVerbose )
{
int nNodesBeg = Aig_ManNodeNum(p->pManAig);
int nNodesEnd = Aig_ManNodeNum(p->pManRes);
printf( "Beg = %7d. End = %7d. (%6.2f %%) Try = %7d. Cuts = %8d.\n",
nNodesBeg, nNodesEnd, 100.0*(nNodesBeg-nNodesEnd)/nNodesBeg,
p->nNodesTried, Csw_TableCountCuts( p ) );
printf( "Triv0 = %6d. Triv1 = %6d. Triv2 = %6d. Cut-replace = %6d.\n",
p->nNodesTriv0, p->nNodesTriv1, p->nNodesTriv2, p->nNodesCuts );
PRTP( "Cuts ", p->timeCuts, p->timeTotal );
PRTP( "Hashing ", p->timeHash, p->timeTotal );
PRTP( "Other ", p->timeOther, p->timeTotal );
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
free( p->puTemp[0] );
Aig_MmFixedStop( p->pMemCuts, 0 );
free( p->pnRefs );
free( p->pEquiv );
free( p->pCuts );
free( p->pTable );
free( p );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

161
src/aig/csw/cswTable.c Normal file
View File

@ -0,0 +1,161 @@
/**CFile****************************************************************
FileName [cswTable.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cut sweeping.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 11, 2007.]
Revision [$Id: cswTable.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes hash value of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Csw_CutHash( Csw_Cut_t * pCut )
{
static int s_FPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned uHash;
int i;
assert( pCut->nFanins <= 16 );
uHash = 0;
for ( i = 0; i < pCut->nFanins; i++ )
uHash ^= pCut->pFanins[i] * s_FPrimes[i];
return uHash;
}
/**Function*************************************************************
Synopsis [Returns the total number of cuts in the table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Csw_TableCountCuts( Csw_Man_t * p )
{
Csw_Cut_t * pEnt;
int i, Counter = 0;
for ( i = 0; i < p->nTableSize; i++ )
for ( pEnt = p->pTable[i]; pEnt; pEnt = pEnt->pNext )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis [Adds the cut to the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut )
{
int iEntry = Csw_CutHash(pCut) % p->nTableSize;
pCut->pNext = p->pTable[iEntry];
p->pTable[iEntry] = pCut;
}
/**Function*************************************************************
Synopsis [Returns an equivalent node if it exists.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut )
{
Aig_Obj_t * pRes = NULL;
Csw_Cut_t * pEnt;
unsigned * pTruthNew, * pTruthOld;
int iEntry = Csw_CutHash(pCut) % p->nTableSize;
for ( pEnt = p->pTable[iEntry]; pEnt; pEnt = pEnt->pNext )
{
if ( pEnt->nFanins != pCut->nFanins )
continue;
if ( pEnt->uSign != pCut->uSign )
continue;
if ( memcmp( pEnt->pFanins, pCut->pFanins, sizeof(int) * pCut->nFanins ) )
continue;
pTruthOld = Csw_CutTruth(pEnt);
pTruthNew = Csw_CutTruth(pCut);
if ( (pTruthOld[0] & 1) == (pTruthNew[0] & 1) )
{
if ( Kit_TruthIsEqual( pTruthOld, pTruthNew, pCut->nFanins ) )
{
pRes = Aig_ManObj( p->pManRes, pEnt->iNode );
assert( pRes->fPhase == Aig_ManObj( p->pManRes, pCut->iNode )->fPhase );
break;
}
}
else
{
if ( Kit_TruthIsOpposite( pTruthOld, pTruthNew, pCut->nFanins ) )
{
pRes = Aig_Not( Aig_ManObj( p->pManRes, pEnt->iNode ) );
assert( Aig_Regular(pRes)->fPhase != Aig_ManObj( p->pManRes, pCut->iNode )->fPhase );
break;
}
}
}
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

48
src/aig/csw/csw_.c Normal file
View File

@ -0,0 +1,48 @@
/**CFile****************************************************************
FileName [csw_.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Cut sweeping.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - July 11, 2007.]
Revision [$Id: csw_.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/aig/csw/module.make Normal file
View File

@ -0,0 +1,4 @@
SRC += src/aig/csw/cswCore.c \
src/aig/csw/cswCut.c \
src/aig/csw/cswMan.c \
src/aig/csw/cswTable.c

View File

@ -36,7 +36,7 @@ extern "C" {
#include <time.h>
//#include "bar.h"
#include "vec2.h"
#include "vec.h"
#include "aig.h"
#include "dar.h"

View File

@ -18,8 +18,8 @@
***********************************************************************/
#include "kit.h"
#include "darInt.h"
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///

703
src/aig/deco/deco.h Normal file
View File

@ -0,0 +1,703 @@
/**CFile****************************************************************
FileName [deco.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [A simple decomposition tree/node data structure and its APIs.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: deco.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __DEC_H__
#define __DEC_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Dec_Edge_t_ Dec_Edge_t;
struct Dec_Edge_t_
{
unsigned fCompl : 1; // the complemented bit
unsigned Node : 30; // the decomposition node pointed by the edge
};
typedef struct Dec_Node_t_ Dec_Node_t;
struct Dec_Node_t_
{
Dec_Edge_t eEdge0; // the left child of the node
Dec_Edge_t eEdge1; // the right child of the node
// other info
void * pFunc; // the function of the node (BDD or AIG)
unsigned Level : 14; // the level of this node in the global AIG
// printing info
unsigned fNodeOr : 1; // marks the original OR node
unsigned fCompl0 : 1; // marks the original complemented edge
unsigned fCompl1 : 1; // marks the original complemented edge
// latch info
unsigned nLat0 : 5; // the number of latches on the first edge
unsigned nLat1 : 5; // the number of latches on the second edge
unsigned nLat2 : 5; // the number of latches on the output edge
};
typedef struct Dec_Graph_t_ Dec_Graph_t;
struct Dec_Graph_t_
{
int fConst; // marks the constant 1 graph
int nLeaves; // the number of leaves
int nSize; // the number of nodes (including the leaves)
int nCap; // the number of allocated nodes
Dec_Node_t * pNodes; // the array of leaves and internal nodes
Dec_Edge_t eRoot; // the pointer to the topmost node
};
typedef struct Dec_Man_t_ Dec_Man_t;
struct Dec_Man_t_
{
void * pMvcMem; // memory manager for MVC cover (used for factoring)
Vec_Int_t * vCubes; // storage for cubes
Vec_Int_t * vLits; // storage for literals
// precomputation information about 4-variable functions
unsigned short * puCanons; // canonical forms
char * pPhases; // canonical phases
char * pPerms; // canonical permutations
unsigned char * pMap; // mapping of functions into class numbers
};
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
////////////////////////////////////////////////////////////////////////
// interator throught the leaves
#define Dec_GraphForEachLeaf( pGraph, pLeaf, i ) \
for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Dec_GraphNode(pGraph, i)), 1); i++ )
// interator throught the internal nodes
#define Dec_GraphForEachNode( pGraph, pAnd, i ) \
for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Dec_GraphNode(pGraph, i)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Creates an edge pointing to the node in the given polarity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl )
{
Dec_Edge_t eEdge = { fCompl, Node };
return eEdge;
}
/**Function*************************************************************
Synopsis [Converts the edge into unsigned integer.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge )
{
return (eEdge.Node << 1) | eEdge.fCompl;
}
/**Function*************************************************************
Synopsis [Converts unsigned integer into the edge.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge )
{
return Dec_EdgeCreate( Edge >> 1, Edge & 1 );
}
/**Function*************************************************************
Synopsis [Converts the edge into unsigned integer.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge )
{
return *(unsigned *)&eEdge;
}
/**Function*************************************************************
Synopsis [Converts unsigned integer into the edge.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge )
{
return *(Dec_Edge_t *)&Edge;
}
/**Function*************************************************************
Synopsis [Creates a graph with the given number of leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves )
{
Dec_Graph_t * pGraph;
pGraph = ALLOC( Dec_Graph_t, 1 );
memset( pGraph, 0, sizeof(Dec_Graph_t) );
pGraph->nLeaves = nLeaves;
pGraph->nSize = nLeaves;
pGraph->nCap = 2 * nLeaves + 50;
pGraph->pNodes = ALLOC( Dec_Node_t, pGraph->nCap );
memset( pGraph->pNodes, 0, sizeof(Dec_Node_t) * pGraph->nSize );
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates constant 0 graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateConst0()
{
Dec_Graph_t * pGraph;
pGraph = ALLOC( Dec_Graph_t, 1 );
memset( pGraph, 0, sizeof(Dec_Graph_t) );
pGraph->fConst = 1;
pGraph->eRoot.fCompl = 1;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates constant 1 graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateConst1()
{
Dec_Graph_t * pGraph;
pGraph = ALLOC( Dec_Graph_t, 1 );
memset( pGraph, 0, sizeof(Dec_Graph_t) );
pGraph->fConst = 1;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates the literal graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Graph_t * Dec_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl )
{
Dec_Graph_t * pGraph;
assert( 0 <= iLeaf && iLeaf < nLeaves );
pGraph = Dec_GraphCreate( nLeaves );
pGraph->eRoot.Node = iLeaf;
pGraph->eRoot.fCompl = fCompl;
return pGraph;
}
/**Function*************************************************************
Synopsis [Creates a graph with the given number of leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dec_GraphFree( Dec_Graph_t * pGraph )
{
FREE( pGraph->pNodes );
free( pGraph );
}
/**Function*************************************************************
Synopsis [Returns 1 if the graph is a constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )
{
return pGraph->fConst;
}
/**Function*************************************************************
Synopsis [Returns 1 if the graph is constant 0.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )
{
return pGraph->fConst && pGraph->eRoot.fCompl;
}
/**Function*************************************************************
Synopsis [Returns 1 if the graph is constant 1.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )
{
return pGraph->fConst && !pGraph->eRoot.fCompl;
}
/**Function*************************************************************
Synopsis [Returns 1 if the graph is complemented.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsComplement( Dec_Graph_t * pGraph )
{
return pGraph->eRoot.fCompl;
}
/**Function*************************************************************
Synopsis [Checks if the graph is complemented.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dec_GraphComplement( Dec_Graph_t * pGraph )
{
pGraph->eRoot.fCompl ^= 1;
}
/**Function*************************************************************
Synopsis [Returns the number of leaves.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph )
{
return pGraph->nLeaves;
}
/**Function*************************************************************
Synopsis [Returns the number of internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph )
{
return pGraph->nSize - pGraph->nLeaves;
}
/**Function*************************************************************
Synopsis [Returns the pointer to the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i )
{
return pGraph->pNodes + i;
}
/**Function*************************************************************
Synopsis [Returns the pointer to the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Node_t * Dec_GraphNodeLast( Dec_Graph_t * pGraph )
{
return pGraph->pNodes + pGraph->nSize - 1;
}
/**Function*************************************************************
Synopsis [Returns the number of the given node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
{
return pNode - pGraph->pNodes;
}
/**Function*************************************************************
Synopsis [Check if the graph represents elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )
{
return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
}
/**Function*************************************************************
Synopsis [Check if the graph represents elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
{
return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
}
/**Function*************************************************************
Synopsis [Returns the elementary variable elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Node_t * Dec_GraphVar( Dec_Graph_t * pGraph )
{
assert( Dec_GraphIsVar( pGraph ) );
return Dec_GraphNode( pGraph, pGraph->eRoot.Node );
}
/**Function*************************************************************
Synopsis [Returns the number of the elementary variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dec_GraphVarInt( Dec_Graph_t * pGraph )
{
assert( Dec_GraphIsVar( pGraph ) );
return Dec_GraphNodeInt( pGraph, Dec_GraphVar(pGraph) );
}
/**Function*************************************************************
Synopsis [Sets the root of the graph.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dec_GraphSetRoot( Dec_Graph_t * pGraph, Dec_Edge_t eRoot )
{
pGraph->eRoot = eRoot;
}
/**Function*************************************************************
Synopsis [Appends a new node to the graph.]
Description [This procedure is meant for internal use.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Node_t * Dec_GraphAppendNode( Dec_Graph_t * pGraph )
{
Dec_Node_t * pNode;
if ( pGraph->nSize == pGraph->nCap )
{
pGraph->pNodes = REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap );
pGraph->nCap = 2 * pGraph->nCap;
}
pNode = pGraph->pNodes + pGraph->nSize++;
memset( pNode, 0, sizeof(Dec_Node_t) );
return pNode;
}
/**Function*************************************************************
Synopsis [Creates an AND node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeAnd( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
{
Dec_Node_t * pNode;
// get the new node
pNode = Dec_GraphAppendNode( pGraph );
// set the inputs and other info
pNode->eEdge0 = eEdge0;
pNode->eEdge1 = eEdge1;
pNode->fCompl0 = eEdge0.fCompl;
pNode->fCompl1 = eEdge1.fCompl;
return Dec_EdgeCreate( pGraph->nSize - 1, 0 );
}
/**Function*************************************************************
Synopsis [Creates an OR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
{
Dec_Node_t * pNode;
// get the new node
pNode = Dec_GraphAppendNode( pGraph );
// set the inputs and other info
pNode->eEdge0 = eEdge0;
pNode->eEdge1 = eEdge1;
pNode->fCompl0 = eEdge0.fCompl;
pNode->fCompl1 = eEdge1.fCompl;
// make adjustments for the OR gate
pNode->fNodeOr = 1;
pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
return Dec_EdgeCreate( pGraph->nSize - 1, 1 );
}
/**Function*************************************************************
Synopsis [Creates an XOR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1, int Type )
{
Dec_Edge_t eNode0, eNode1, eNode;
if ( Type == 0 )
{
// derive the first AND
eEdge0.fCompl ^= 1;
eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
eEdge0.fCompl ^= 1;
// derive the second AND
eEdge1.fCompl ^= 1;
eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the final OR
eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
}
else
{
// derive the first AND
eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the second AND
eEdge0.fCompl ^= 1;
eEdge1.fCompl ^= 1;
eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
// derive the final OR
eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
eNode.fCompl ^= 1;
}
return eNode;
}
/**Function*************************************************************
Synopsis [Creates an XOR node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t eEdgeC, Dec_Edge_t eEdgeT, Dec_Edge_t eEdgeE, int Type )
{
Dec_Edge_t eNode0, eNode1, eNode;
if ( Type == 0 )
{
// derive the first AND
eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
// derive the second AND
eEdgeC.fCompl ^= 1;
eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
// derive the final OR
eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
}
else
{
// complement the arguments
eEdgeT.fCompl ^= 1;
eEdgeE.fCompl ^= 1;
// derive the first AND
eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
// derive the second AND
eEdgeC.fCompl ^= 1;
eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
// derive the final OR
eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
eNode.fCompl ^= 1;
}
return eNode;
}
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -35,7 +35,7 @@ extern "C" {
#include <assert.h>
#include <time.h>
#include "vec2.h"
#include "vec.h"
#include "aig.h"
#include "dar.h"
#include "satSolver.h"

Some files were not shown because too many files have changed in this diff Show More