abc::sec
Prev   Next

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)

Prev   Next
abc::print_unate Home abc::sat