• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
        • Rewriting
        • Svex
          • Svar
          • Least-fixpoint
            • Flatnorm->ideal-fsm
          • Svex-p
          • Svex-select
          • Svex-alist
          • Svex-equiv
          • Svexlist
          • Svex-call
          • Fnsym
          • Svex-quote
          • Svex-var
          • Svcall-rw
          • Svcall
          • Svex-kind
          • Svcall*
          • Svex-fix
          • Svex-count
          • Svex-1z
          • Svex-1x
          • Svex-z
          • Svex-x
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Least-fixpoint

Flatnorm->ideal-fsm

Returns the fixpoint FSM derived from the assignment network and state updates (delays) given by the input.

Signature

(flatnorm->ideal-fsm x) → fsm

Arguments

x — Guard (flatnorm-res-p x).

Returns

fsm — Type (fsm-p fsm).

Definitions and Theorems

Function: flatnorm->ideal-fsm

(defun flatnorm->ideal-fsm (x)
 (declare (xargs :guard (flatnorm-res-p x)))
 (declare
  (xargs
   :guard
   (and
    (svex-alist-width (flatnorm-res->assigns x))
    (not (hons-dups-p (svex-alist-keys (flatnorm-res->assigns x)))))
   :non-executable t))
 (prog2$
  (acl2::throw-nonexec-error 'flatnorm->ideal-fsm
                             (list x))
  (let ((__function__ 'flatnorm->ideal-fsm))
    (declare (ignorable __function__))
    (b* (((flatnorm-res x))
         (values (svex-alist-least-fixpoint x.assigns)))
      (make-fsm :values values
                :nextstate (svex-alist-compose x.delays values))))))

Theorem: fsm-p-of-flatnorm->ideal-fsm

(defthm fsm-p-of-flatnorm->ideal-fsm
  (b* ((fsm (flatnorm->ideal-fsm x)))
    (fsm-p fsm))
  :rule-classes :rewrite)

Theorem: flatnorm->ideal-fsm-with-overrides-override-transparent

(defthm flatnorm->ideal-fsm-with-overrides-override-transparent
 (b* (((flatnorm-res x))
      (override-flatnorm (flatnorm-add-overrides x overridekeys))
      (override-fsm (flatnorm->ideal-fsm override-flatnorm)))
  (implies
      (and (no-duplicatesp-equal (svex-alist-keys x.assigns))
           (no-duplicatesp-equal (svarlist-fix overridekeys))
           (svex-alist-width x.assigns)
           (svarlist-override-p overridekeys nil)
           (svex-alist-monotonic-on-vars (svex-alist-keys x.assigns)
                                         x.assigns)
           (subsetp-equal (svarlist-fix overridekeys)
                          (svex-alist-keys x.assigns))
           (svarlist-override-p (svex-alist-keys x.assigns)
                                nil)
           (svarlist-override-p (svex-alist-vars x.assigns)
                                nil)
           (svarlist-override-p (svex-alist-vars x.delays)
                                nil))
      (fsm-overridekey-transparent-p override-fsm overridekeys))))

Theorem: flatnorm->ideal-fsm-overrides->>=-phase-fsm-composition-values

(defthm
     flatnorm->ideal-fsm-overrides->>=-phase-fsm-composition-values
 (b*
  (((flatnorm-res x))
   (override-keys (svtv-assigns-override-vars
                       x.assigns
                       (phase-fsm-config->override-config config)))
   (override-flatnorm (flatnorm-add-overrides x override-keys))
   ((fsm ideal-fsm)
    (flatnorm->ideal-fsm override-flatnorm))
   ((fsm approx-fsm)))
  (implies
      (and (phase-fsm-composition-p approx-fsm x config)
           (svex-alist-monotonic-on-vars (svex-alist-keys x.assigns)
                                         x.assigns)
           (svex-alist-width x.assigns)
           (no-duplicatesp-equal (svex-alist-keys x.assigns))
           (svarlist-override-p (svex-alist-vars x.assigns)
                                nil)
           (svarlist-override-p (svex-alist-keys x.assigns)
                                nil))
      (svex-alist-<<= approx-fsm.values ideal-fsm.values))))

Theorem: flatnorm->ideal-fsm-overrides->>=-phase-fsm-composition-nextstate

(defthm
  flatnorm->ideal-fsm-overrides->>=-phase-fsm-composition-nextstate
 (b*
   (((flatnorm-res x))
    (overridekeys (svtv-assigns-override-vars
                       x.assigns
                       (phase-fsm-config->override-config config)))
    (override-flatnorm (flatnorm-add-overrides x overridekeys))
    ((fsm ideal-fsm)
     (flatnorm->ideal-fsm override-flatnorm))
    ((fsm approx-fsm)))
  (implies
      (and (phase-fsm-composition-p approx-fsm x config)
           (svex-alist-monotonic-on-vars (svex-alist-keys x.assigns)
                                         x.assigns)
           (svex-alist-monotonic-on-vars (svex-alist-keys x.assigns)
                                         x.delays)
           (svex-alist-width x.assigns)
           (no-duplicatesp-equal (svex-alist-keys x.assigns))
           (svarlist-override-p (svex-alist-vars x.assigns)
                                nil)
           (svarlist-override-p (svex-alist-keys x.assigns)
                                nil)
           (svarlist-override-p (svex-alist-vars x.delays)
                                nil))
      (svex-alist-<<= approx-fsm.nextstate
                      ideal-fsm.nextstate))))

Theorem: flatnorm->ideal-fsm-overrides->>=-phase-fsm-composition

(defthm flatnorm->ideal-fsm-overrides->>=-phase-fsm-composition
 (b*
   (((flatnorm-res x))
    (overridekeys (svtv-assigns-override-vars
                       x.assigns
                       (phase-fsm-config->override-config config)))
    (override-flatnorm (flatnorm-add-overrides x overridekeys))
    (ideal-fsm (flatnorm->ideal-fsm override-flatnorm)))
  (implies
      (and (phase-fsm-composition-p approx-fsm x config)
           (svex-alist-monotonic-on-vars (svex-alist-keys x.assigns)
                                         x.assigns)
           (svex-alist-monotonic-on-vars (svex-alist-keys x.assigns)
                                         x.delays)
           (svex-alist-width x.assigns)
           (no-duplicatesp-equal (svex-alist-keys x.assigns))
           (svarlist-override-p (svex-alist-vars x.assigns)
                                nil)
           (svarlist-override-p (svex-alist-keys x.assigns)
                                nil)
           (svarlist-override-p (svex-alist-vars x.delays)
                                nil))
      (fsm-<<= approx-fsm ideal-fsm))))

Theorem: svar-override-triplelist->testvars-of-svarlist-to-override-triples

(defthm
 svar-override-triplelist->testvars-of-svarlist-to-override-triples
 (equal (svar-override-triplelist->testvars
             (svarlist-to-override-triples keys))
        (svarlist-change-override keys :test)))

Theorem: phase-fsm-composition-ovmonotonic-values

(defthm phase-fsm-composition-ovmonotonic-values
  (b* (((flatnorm-res x)) ((fsm approx-fsm)))
    (implies (and (phase-fsm-composition-p approx-fsm x config)
                  (svex-alist-monotonic-p x.assigns)
                  (svarlist-override-p (svex-alist-vars x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.assigns)
                                       nil))
             (svex-alist-ovmonotonic approx-fsm.values))))

Theorem: phase-fsm-composition-ovcongruent-values

(defthm phase-fsm-composition-ovcongruent-values
  (b* (((flatnorm-res x)) ((fsm approx-fsm)))
    (implies (and (phase-fsm-composition-p approx-fsm x config)
                  (svarlist-override-p (svex-alist-vars x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.assigns)
                                       nil))
             (svex-alist-ovcongruent approx-fsm.values))))

Theorem: svex-alist-ovmonotonic-of-append

(defthm svex-alist-ovmonotonic-of-append
  (implies (and (svex-alist-ovmonotonic x)
                (svex-alist-ovmonotonic y))
           (svex-alist-ovmonotonic (append x y))))

Theorem: phase-fsm-composition-ovmonotonic-nextstate

(defthm phase-fsm-composition-ovmonotonic-nextstate
  (b* (((flatnorm-res x)) ((fsm approx-fsm)))
    (implies (and (phase-fsm-composition-p approx-fsm x config)
                  (svex-alist-monotonic-p x.assigns)
                  (svex-alist-monotonic-p x.delays)
                  (svarlist-override-p (svex-alist-vars x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-vars x.delays)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.delays)
                                       nil))
             (svex-alist-ovmonotonic approx-fsm.nextstate))))

Theorem: svex-envs-similar-of-append

(defthm svex-envs-similar-of-append
  (implies (and (svex-envs-similar x1 x2)
                (svex-envs-similar y1 y2)
                (set-equiv (alist-keys (svex-env-fix x1))
                           (alist-keys (svex-env-fix x2))))
           (equal (svex-envs-similar (append x1 y1)
                                     (append x2 y2))
                  t)))

Theorem: svex-alist-ovcongruent-of-append

(defthm svex-alist-ovcongruent-of-append
  (implies (and (svex-alist-ovcongruent x)
                (svex-alist-ovcongruent y))
           (svex-alist-ovcongruent (append x y))))

Theorem: phase-fsm-composition-ovcongruent-nextstate

(defthm phase-fsm-composition-ovcongruent-nextstate
  (b* (((flatnorm-res x)) ((fsm approx-fsm)))
    (implies (and (phase-fsm-composition-p approx-fsm x config)
                  (svarlist-override-p (svex-alist-vars x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-vars x.delays)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.delays)
                                       nil))
             (svex-alist-ovcongruent approx-fsm.nextstate))))

