ACL2 interface to AIG-based safety model checking

The GLMC package allows automated proving of safety properties of state machines defined in ACL2. It uses GL to obtain a representation for the next-state function, property, etc. as AIGs, and calls on an AIG model checker such as ABC to verify the property.

Here is a small example:

(include-book "glmc") (include-book "bfr-mcheck-abc") (include-book "centaur/gl/bfr-satlink" :dir :system) ;; use abc as the model checking engine (bfr-mcheck-use-abc-simple) ;; use satlink (glucose) as the SAT checker (gl-satlink-mode) ;; start the external shell interface (value-triple (acl2::tshell-start)) ;; Definition of a (very) simple machine: machine state is just a 4-bit natural ;; which can be reset to 0 or incremented, but when incremented to exactly 10 ;; resets to 0. This is the next-state function: (defun my-nextst (st incr reset) (b* (((when reset) 0) (st (lnfix st)) ((unless incr) st) (next (1+ st)) ((when (eql next 10)) 0)) next)) ;; We'll check that this machine never reaches a state equal to 14. This function ;; checks the property for any finite run, where st is the initial state and ins ;; is the list of input pairs (incr . reset): (defund my-run-prop (st ins) (declare (xargs :measure (len ins))) (if (atom ins) t (and (not (equal st 14)) (my-run-prop (my-nextst st (caar ins) (cdar ins)) (cdr ins))))) ;; Here we prove that if the initial value of the machine state is less than ;; 5, then our property holds: (defthm my-run-prop-correct (implies (and (natp st) (< st 5)) (my-run-prop st ins)) :hints ((glmc-hint :shape-spec-bindings `((incr ,(g-var 'incr)) (reset ,(g-var 'reset)) (st ,(g-int 0 1 5))) :state-var st :initstatep (< st 5) :nextstate (my-nextst st incr reset) :frame-input-bindings ((incr (caar ins)) (reset (cdar ins))) :rest-of-input-bindings ((ins (cdr ins))) :end-of-inputsp (atom ins) :measure (len ins) :run (my-run-prop st ins) :state-hyp (and (natp st) (< st 16)) :prop (not (equal st 14)) :run-check-hints ('(:expand ((my-run-prop st ins)))))))

