		Search-engine friendly clone of the ACL2 documentation.

Glmc

Bfr-mcheck

Attachable interface for glmc's model-checking backend

Bfr-mcheck is a constrained function that GLMC calls in order to solve hardware model-checking queries.

Bfr-mcheck operates on hons-AIGs (see aig) whose input variables are natural numbers. This is potentially important because it provides an easy way for a backend to generate new variables that are known to be unused. Some of the variables represent primary inputs and some represent states; the state variables are simply those that are bound in the next-state alist. Below, when we refer to a "single AIG", this means a single hons-AIG object, which represents a single-output Boolean function.

Inputs:

prop: Single AIG giving the invariant property to prove.
constr: Single AIG giving the invariant constraint to assume.
updates: Alist mapping each state variable to a single AIG representing its next-state function.
initstp: Single AIG assumed to be true of any initial state.
max-bvar: Natural number greater than all variables used in the AIGs.

Outputs:

result: one of the symbols :proved, :refuted, or :failed, indicating the status of the check.
ctrex-initst: when refuted, an alist mapping each state variable to its Boolean initial state in the counterexample.
ctrex-ins: when refuted, a list of alists representing the frames of the counterexample, each alist mapping each non-state variable to a Boolean value.

The constraint assumed of bfr-mcheck pertains to what is implied when it returns the result :proved:

(b* (((mv result ?ctrex-initst ?ctrex-ins) (bfr-mcheck prop constr updates initstp max-bvar)))
     (implies (and (equal result :proved)
                   (bfr-eval initstp (bfr-env-override (bfr-updates->states updates) init-st (car ins)))
                   (pbfr-vars-bounded max-bvar t prop)
                   (pbfr-vars-bounded max-bvar t constr)
                   (pbfr-vars-bounded max-bvar t initstp)
                   (pbfr-list-vars-bounded max-bvar t (alist-vals (bfr-updates-fix updates)))
                   ;; (subsetp (bfr-vars initstp) (bfr-updates->states updates))
                   (bfr-varlist-bounded max-bvar (bfr-updates->states updates)))
              (bfr-constrained-mcrun prop constr updates init-st ins)))

This basically says:

If bfr-mcheck returned :proved, then assuming that all the input AIGs use only variables below max-bvar and that the initial state of a finite run satisfies initstp, then the property holds at every frame of that run at which the constraint has not yet been violated.

See bfr-mcheck-abc-simple for an example backend that may be attached to bfr-mcheck.