• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Esim

Esim-simplify-update-fns

Pluggable conservative simplifier for ESIM fixpoint extraction

Esim-simplify-update-fns is a constrained function that is called in conservative versions of ESIM such as ESIM-SEXPR-SIMP. It is constrained to produce a conservative approximation of the update functions that it is passed. An executable function that obeys these constraints can be attached to it. Thus, it can be used to (say) replace the update functions with Xes, rewrite them into a nicer form, perform Shannon expansion on certain signals, etc. Esim-simplify-update-fns is also passed the module that is currently being examined, so that you may choose to only perform simplifcations on certain modules. By default, esim-simplify-update-fns has an attachment that simply preserves the existing update functions without modification.

Definitions and Theorems

Theorem: esim-simplify-update-fns-conservative

(defthm esim-simplify-update-fns-conservative
  (4v-sexpr-alist-<= (esim-simplify-update-fns mod update-fns)
                     update-fns))

Theorem: esim-simplify-update-fns-alist-keys-same

(defthm esim-simplify-update-fns-alist-keys-same
  (set-equiv (alist-keys (esim-simplify-update-fns mod update-fns))
             (alist-keys update-fns)))

Theorem: esim-simplify-update-fns-4v-sexpr-vars-subset

(defthm esim-simplify-update-fns-4v-sexpr-vars-subset
  (subsetp-equal
       (4v-sexpr-vars-list
            (alist-vals (esim-simplify-update-fns mod update-fns)))
       (append (4v-sexpr-vars-list (alist-vals update-fns))
               (alist-keys (mod-varmap mod)))))

Theorem: good-sexpr-varmap-esim-simplify-update-fns

(defthm good-sexpr-varmap-esim-simplify-update-fns
 (implies
     (good-sexpr-varmap (mod-varmap mod)
                        update-fns)
     (good-sexpr-varmap (mod-varmap mod)
                        (esim-simplify-update-fns mod update-fns))))