abctcl — control the ABC synthesis system
ABCTcl is a collection of procedures that control the ABC synthesis system using Expect. A typical procedure of the collection performs a single ABC command, then parses its output and provide it in an array.
The following procedures are defined. For detailed description, see their respective manual pages.
result]
[timeout]
Starts ABC, commands it to source configured initialization files.
Commands ABC to stop and closes the communication.
command
[result]
[timeout]
Sends command to ABC. No parsing is done on its output.
file
[result]
[params]
[timeout]
Commands ABC to source an ABC script.
result]
[params]
[timeout]
Commands ABC to read a circuit description. The type of the input is determined by the suffix of the file.
result]
[params]
[timeout]
,
abc::print_latch
[result]
[params]
[timeout]
,
abc::print_auto
[result]
[params]
[timeout]
,
abc::print_fanio
[result]
[params]
[timeout]
,
abc::print_gates
[result]
[params]
[timeout]
,
abc::print_symm
[result]
[params]
[timeout]
,
abc::print_unate
[result]
[params]
[timeout]
Invoke respective ABC commands. Parse the output so that the reported data can be used for evaluation and control.
result]
[params]
[timeout]
,
abc::cec
[result]
[params]
[timeout]
,
abc::dsec
[result]
[params]
[timeout]
,
abc::dprove
[result]
[params]
[timeout]
Check circuit equivalence using respective ABC commands.
result]
[params]
[timeout]
,
abc::prove
[result]
[params]
[timeout]
,
abc::sat
[result]
[params]
[timeout]
Solve an instance of the boolean satisfiability problem using respective ABC commands.
result]
[params]
[timeout]
Obtain and parse ABC time report.
The equivalence checking procedures and satisfiability procedures return a structured string (see abc::messages(n) ) indicating their results. Other procedures return empty strings. All procedures use
return -code ok
if no error occurs,
return -code error -errorcode code -errorinfo info
otherwise.
code defaults to NONE if no error occured.
See
abc::messages(n)
for the structure of code and info
for possible values and their semantics.
ABCTcl uses the file abctcl.conf.tcl for configuration.
It searches for that file in the same directory where abctcl.tcl
is located. The file itself is Tcl code. For variables that can
be configured there, see
abctcl.conf.tcl(5)
.
The program below is a tiny but complete example. It reads
a circuit from a file specified on the command line and decides
whether it is sequential or combinatorial. The locations
of tclsh and abctcl.tcl may, of course, vary.
#!/usr/bin/tclsh
source /usr/local/libexec/abctcl.tcl
abc::init
abc::read {} [lindex $argv 0]
abc::print_latch result
if {$result(total_latches) == 0} {
puts "combinational"
} else {
puts "sequential"
}
abc::done
abctcl.conf.tcl(5), abc::messages(n), abc::init(n), abc::done(n), abc::command(n), abc::source(n), abc::read(n), abc::print_stats(n), abc::print_latch(n), abc::print_auto(n), abc::print_fanio(n), abc::print_gates(n), abc::print_symm(n), abc::print_unate(n), abc::sec(n), abc::sat(n), abc::time(n)