Chapter 1. Reference Pages

Table of Contents

TCL programming interface to ABC
Introduction, configuration and error messages
Start, termination and and general commands
Reading circuit data and scripts
Obtaining circuit characteristics
Comparing circuits
Solving Satisfiability instances
Command-line utilities
Graphical user interface

TCL programming interface to ABC

Introduction, configuration and error messages

Start, termination and and general commands

Reading circuit data and scripts

Obtaining circuit characteristics

Comparing circuits

Solving Satisfiability instances


abctcl

Name

abctcl — control the ABC synthesis system

DESCRIPTION

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.

abc::init
 [result]
 [timeout]

Starts ABC, commands it to source configured initialization files.

abc::done

Commands ABC to stop and closes the communication.

abc::command command [result] [timeout]

Sends command to ABC. No parsing is done on its output.

abc::source
  file
 [result]
 [params]
 [timeout]

Commands ABC to source an ABC script.

abc::read
 [result]
 [params]
 [timeout]

Commands ABC to read a circuit description. The type of the input is determined by the suffix of the file.

    abc::print_stats
     [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.

    abc::sec
     [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.

    abc::iprove
     [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.

abc::time
 [result]
 [params]
 [timeout]

Obtain and parse ABC time report.

RETURN CODES

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.

CONFIGURATION

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) .

EXAMPLE

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

BUGS

The collection should be installed as a Tcl package.

SEE ALSO

   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)


abctcl.conf.tcl

Name

abctcl.conf.tcl — ABCTcl configuration file

DESCRIPTION

The file abctcl.conf.tcl is a piece of Tcl code, executed when the file is sourced by an application (e.g abctclgui). It sets variables configuration variables to default values, in some cases determined during installation of ABCTcl

For computation of the values, all Tcl global variables and Tcl commands are available (see tclvars(n)).

VARIABLES

int timeout

Default timeout of an ABC command. Procedures sending commands to ABC can have a `local' timeout as an argument. This, however, does not affect the value of this variable. The variable is global and is defined by Expect. Can be overriden at any time between ABC commands.

string abc::expect_buffer_size

Maximum size of ABC's output. Used by Expect. Set to 100kB. Can be overriden at any time between ABC commands.

string abc::dir

The directory with ABC executable. The path shall be absolute. Set to the directory determined by configure during installation. The value can but needs not to end with a path separator (`/' or `\'). Can be overriden before the call to abc::init.

string abc::exe

The name of ABC executable. Determined by configure during installation. Can be overriden before the call to abc::init.

list of string abc::initList

Each string is a name of an ABC script, for example the standard /fIabc.rc/fR script. The order in which the files are sourced is given by their order in the list. Notice that all files are attemtpted to be read, unlike the initialization schemes built into ABC. For files read when the default value applies, see DEFAULT ABC INITIALIZATION

DEFAULT ABC INITIALIZATION

The order and locations of initialization files are similar to those built into ABC. As in ABC, they differ across platform types. abctcl.conf.tcl uses the Tcl variable $tcl_platform(platform) to detect the platform type. Unlike ABC, ABCTcl tries to read each file if it exists.

Windows

  • An abc.rc file two levels up from the current directory.

  • An abc.rc file one level up from the current directory.

  • An abc.rc file in the current directory.

Unix

  • The `system' abc.rc file located during installation (see THE SYSTEM-WIDE ABC.RC LOCATION)

  • If the environment variable HOME is set to a non-empty value, a .abc.rc file the directory (usually, the user's home directory).

  • A .abc.rc in the current directory.

The order is from general files to files particular for a user or a problem, so that the more specific file has a chance to redefine some ABC's aliases and other things. The value of abc::initList can be overriden before the call to abc::init.

THE SYSTEM-WIDE ABC.RC LOCATION

The location of the abc.rc file can be set by an argument to configure. If it is not, configure searches in the following directories for abc.rc, assuming that abcdir is the directory where the ABC executable is:

  • abcdir

  • abcdir/../lib

  • abcdir/../lib/abc

The first file found is the system-wide abc.rc file.

BUGS

  • The mechanism using abc::initList has been built because the sequences built into ABC do not cover usual needs. We do not have, however, an option to switch this mechanism off and to revert to the built-in sequences.

  • To model standard ABC initialization sequences more closely, we would need a structure more sophisticated than a mere list. It should be able to express the notions of `the fist one from a list that can be found' and `all of the list that can be found'. The present solution trades expresiveness for simplicity.

SEE ALSO

expect(1),
tclvars(5),

    abc::init(n)


abc::messages

Name

abc::messages, abc::errorReturn, abc::consCode, abc::extrSymb, abc::extrSeverity — error messages and message manipulation functions

Synopsis

abc::errorReturn retArrayName symbol [par...]

abc::consCode symbol [par...]

abc::extrSymb errorcode

abc::extrSeverity errorcode

DESCRIPTION

Symbolic error code structure

An ABCTcl error code is structured as symbol explanation. The symbol has the form ABC_S_XXX, where S is a letter indicating severity, and XXX determines the error. explanation is a human-readable text.

Variables

abc::messages

An associative array. For each error symbol used by ABCTcl, it contains a human-readable explanation that can be used by Tcl format. Set up when the abctcl.tcl file is sourced.

Procedures

abc::errorReturn retArrayName symbol [par...]

When called from a procedure, it causes that procedure to return with error. The Tcl variable ::errorCode is constructed from the provided symbol and the explanation from abc::messages, using pars when required by the explanation. The value is also stored in retArray(errorCode). Also the value of ::errorInfo is derived from the constructed error code.

Returns empty string. Used internally by all ABCTcl procedures.

abc::consCode symbol [par...]

Returns an error code constructed from the provided symbol and the explanation from abc::messages, using pars when required by the explanation. Used internally by abc::errorReturn.

abc::extrSymb errorcode

Returns the error symbol contained in errorcode.

abc::extrSeverity errorcode

Returns the letter specifying severity from an error code or an error symbol in errorcode.

SYMBOLOIC CODES

Notices

Error Code: ABC_N_EQ_YES
Explanation: The networks are equivalent.
Error Code: ABC_N_SAT_YES
Explanation: The formula is satisfiable.
Error Code: ABC_N_EQ_NO
Explanation: The networks are not equivalent.
Error Code: ABC_N_SAT_NO
Explanation: The formula is unsatisfiable.
Error Code: ABC_N_EQ_UND
Explanation: The equivalence of the networks could not be determined.
Error Code: ABC_N_SAT_UND
Explanation: The satisfiablility of the formula could not be determined.

File errors

Error Code: ABC_E_READ
Explanation: Error reading %s: %s.
Error Code: ABC_E_EXEC
Explanation: Error executing %s.
Error Code: ABC_E_SUFF
Explanation: Unknown file suffix %s.
Error Code: ABC_E_OPEN
Explanation: Error opening file %s.
Error Code: ABC_E_EXF
Explanation: %s does not exist or is not executable.
Error Code: ABC_E_EXD
Explanation: %s does not exist or is not a directory.

ABC errors

Error Code: ABC_E_PARAMS
Explanation: Incorrect parameters.
Error Code: ABC_E_CMD
Explanation: ABC command error: %s.
Error Code: ABC_E_EMPTY
Explanation: An empty network detected by ABC.
Error Code: ABC_E_PARSE
Explanation: The output could not be parsed.
Error Code: ABC_E_INCOMP
Explanation: Compared networks differ in inputs and/or outputs.
Error Code: ABC_E_TOUT
Explanation: ABC command timeout.
Error Code: ABC_E_EOF
Explanation: Unexpected end-of-file from ABC.
Error Code: ABC_E_BUSY
Explanation: Another ABC command in progress.


abc::init

Name

abc::init — Run and initialize ABC, start communication

Synopsis

abc::init [result] [timeout]

DESCRIPTION

The procedure looks in the directory given by the variable abc::dir for executable file named by variable abc::exe. Spawns that program using Expect with the option -s, which prevets ABC from sourcing initialization files. Then the procedures uses the ABC command source to read all the named initializaton files. Their locations and order is defined by a list in the abc::initList variable. Errors caused by nonexistent files are ignored. Failures to parse the file are detected and cause immediate error return. For a more detailed description and for standard file sequences, see abctcl.conf.tcl(5)

The variables abc::dir, abc::exe. and abc::initList are set by commands in the abctcl.conf.tcl file (see abctcl.conf.tcl(5) ) but can be overriden before the first invocation of abc::init.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

string abcVersion (out)

The first line returned by ABC, including version and date of compilation.

int spawn_id (out)

Process id as returned by the Expect spawn command.

list of strings sourced (out)

List of files that were sucessfully sourced into ABC.

list of strings failed (out)

List of files that failed to source into ABC.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_DIR
Diagnostic: The path named by abc::dir does not exist or is not a directory.
Error Code: ABC_E_EXF
Diagnostic: The file named by abc::exe does not exist or is not executable.
Error Code: ABC_E_EXEC
Diagnostic: The program failed to spawn.
Error Code: ABC_E_CMD
Diagnostic: Some of the initialization files could not be parsed.

EXAMPLE

This sequence initializes ABC with error reporting and recovery. script:

if { [catch { abc::init res }] } {
    puts $errorCode
    puts ".failed"
    foreach initFile $res(sourced) {
        puts $initFile
    }
    exit
} else {
    foreach initFile $res(sourced) {
        puts -nonewline "$initFile ... "
    }
    puts ".ok"
    puts "greeting:"
    puts $res(abcVersion)
    puts "final prompt number: $res(promptNumber)"
    puts "raw output follows:"
    puts $res(rawOutput)
}

SEE ALSO

abctcl.conf.tcl(5) , abctcl(n) , abc::messages(n) , abc::dome(n)


abc::done

Name

abc::done — terminate ABC

Synopsis

abc::done

DESCRIPTION

abc::done sends a quit command to ABC and then closes the connection. It has no arguments and returns empty string.

BUGS

  • There is no provision to terminate an ABC command that timed out.

SEE ALSO

abctcl(n)


abc::command

Name

abc::command — run an arbitrary ABC command

Synopsis

abc::command command [result] [timeout]

DESCRIPTION

Sends command to ABC and waits for a prompt. No processing is done on the output obtained from ABC.

ARGUMENTS

string command (in)

The ABC command including eventual parameters. Passed to ABC without change.

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.

SEE ALSO

abctcl.conf.tcl(5) , abctcl(n) , abc::messages(n)


abc::time

Name

abc::time — measure time elapsed by ABC

Synopsis

abc::print_unate [result] [parameters] [timeout]

DESCRIPTION

Sends the command time parameters to ABC and waits for a prompt. Parses the output and converts values reported by ABC to items in the result array.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

float elapse (out)

Time elapsed by the time command itself as reported by the ABC process.

float total(out)

Time elapsed by ABC as reported by the ABC process.

string parameters (in)

Optional argument. Parameters for the respective ABC commands. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: abc::print_unate could not parse the output of ABC. A new version with different labels might be in use.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::read

Name

abc::read — read a circuit description into ABC

Synopsis

abc::read [result] [parameters] [timeout]

DESCRIPTION

Sends the command read parameters to ABC and waits for a prompt. Parses the output to detect errors reported by ABC.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

string parameters (in)

Optional argument. Parameters for the ABC read command. Defaults to an empty string. This argument, although syntactically optional, is necessary, because it has to define the name of the file to read.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_OPEN
Diagnostic: The file specified in parameters could not be opened.
Error Code: ABC_E_SUFFIX
Diagnostic: The kind of circuit description could not be determined from the file name specified in parameters
Error Code: ABC_E_READ
Diagnostic: ABC could not input the circuit description in the specified file.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::source

Name

abc::source — source a script into ABC

Synopsis

abc::init file [result] [timeout]

DESCRIPTION

Sends the source file to ABC and waits for prompt. Parses the output to detect errors in opening the file and parse errors.

ARGUMENTS

string file (in)

The name of the sourced file.

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_READ
Diagnostic: Error reading file. The reason reported by ABC is also included
Error Code: ABC_E_CMD
Diagnostic: ABC could not parse commands in file.

SEE ALSO

abctcl.conf.tcl(5) , abctcl(n) , abc::messages(n)


abc::print_auto

Name

abc::print_auto — report circuit autosymmetries

Synopsis

abc::print_auto [result] [parameters] [timeout]

DESCRIPTION

Sends the command print_auto parameters to ABC and waits for a prompt. Parses the output and converts values reported by ABC to items in the result array.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int ins (out)

TO BE DETERMINED.

int inMax (out)

TO BE DETERMINED.

int outs (out)

TO BE DETERMINED.

int auto (out)

TO BE DETERMINED.

int sumK (out)

TO BE DETERMINED.

int kMax (out)

TO BE DETERMINED.

int supp (out)

TO BE DETERMINED.

float time (out)

TO BE DETERMINED.

string parameters (in)

Optional argument. Parameters for the ABC print_auto command. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.

BUGS

  • The Output-Input-AutoK table is not parsed.

  • The message `This command works only for AIGs (run "strash").' is not parsed.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::print_fanio

Name

abc::print_fanio — report signal branching and gate input counts in the circuit

Synopsis

abc::print_fanio [result] [parameters] [timeout]

DESCRIPTION

Sends the command print_fanio parameters to ABC and waits for a prompt. Parses the output and converts values reported by ABC to items in the result array. The parsing works with ABC 90813 version only. The fanin and fanout distribution table is not parsed.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int fanins_max (out)

Maximum number of inputs to a single gate.

int fanins_ave (out)

Average number of inputs to a single gate.

int fanouts_max (out)

Maximum number of inputs fed by the output of a single element.

int fanouts_max (out)

Average number of inputs fed by the output of a single element.

string parameters (in)

Optional argument. Parameters for the ABC print_fanio command. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: abc::print_fanio could not parse the output of ABC. A new version with different labels might be in use.
Error Code: ABC_E_EMPTY
Diagnostic: The current circuit description in ABC is empty. Use abc::read.

BUGS

  • ABC 70930 does not provide the summary information and therefore the procedure fails with ABC_E_PARSE.

  • The fanin and fanout distribution table printed by ABC is not parsed.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::print_gates

Name

abc::print_gates — report staistics of gate types

Synopsis

abc::print_gates [result] [parameters] [timeout]

DESCRIPTION

Sends the command print_gates parameters to ABC and waits for a prompt. Parses the output and converts values reported by ABC to items in the result array.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int const, float const_percent (out)

Number and percentage of constant generators (logical 0, 1).

int buffer, float buffer_percent (out)

Number and percentage of buffers.

int inverter, float inverter_percent (out)

Number and percentage of inverters.

int and, float and_percent (out)

Number and percentage of AND gates, including gates derived from AND by inversion of inputs, e.g. NOR.

int or, float or_percent (out)

Number and percentage of OR gates, including gates derived from OR by inversion of inputs, e.g. NAND.

int other, float other_percent (out)

Number and percentage of other gates, i. e. XOR and XNOR.

int total, float total_percent (out)

Number and percentage of all gates. The percentage is always 100%.

string parameters (in)

Optional argument. Parameters for the ABC print_gates command. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: abc::print_gates could not parse the output of ABC. A new version with different labels might be in use.
Error Code: ABC_E_EMPTY
Diagnostic: The current circuit description in ABC is empty. Use abc::read.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::print_latch

Name

abc::print_latch — report statistics of latches in the circuit

Synopsis

abc::print_latch [result] [parameters] [timeout]

DESCRIPTION

Sends the command print_fanio parameters to ABC and waits for a prompt. Parses the output and converts values reported by ABC to items in the result array. The parsing covers both ABC 70930 and 90813 versions (the latter has less cryptic category labels). When ABC reports the circuit as combinational, latch counts in all categories are set to 0.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int total_latches (out)

Total number of latches (flip-flops) in the circuit.

int init0 (out)

Number of latches initialized to logical 0.

int init1 (out)

Number of latches initialized to logical 1.

int initDC (out)

Number of uninitialized latches.

int const_data (out)

Number of latches with constant input.

string parameters (in)

Optional argument. Parameters for the ABC print_latch command. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: abc::print_latch could not parse the output of ABC. A new version with different labels might be in use.
Error Code: ABC_E_EMPTY
Diagnostic: The current circuit description in ABC is empty. Use abc::read.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::print_stats

Name

abc::print_stats — report general circuit statistics

Synopsis

abc::print_stats [result] [parameters] [timeout]

DESCRIPTION

Sends the command print_stats parameters to ABC and waits for a prompt. Parses the output and converts values reported by ABC to items in the result array.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int i (out)

TO BE DETERMINED

int o (out)

TO BE DETERMINED

int a (out)

TO BE DETERMINED

int lat (out)

TO BE DETERMINED

int lev (out)

TO BE DETERMINED

int edge (out)

TO BE DETERMINED

int net (out)

TO BE DETERMINED

int nd (out)

TO BE DETERMINED

int wbox (out)

TO BE DETERMINED

int bbox (out)

TO BE DETERMINED

int choice (out)

TO BE DETERMINED

int exor (out)

TO BE DETERMINED

int mux (out)

TO BE DETERMINED

int pure_and (out)

TO BE DETERMINED

int and (out)

TO BE DETERMINED

int cube (out)

TO BE DETERMINED

int aig (out)

TO BE DETERMINED

int lit_fac (out)

TO BE DETERMINED

double area (out)

TO BE DETERMINED

double delay (out)

TO BE DETERMINED

double power (out)

TO BE DETERMINED

double glitch (out)

TO BE DETERMINED

string parameters (in)

Optional argument. Parameters for the ABC print_stats command. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: abc::print_stats could not parse the output of ABC. A new version with different labels might be in use.
Error Code: ABC_E_EMPTY
Diagnostic: The current circuit description in ABC is empty. Use abc::read.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::print_symm

Name

abc::print_symm — report autosymmetries in the circuit

Synopsis

abc::print_symm [result] [parameters] [timeout]

DESCRIPTION

Sends the command print_symm parameters to ABC and waits for a prompt. Parses the output and converts values reported by ABC to items in the result array.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int total_func_supps (out)

TO BE DETERMINED.

int total_struct_supps (out)

TO BE DETERMINED.

int total_symm (out)

TO BE DETERMINED.

int structural_symm (out)

TO BE DETERMINED.

int total_non_sym (out)

TO BE DETERMINED.

int total_var_pairs (out)

TO BE DETERMINED.

string parameters (in)

Optional argument. Parameters for the ABC print_symm command. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: abc::print_symm could not parse the output of ABC. A new version with different labels might be in use.
Error Code: ABC_E_EMPTY
Diagnostic: The current circuit description in ABC is empty. Use abc::read.

BUGS

  • The message `This command works only for combinational networks (run "comb").' is not detected.

  • The ABC output has two parts - on supports and on symmetries. Some entries in the parts have equal names and are not parsed. In this case, blind regexp does not suffice.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::print_unate

Name

abc::print_unate — report unate functions in the circuit

Synopsis

abc::print_unate [result] [parameters] [timeout]

DESCRIPTION

Sends the command print_unate parameters to ABC and waits for a prompt. Parses the output and converts values reported by ABC to items in the result array.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

int shared_BDD_size (out)

TO BE DETERMINED.

int ins (out)

TO BE DETERMINED.

int outs (out)

TO BE DETERMINED.

float glob_BDDs (out)

TO BE DETERMINED.

int total_supp (out)

TO BE DETERMINED.

int total_unate (out)

TO BE DETERMINED.

float unateness (out)

TO BE DETERMINED.

float total (out)

TO BE DETERMINED.

string parameters (in)

Optional argument. Parameters for the ABC print_symm command. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedure returns an empty string. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: abc::print_unate could not parse the output of ABC. A new version with different labels might be in use.
Error Code: ABC_E_EMPTY
Diagnostic: The current circuit description in ABC is empty. Use abc::read.

BUGS

  • The message `This command works only for AIGs (run "strash").' is not detected.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::sec

Name

abc::sec, abc::cec, abc::dsec, abc::dprove — check circuits equivalence

Synopsis

abc::sec [result] [parameters] [timeout]

abc::cec [result] [parameters] [timeout]

abc::dsec [result] [parameters] [timeout]

abc::dprove [result] [parameters] [timeout]

DESCRIPTION

The procedures check whether two circuits are equivalent. They send respective commands together with parameters to ABC and wait for a prompt. The output is parsed to determine the result and detect error messages from ABC. The result is returned by symbolic return codes.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

string answer (out)

The result of the equivalence check. Also provided as the return value of the procedures. One of ABC_N_EQ_YES, ABC_N_EQ_NO, ABC_N_EQ_UND.

string parameters (in)

Optional argument. Parameters for the respective ABC commands. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedures returns a string representing the result, or an empty string in case of error. The returned symbol is one of

Symbol: ABC_N_EQ_YES
Meaning: The circuits are equivalent.
Symbol: ABC_N_EQ_NO
Meaning: The circuits are not equivalent.
Symbol: ABC_N_EQ_UND
Meaning: The equivalence of the circuits could not be established.

If the circuits have different inputs and outputs, ABC_E_INCOMP error occurs and ABC_N_EQ_UND is not reported. See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: The procedure could not parse the output of ABC. A new version with different labels might be in use.
Error Code: ABC_E_EMPTY
Diagnostic: The current circuit description in ABC is empty. Use abc::read.
Error Code: ABC_E_INCOMP
Diagnostic: The circuits have different inputs and/or outputs.

SEE ALSO

abctcl(n) , abc::messages(n)


abc::sat

Name

abc::sat, abc::iprove, abc::prove — check staisfiability

Synopsis

abc::sat [result] [parameters] [timeout]

abc::iprove [result] [parameters] [timeout]

abc::prove [result] [parameters] [timeout]

DESCRIPTION

The procedures take a combinational circuit and determines whether there exist a combination of input values that results in logical 1 at the output. This is known as the Boolean Satisfiability Problem (SAT). The procedures send respective commands together with parameters to ABC and wait for a prompt. The output is parsed to determine the result and detect error messages from ABC. The result is returned by symbolic return codes.

ARGUMENTS

array result (out)

Optional argument. If omitted, no information is returned. The following items are present:

string errorCode (out)

Error code. See RETURN CODES below. Also put to the errorCode global variable.

string rawOutput (out)

The unprocessed output of ABC, including the final prompt.

int promptNumber (out)

The number included in the final prompt. The ABC prompt has the "abc123> " form. The number indicates successive version of the network stored in ABC.

int cmdTime (out)

Time in milliseconds elapsed by the command.

string answer (out)

The result of the equivalence check. Also provided as the return value of the procedures. One of ABC_N_SAT_YES, ABC_N_SAT_NO, ABC_N_SAT_UND.

string parameters (in)

Optional argument. Parameters for the respective ABC commands. Defaults to an empty string.

int timeout (in)

Optional argument. If given, sets the timeout of Expect for this command. Othervise, the value of the timeout global variable applies.

RETURN CODES

The procedures returns a string representing the result, or an empty string in case of error. The returned symbol is one of

Symbol: ABC_N_SAT_YES
Meaning: This instance of the SAT problem is satisfiable.
Symbol: ABC_N_SAT_NO
Meaning: This instance of the SAT problem is unsatisfiable.
Symbol: ABC_N_SAT_UND
Meaning: The satisfiability of this instance could not be established.

See abctcl(n) , abc::messages(n) for error reporting and error symbols. The following error symbols can occur:

Error Code: ABC_E_BUSY
Diagnostic: Prompt from the previous command has not been detected yet.
Error Code: ABC_E_EOF
Diagnostic: A premature end-of-file detected. Perhaps the ABC process crashed.
Error Code: ABC_E_TOUT
Diagnostic: Timeout expired before the prompt was detected.
Error Code: ABC_E_PARAMS
Diagnostic: ABC could not interpret parameters.
Error Code: ABC_E_PARSE
Diagnostic: The procedure could not parse the output of ABC. A new version with different labels might be in use.
Error Code: ABC_E_EMPTY
Diagnostic: The current circuit description in ABC is empty. Use abc::read.

BUGS

  • The message `abc: src/base/abci/abcSat.c:58: Abc_NtkMiterSat: Assertion `Abc_NtkLatchNum(pNtk) == 0' failed. Aborted' (which means that the circuit contains latches) is not detected.

SEE ALSO

abctcl(n) , abc::messages(n)


Command-line utilities


abctclstub

Name

abctclstub — a script stub generator for ABCTcl

Synopsis

abctclstub script-file

DESCRIPTION

A script that generates empty ABCTcl scripts for Unix systems. The generated stub contains proper call to tclsh determined during installation and proper argument to Tcl source command for incorporation of ABCTcl.

SEE ALSO

abctcl.conf.tcl(5) , abctcl(n)


compare_resyn

Name

compare_resyn — a demonstration script for ABCTcl

Synopsis

compare_resyn circuit-file

tclsh compare_resyn.tcl circuit-file

DESCRIPTION

A simple ABCTcl script. It compares several resynthesis procedures using ABC. For each resynthesis, ABC reads circuit-file, performs resynthesis, and then reports results to the script. They are compared and a summary produced.

FILES

compare_resyn is a wrapper that sources compare_resyn.tcl. As compare_resyn.tcl uses the ABCTcl procedure collection, it also indirectly uses the abctcl.conf.tcl file.

SEE ALSO

abc::message(n) , abctcl.conf.tcl(5) , abctcl(n)


Graphical user interface


abctclgui

Name

abctclgui — a graphical front end for ABCTcl

Synopsis

abctclgui

wish abctclgui.tcl

DESCRIPTION

abctclgui facilitates controlling ABC. The output of multiple ABC commands can be viewed simultaneously. Commands can be assembled interactively. The application uses the following windows:

Main window.

Controls which windows will be displayed. Records ABC status (initializing, busy, ready...). Also has controls for reading and writing circuit descriptions to and from ABC. Closing this window causes the application to exit.

Command window.

Serves for interactive command assembly. Contain a list of ABC commands, translates them to Tcl calls of ABCTcl and collects arguments to the command. Instead of ABCTcl calls, an arbitrary Tcl/Tk command can be entered. Selects an output window where the output of ABC will be displayed.

Output window.

Displays the result of a command, usually an ABCTcl call. The output can be filtered to hide null values or the raw output of ABC. The last command issued is stored, displayed and can be rerun.

Console window.

Standard input, output and error output of the application. On Unix systems, the terminal window where abctclgui has been called serves this purpose. On Windows, there is a special text window similar to the command line console.

FILES

The appearance of the application, i. e. the presence and size of its windows is stored in a configuration file named abctclgui.conf.tcl. On exit, the application asks the user whether this file shall be stored in the current directory. On startup, the following locations are searched, until the file is found:

  • Current directory.

  • If the environment variable HOME is set to a non-empty value, the directory named by it (the user's home directory).

  • The directory where abctclgui.tcl has been installed.

As abctclgui uses the ABCTcl procedure collection, it also indirectly uses abctcl.conf.tcl file.

BUGS

  • (Usability problem) The buttons Load file and Save file in the main window belong to the command window.

  • (Usability problem) The buttons Load file and Save file in the main window shall be labeled in ABC parlance, i.e. Read file and Write file.

  • (Usability problem) Details of the generated Tcl command in the command window are irrelevant for the user. The text field shall not permit to modify the result variable. On the other hand, no field for parameters is provided.

  • (Usability problem) No means to obtain help for the selected command is provided, although ABC has a unified mechanism for that.

  • (Usability problem) No means for timeout setting is provided.

  • (Usability problem) Error information returned from an ABCTcl command is displayed only as an item in the result array. Shall be displayed separately.

  • (Consistency problem) On Unix systems, it is customary to hide configuration files by prepending a dot to the name. abctclgui does not do so.

  • (Functionality problem) When saving the configuration file, a file chooser dialog would be expected. Also, Load configuratiuon and Save configuration with file choosers would permit multiple stored configurations.

SEE ALSO

abc::command(n) , abctcl.conf.tcl(5) , abctcl(n)