Theorem: phase-fsm-composition-ovmonotonic

(defthm phase-fsm-composition-ovmonotonic
  (b* (((flatnorm-res x)) ((fsm approx-fsm)))
    (implies (and (phase-fsm-composition-p approx-fsm x config)
                  (svex-alist-monotonic-p x.assigns)
                  (svex-alist-monotonic-p x.delays)
                  (svarlist-override-p (svex-alist-vars x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-vars x.delays)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.delays)
                                       nil))
             (fsm-ovmonotonic approx-fsm))))

Theorem: phase-fsm-composition-ovcongruent

(defthm phase-fsm-composition-ovcongruent
  (b* (((flatnorm-res x)) ((fsm approx-fsm)))
    (implies (and (phase-fsm-composition-p approx-fsm x config)
                  (svarlist-override-p (svex-alist-vars x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-vars x.delays)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.delays)
                                       nil))
             (fsm-ovcongruent approx-fsm))))

Theorem: flatnorm->ideal-fsm-with-overrides-is-phase-fsm-composition

(defthm flatnorm->ideal-fsm-with-overrides-is-phase-fsm-composition
  (b*
    (((flatnorm-res x))
     (overridekeys (svtv-assigns-override-vars
                        x.assigns
                        (phase-fsm-config->override-config config)))
     (override-flatnorm (flatnorm-add-overrides x overridekeys))
     (override-fsm (flatnorm->ideal-fsm override-flatnorm)))
    (phase-fsm-composition-p override-fsm x config)))

