• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
    • Gl
      • Term-level-reasoning
      • Glmc
        • Bfr-mcheck
        • Bfr-mcheck-abc-simple
      • Other-resources
      • Optimization
      • Reference
      • Debugging
      • Basic-tutorial
    • Witness-cp
    • Ccg
    • Install-not-normalized
    • Rewrite$
    • Removable-runes
    • Efficiency
    • Rewrite-bounds
    • Bash
    • Def-dag-measure
    • Fgl
    • Bdd
    • Remove-hyps
    • Contextual-rewriting
    • Simp
    • Rewrite$-hyps
    • Bash-term-to-dnf
    • Use-trivial-ancestors-check
    • Minimal-runes
    • Clause-processor-tools
    • Fn-is-body
    • Without-subsumption
    • Rewrite-equiv-hint
    • Def-bounds
    • Rewrite$-context
    • Try-gl-concls
    • Hint-utils
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Glmc

Bfr-mcheck-abc-simple

Bfr-mcheck interface for ABC model-checking

Signature

(bfr-mcheck-abc-simple prop constr updates initstp max-bvar) 
  → 
(mv result ctrex-initst ctrex-ins)

Arguments

updates — Guard (bfr-updates-p updates).

max-bvar — Guard (natp max-bvar).

Definitions and Theorems

Function: bfr-mcheck-abc-simple

(defun
 bfr-mcheck-abc-simple
 (prop constr updates initstp max-bvar)
 (declare (xargs :guard (and (bfr-updates-p updates)
                             (natp max-bvar))))
 (let
  ((__function__ 'bfr-mcheck-abc-simple))
  (declare (ignorable __function__))
  (b*
     (((unless (bfr-mode))
       (prog2$ (er hard? 'bfr-mcheck-abc
                   "ABC model checking not supported in BDD mode")
               (mv :failed nil nil)))
      ((mv prop1
           constr1 updates1 initst1 next-bvar)
       (bfrmc-set-initst-pred prop constr updates initstp max-bvar))
      ((mv prop2 updates2)
       (bfrmc-add-constraint prop1 constr1 updates1 next-bvar))
      (initst2 (bfr-set-var next-bvar nil initst1))
      ((mv status ctrex)
       (abc-mcheck-simple prop2 updates2 initst2))
      ((unless (and (eq status :refuted)
                    (consp ctrex)))
       (mv status nil nil))
      (first-ins (make-fast-alist (car ctrex)))
      (ctrex-initst1
           (bfr-ins-to-initst
                (acl2::hons-set-diff (bfr-updates->states updates)
                                     (bfr-updates->states initst1))
                (+ 1 (lnfix max-bvar))
                first-ins))
      (ctrex-initst2 (hons-shrink-alist initst2 ctrex-initst1)))
     (fast-alist-free first-ins)
     (mv :refuted ctrex-initst2 ctrex))))

Theorem: aig-fsm-run-prop-ok-when-abc-mcheck-simple-rw

(defthm
 aig-fsm-run-prop-ok-when-abc-mcheck-simple-rw
 (b*
  (((mv result ?ctrex)
    (abc-mcheck-simple prop updates init-st)))
  (implies (bind-free '((ins bfrmc-set-initst-pred-inputs
                             updates initstp max-bvar init-st ins)))
           (iff (equal result :proved)
                (and (bfr-mcrun prop updates init-st ins)
                     (hide (equal result :proved)))))))

Theorem: not-member-vars-when-pbfr-list-vars-bounded

(defthm not-member-vars-when-pbfr-list-vars-bounded
        (implies (and (pbfr-list-vars-bounded max-bvar t x)
                      (bfr-varname-p var)
                      (bfr-mode)
                      (or (not (natp var))
                          (<= (nfix max-bvar) var)))
                 (not (member var (bfrlist-vars x)))))

Theorem: bfr-mcheck-abc-simple-correct

(defthm
 bfr-mcheck-abc-simple-correct
 (b*
  (((mv result ?ctrex-initst ?ctrex-ins)
    (bfr-mcheck-abc-simple 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)))
     (bfr-varlist-bounded max-bvar (bfr-updates->states updates)))
   (bfr-constrained-mcrun prop constr updates init-st ins))))