• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • 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
          • Svtv-spec-run
          • Svtv-spec-fix
          • Make-svtv-spec
          • Svtv-spec-p
          • Svtv-spec-equiv
          • Svtv-spec->override-test-alists
          • Svtv-spec->override-val-alists
          • Svtv-spec->cycle-phases
          • Change-svtv-spec
          • Svtv-spec->namemap
          • Svtv-spec->initst-alist
          • Svtv-spec->in-alists
          • Svtv-spec->probes
          • Svtv-spec->fsm
        • Defsvtv
        • Process.lisp
        • 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

• Svtv-spec

Svtv-spec-run

Run an svtv-spec object and return its outputs

Signature

(svtv-spec-run x pipe-env &key base-ins initst) → pipe-out

Arguments

x — Guard (svtv-spec-p x).

pipe-env — Guard (svex-env-p pipe-env).

base-ins — Guard (svex-envlist-p base-ins).

initst — Guard (svex-env-p initst).

Returns

pipe-out — Type (svex-env-p pipe-out).

Definitions and Theorems

Function: svtv-spec-run-fn

(defun svtv-spec-run-fn (x pipe-env base-ins initst)
 (declare (xargs :guard (and (svtv-spec-p x)
                             (svex-env-p pipe-env)
                             (svex-envlist-p base-ins)
                             (svex-env-p initst))))
 (declare
  (xargs
   :guard
   (and
    (not
        (hons-dups-p
             (svex-alist-keys (fsm->nextstate (svtv-spec->fsm x)))))
    (equal (svex-alist-keys (svtv-spec->initst-alist x))
           (svex-alist-keys (fsm->nextstate (svtv-spec->fsm x))))
    (svtv-cyclephaselist-has-outputs-captured
         (svtv-spec->cycle-phases x)))))
 (let ((__function__ 'svtv-spec-run))
  (declare (ignorable __function__))
  (b*
   (((svtv-spec x))
    (phase-ins (svtv-spec-pipe-env->phase-envs x pipe-env))
    (full-ins (svex-envlist-x-override phase-ins base-ins))
    (full-initst
      (svex-env-x-override (svex-alist-eval x.initst-alist pipe-env)
                           initst))
    (phase-outs
     (mbe
      :logic (fsm-eval full-ins full-initst x.fsm)
      :exec
      (fsm-eval
          full-ins
          (svex-env-extract (svex-alist-keys (fsm->nextstate x.fsm))
                            full-initst)
          x.fsm))))
   (svtv-spec-phase-outs->pipe-out x phase-outs))))

Theorem: svex-env-p-of-svtv-spec-run

(defthm svex-env-p-of-svtv-spec-run
  (b* ((pipe-out (svtv-spec-run-fn x pipe-env base-ins initst)))
    (svex-env-p pipe-out))
  :rule-classes :rewrite)

Theorem: keys-of-svtv-spec-run

(defthm keys-of-svtv-spec-run
  (b* ((?pipe-out (svtv-spec-run-fn x pipe-env base-ins initst)))
    (equal (alist-keys pipe-out)
           (alist-keys (svtv-spec->probes x)))))

Theorem: svtv-spec-run-fn-of-svtv-spec-fix-x

(defthm svtv-spec-run-fn-of-svtv-spec-fix-x
  (equal (svtv-spec-run-fn (svtv-spec-fix x)
                           pipe-env base-ins initst)
         (svtv-spec-run-fn x pipe-env base-ins initst)))

Theorem: svtv-spec-run-fn-svtv-spec-equiv-congruence-on-x

(defthm svtv-spec-run-fn-svtv-spec-equiv-congruence-on-x
  (implies
       (svtv-spec-equiv x x-equiv)
       (equal (svtv-spec-run-fn x pipe-env base-ins initst)
              (svtv-spec-run-fn x-equiv pipe-env base-ins initst)))
  :rule-classes :congruence)

Theorem: svtv-spec-run-fn-of-svex-env-fix-pipe-env

(defthm svtv-spec-run-fn-of-svex-env-fix-pipe-env
  (equal (svtv-spec-run-fn x (svex-env-fix pipe-env)
                           base-ins initst)
         (svtv-spec-run-fn x pipe-env base-ins initst)))

Theorem: svtv-spec-run-fn-svex-env-equiv-congruence-on-pipe-env

(defthm svtv-spec-run-fn-svex-env-equiv-congruence-on-pipe-env
  (implies
       (svex-env-equiv pipe-env pipe-env-equiv)
       (equal (svtv-spec-run-fn x pipe-env base-ins initst)
              (svtv-spec-run-fn x pipe-env-equiv base-ins initst)))
  :rule-classes :congruence)

Theorem: svtv-spec-run-fn-of-svex-envlist-fix-base-ins

(defthm svtv-spec-run-fn-of-svex-envlist-fix-base-ins
  (equal (svtv-spec-run-fn x pipe-env (svex-envlist-fix base-ins)
                           initst)
         (svtv-spec-run-fn x pipe-env base-ins initst)))

Theorem: svtv-spec-run-fn-svex-envlist-equiv-congruence-on-base-ins

(defthm svtv-spec-run-fn-svex-envlist-equiv-congruence-on-base-ins
  (implies
       (svex-envlist-equiv base-ins base-ins-equiv)
       (equal (svtv-spec-run-fn x pipe-env base-ins initst)
              (svtv-spec-run-fn x pipe-env base-ins-equiv initst)))
  :rule-classes :congruence)

Theorem: svtv-spec-run-fn-of-svex-env-fix-initst

(defthm svtv-spec-run-fn-of-svex-env-fix-initst
  (equal (svtv-spec-run-fn x
                           pipe-env base-ins (svex-env-fix initst))
         (svtv-spec-run-fn x pipe-env base-ins initst)))

Theorem: svtv-spec-run-fn-svex-env-equiv-congruence-on-initst

(defthm svtv-spec-run-fn-svex-env-equiv-congruence-on-initst
  (implies
       (svex-env-equiv initst initst-equiv)
       (equal (svtv-spec-run-fn x pipe-env base-ins initst)
              (svtv-spec-run-fn x pipe-env base-ins initst-equiv)))
  :rule-classes :congruence)