		Search-engine friendly clone of the ACL2 documentation.

Aignet-abc-interface

Aignet-run-abc-core

Run abc on an aignet, without using state

Signature
(aignet-run-abc-core input-aignet output-aignet frames script &key script-filename input-filename output-filename ctrex-filename (force-status 'nil) (quiet 'nil)) → (mv status new-output-aignet new-frames)
Arguments: input-aignet — input AIG.; output-aignet — output AIG.; frames — output ctrex.; script — Commands for ABC to run, including reading the input aiger file and writing the output, if desired.
Guard (stringp script).; script-filename — Guard (stringp script-filename).; input-filename — Guard (stringp input-filename).; output-filename — If set, implies that the script writes a new aignet to this file.
Guard (acl2::maybe-stringp output-filename).; ctrex-filename — If set, implies that the script may dump a counterexample in this file.
Guard (acl2::maybe-stringp ctrex-filename).; force-status — If set to true, causes an error if no proof status line is present in the output.; quiet — Don't print the output from ABC.
Returns: status — Either :refuted, :proved, :failed, NIL, or an error message. NIL implies that there was no error detected but also no proof status line, implying that maybe no proof was attempted.

This function dumps the input aignet into a specified aiger file given as :input-filename, writes the given script into script-filename, then runs abc with that script. If the output-filename option is given, then when abc finishes it attempts to read a new aignet from that file, which overwrites output-aignet. If the ctrex-filename option is given and ABC outputs a status line indicating that it has a counterexample, then this function reads the counterexample from that file, which overwrites frames.

This function does not make any modifications to the given ABC script and does not attempt to ensure that it makes sense. For example, if ctrex-filename is given, then the script should likely contain:

print_status
write_ctrex ctrex-filename

If output-filename is given, then the script should contain a command that writes out the final network to that file, such as:

&w output-filename

This function is not axiomatized in any way, because it could be used for at least four different applications, which would make sense to axiomatize differently:

combinational simplification
combinational (equivalence, satisfiability) checking
sequential simplification
sequential (equivalence, model) checking.

See abc-example-scripts for some scripts that do these things.

Definitions and Theorems

Function: aignet-run-abc-core-fn

(defun aignet-run-abc-core-fn
       (input-aignet output-aignet
                     frames script script-filename
                     input-filename output-filename
                     ctrex-filename force-status quiet)
 (declare (xargs :stobjs (input-aignet output-aignet frames)))
 (declare (xargs :guard (and (stringp script)
                             (stringp script-filename)
                             (stringp input-filename)
                             (acl2::maybe-stringp output-filename)
                             (acl2::maybe-stringp ctrex-filename))))
 (let ((__function__ 'aignet-run-abc-core))
  (declare (ignorable __function__))
  (with-local-state
   (mv-let
    (status output-aignet frames state)
    (aignet-run-abc-core-st input-aignet output-aignet frames script
                            :script-filename script-filename
                            :input-filename input-filename
                            :output-filename output-filename
                            :ctrex-filename ctrex-filename
                            :force-status force-status
                            :quiet quiet)
    (mv status output-aignet frames)))))

Theorem: frames-ncols-of-aignet-run-abc-core-logic-when-refuted

(defthm frames-ncols-of-aignet-run-abc-core-logic-when-refuted
  (b* (((mv ?status ?new-output-aignet ?new-frames)
        (aignet-run-abc-core-fn input-aignet output-aignet
                                frames script script-filename
                                input-filename output-filename
                                ctrex-filename force-status quiet)))
    (implies (and (equal status :refuted)
                  ctrex-filename)
             (equal (stobjs::2darr->ncols new-frames)
                    (num-ins input-aignet)))))