Theorem: flatnorm->ideal-fsm-with-overrides-ovmonotonic

(defthm flatnorm->ideal-fsm-with-overrides-ovmonotonic
  (b*
    (((flatnorm-res x))
     (overridekeys (svtv-assigns-override-vars
                        x.assigns
                        (phase-fsm-config->override-config config)))
     (override-flatnorm (flatnorm-add-overrides x overridekeys))
     (override-fsm (flatnorm->ideal-fsm override-flatnorm)))
    (implies (and (svex-alist-monotonic-p x.assigns)
                  (svex-alist-monotonic-p x.delays)
                  (svarlist-override-p (svex-alist-vars x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-vars x.delays)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.delays)
                                       nil))
             (fsm-ovmonotonic override-fsm))))

Theorem: flatnorm->ideal-fsm-with-overrides-ovcongruent

(defthm flatnorm->ideal-fsm-with-overrides-ovcongruent
  (b*
    (((flatnorm-res x))
     (overridekeys (svtv-assigns-override-vars
                        x.assigns
                        (phase-fsm-config->override-config config)))
     (override-flatnorm (flatnorm-add-overrides x overridekeys))
     (override-fsm (flatnorm->ideal-fsm override-flatnorm)))
    (implies (and (svarlist-override-p (svex-alist-vars x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.assigns)
                                       nil)
                  (svarlist-override-p (svex-alist-vars x.delays)
                                       nil)
                  (svarlist-override-p (svex-alist-keys x.delays)
                                       nil))
             (fsm-ovcongruent override-fsm))))

Theorem: alist-keys-of-flatnorm->ideal-fsm

(defthm alist-keys-of-flatnorm->ideal-fsm
  (b* ((?fsm (flatnorm->ideal-fsm x)))
    (b* (((fsm fsm)) ((flatnorm-res x)))
      (and (equal (svex-alist-keys fsm.values)
                  (svex-alist-keys x.assigns))
           (equal (svex-alist-keys fsm.nextstate)
                  (svex-alist-keys x.delays))))))

Theorem: flatnorm->ideal-fsm-of-flatnorm-res-fix-x

(defthm flatnorm->ideal-fsm-of-flatnorm-res-fix-x
  (equal (flatnorm->ideal-fsm (flatnorm-res-fix x))
         (flatnorm->ideal-fsm x)))

Theorem: flatnorm->ideal-fsm-flatnorm-res-equiv-congruence-on-x

(defthm flatnorm->ideal-fsm-flatnorm-res-equiv-congruence-on-x
  (implies (flatnorm-res-equiv x x-equiv)
           (equal (flatnorm->ideal-fsm x)
                  (flatnorm->ideal-fsm x-equiv)))
  :rule-classes :congruence)