abc::sat

abc::sat
Prev		Next

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.

Prev		Next
abc::sec	Home	abctclstub