The notable thing about this example is that the property, as stated, is not
inductive. The usual way to prove this in ACL2 would be to strengthen the
property into an invariant that is inductive -- either weaken the initial state
assumption so that it is inductive (assume

GLMC is invoked by the glmc-hint macro, which takes several keyword options:

:state-var is the variable containing the current machine state (as distinguished from the inputs).:body-bindings is a list of b* bindings under which to evaluate the:nextstate ,:initstatep :prop , and:constraint terms. It should only use the state variable and frame inputs.:initstatep is a term that must be true for valid initial states, though it may reference any variables bound in:body-bindings as well as the state and frame input variables.:nextstate is a term giving the next value of the state, in terms of the state variable, frame inputs, and variables bound by:body-bindings .:run is a term calling some function that recursively checks the property on some finite run, i.e. it checks the property of the current state and input frame, then recurs after updating the state with the nextstate function.:frame-input-bindings is a binding list (such as in alet ), giving the current-frame inputs in terms of the inputs to the run function. We'll refer to (e.g.) the list of all remaining frame inputs as the "run inputs", versus (e.g.) a single element of that list as the "frame inputs". E.g., if the input to the run function is simply a list of frame inputs, then this binding might be((in (car ins))) .:rest-of-input-bindings is a binding list giving the rest of the inputs after the current frame, such as is passed to the recursive call of the run function -- e.g.,((ins (cdr ins))) .:end-of-inputsp is a term saying when to stop the run; the run function should always be true when:end-of-inputsp holds, because that means it has failed to find a frame in which the property is violated. In the case of a simple list of frame inputs, this would be(atom ins) .:measure gives a measure for the run function; for technical reasons, we must reprove the termination of the run function.:shape-spec-bindings gives a binding of the state variable and frame input variables to shape specifier objects; see shape-specs. Unlike the other arguments, this one is evaluated, so if you don't want to evaluate it, quote it.:input-hyp gives an assumption about the frame inputs that must hold in each frame or else the run function will return true. (If you want to have a separate theorem hypothesis saying that the assumption holds for each input, you may include this in the:run term usingimplies .) This is used to prove that the shape-spec given for each non-state input is sufficient to cover all allowed inputs.:state-hyp gives an assumption that must hold of all valid states; it is used to prove that the shape-spec given for the state variable is sufficient to cover all possible states. The goal to be proved must assume the state-hyp holds of the initial state, and it will be proven to hold of all other states by model checking or inductively; see the:state-hyp-method option below.:state-hyp-method should be one of:inductive-sat ,:inductive-clause , or:mcheck (the default); this determines the method by which we show that the state hyp is invariant. If it is:inductive-clause , a proof obligation is generated saying that the state hyp holds of the next-state if the input hyp and state hyp hold of the current state. If it is:inductive-sat , a SAT check is issued which proves this at the Boolean level. If it is:mcheck , then the condition is ANDed with the property in the model checking problem. This is a more flexible method (though potentially slower) because the state hyp may be an invariant of all reachable states without being an inductive invariant.:prop gives the property that must be proven to hold in each frame (i.e., the run function returns false if it is ever violated). It may reference the state and frame input variables as well as variables bound in the:body-bindings .:constraint gives a constraint that is assumed to hold in each frame (i.e., the run function returns true if it is ever violated). (This may be omitted; its default isT .) It may reference the state and frame input variables as well as variables bound in the:body-bindings .:side-goals , if set toT , skips the actual model checking and simply returns the "side goals" such as coverage and the check that the run function and input clause are of the expected form. (A theorem with:side-goals t will always fail to prove, but if everything is successful only a single subgoal of the form(not (gl-cp-hint 'side-goals-fake-goal)) will remain.):check-vacuity isT by default; when true, GLMC will check that the state-hyp, input-hyp, initial state predicate, constraint, and property are each separately satisfiable, since any of these being unsatisfiable likely indicates something unexpected. Setting this toNIL skips these checks.:clause-check-hints ,:run-check-hints ,:measure-hints , and:state-hyp-inductive-hints provide computed hints to various side goals produced by the clause processor. Each entry should be a list of hints like the usual:hints provided to a defthm event, but all the hints should be computed hints, not subgoal hints. The side goals are discussed below.:do-not-expand ,:cov-theory-add ,:cov-hints , and:cov-hints-position affect the hints given to the coverage side goal; see coverage-problems. To provide your own hints, completely overriding the default hints provided for coverage, use:cov-hints to give your hints and set:cov-hints-position :replace .

A few proof obligations are produced by a successful call of the GLMC clause processor.

- Coverage: Shows that the shape specifiers provided in the
:shape-spec-bindings argument are sufficient to cover all possible states and inputs allowed by the state and input hyps. This goal has the same form as any GL coverage proof; see shape-specs and coverage-problems. - Clause check: This simply shows that the goal clause is of the required
form. Specifically, the original goal must follow from this conjecture, which
is what GLMC actually proves:
(implies (and <initstp> <st-hyp>) <run>)

- Run check: This checks that the
:run term is implied by the recurrence that is proved by the model check, namely:(if <end-of-inputs> t (let <frame-input-bindings> (let <rest-of-input-bindings> (if (not (and <input-hyp> (b* <body-bindings> <constraint>))) t (if (not (b* <body-bindings> <prop>)) nil (let ((<st-var> (b* <body-bindings> <nextstate>))) (if (not <state-hyp>) 'nil <run>)))))))

- Measure check: This rechecks that the run function terminates, which is necessary for technical reasons.
- State-hyp-inductive check: This only occurs if the
:state-hyp-method is:inductive-clause ; it shows that the state hyp is invariant.

GLMC uses the same method as GL to solve combinational SAT problems, such as
vacuity checks (see modes). GLMC calls its model-checking backend
through an attachable function called bfr-mcheck. The book
"glmc/bfr-mcheck-abc.lisp" provides one backend that can be attached to

- Bfr-mcheck
- Attachable interface for glmc's model-checking backend
- Bfr-mcheck-abc-simple
- Bfr-mcheck interface for ABC model-checking