• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
        • Svtv-data
        • Defsvtv$
        • Svtv-run
        • Defsvtv-phasewise
        • Svtv
        • Svtv-spec
        • Defsvtv
        • Process.lisp
          • Svtv-compile
          • Defsvtv-events
          • Svtv-compile-lazy
          • Svtv-compile-phase
          • Svtv-compile-phases-lazy
          • Svtv-allphases-inputs
          • Svtv-phase-inputs
          • Svtv-inalist-resolve-unassigned
          • Svtv-simplify-outs/states
          • Svtv-collect-inmap
          • Svar-boolmasks-limit-to-bound-vars
          • Svtv-overrides->assigns
          • Svtv-non-override-test-input-vars
          • Svtv-outputs->outalist
          • Svtv-run-squash-dontcares
          • Svtv-inputs->assigns
          • Svtv-phase-var-assigns
          • Defsvtv-fn
          • Svtv-entries->overrideconds
          • Svtv-entries->vars
          • Svtv-easy-bindings-main
          • Svtv-collect-masks
          • Svtv-baseentry-svex
          • Svtv-init-states
          • Lhs->mask
          • Svtv-easy-bindings-svtv-vars
          • Svtv-autoins-aux
          • Svtv-autohyps-aux
          • Svtv-autobinds-aux
          • Svtv-autoins
          • Svtv-autohyps
          • Svtv-autobinds
          • Fast-alist-free-list
          • Defsvtv-default-names
        • Svtv-doc
        • Svtv-chase$
        • Svtv-versus-stv
        • Svtv-debug-fsm
        • Structure.lisp
        • Svtv-debug
        • Def-pipeline-thm
        • Expand.lisp
        • Def-cycle-thm
        • Svtv-utilities
        • Svtv-debug$
        • Defsvtv$-phasewise
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Process.lisp

Svtv-simplify-outs/states

Signature

(svtv-simplify-outs/states outs nextstates simplify) 
  → 
(mv simp-outs simp-states)

Arguments

outs — Guard (svex-alist-p outs).

nextstates — Guard (svex-alist-p nextstates).

Returns

simp-outs — Type (svex-alist-p simp-outs).

simp-states — Type (svex-alist-p simp-states).

Definitions and Theorems

Function: svtv-simplify-outs/states

(defun svtv-simplify-outs/states (outs nextstates simplify)
  (declare (xargs :guard (and (svex-alist-p outs)
                              (svex-alist-p nextstates))))
  (let ((__function__ 'svtv-simplify-outs/states))
    (declare (ignorable __function__))
    (b* ((outs (svex-alist-fix outs))
         (nextstates (svex-alist-fix nextstates))
         ((unless simplify) (mv outs nextstates))
         (alist (append outs nextstates))
         (simp-alist (svex-alist-normalize-concats
                          (svex-alist-rewrite-fixpoint alist
                                                       :verbosep t)
                          :verbosep t))
         (outs-len (len outs))
         (simp-outs (take outs-len simp-alist))
         (simp-states (nthcdr outs-len simp-alist)))
      (mv simp-outs simp-states))))

Theorem: svex-alist-p-of-svtv-simplify-outs/states.simp-outs

(defthm svex-alist-p-of-svtv-simplify-outs/states.simp-outs
  (b* (((mv ?simp-outs ?simp-states)
        (svtv-simplify-outs/states outs nextstates simplify)))
    (svex-alist-p simp-outs))
  :rule-classes :rewrite)

Theorem: svex-alist-p-of-svtv-simplify-outs/states.simp-states

(defthm svex-alist-p-of-svtv-simplify-outs/states.simp-states
  (b* (((mv ?simp-outs ?simp-states)
        (svtv-simplify-outs/states outs nextstates simplify)))
    (svex-alist-p simp-states))
  :rule-classes :rewrite)

Theorem: svtv-simplify-outs/states-of-svex-alist-fix-outs

(defthm svtv-simplify-outs/states-of-svex-alist-fix-outs
  (equal (svtv-simplify-outs/states (svex-alist-fix outs)
                                    nextstates simplify)
         (svtv-simplify-outs/states outs nextstates simplify)))

Theorem: svtv-simplify-outs/states-svex-alist-equiv-congruence-on-outs

(defthm
      svtv-simplify-outs/states-svex-alist-equiv-congruence-on-outs
 (implies
   (svex-alist-equiv outs outs-equiv)
   (equal
        (svtv-simplify-outs/states outs nextstates simplify)
        (svtv-simplify-outs/states outs-equiv nextstates simplify)))
 :rule-classes :congruence)

Theorem: svtv-simplify-outs/states-of-svex-alist-fix-nextstates

(defthm svtv-simplify-outs/states-of-svex-alist-fix-nextstates
  (equal (svtv-simplify-outs/states outs (svex-alist-fix nextstates)
                                    simplify)
         (svtv-simplify-outs/states outs nextstates simplify)))

Theorem: svtv-simplify-outs/states-svex-alist-equiv-congruence-on-nextstates

(defthm
 svtv-simplify-outs/states-svex-alist-equiv-congruence-on-nextstates
 (implies
   (svex-alist-equiv nextstates nextstates-equiv)
   (equal
        (svtv-simplify-outs/states outs nextstates simplify)
        (svtv-simplify-outs/states outs nextstates-equiv simplify)))
 :rule-classes :congruence)