• 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
          • Svtv-run-defsvtv$
          • Stv-run
        • Defsvtv-phasewise
        • Svtv
        • Svtv-spec
        • 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

• Svex-stvs

Svtv-run

Run an SVTV and get the outputs.

Signature

(svtv-run svtv inalist &key (skip 'nil) 
          (include 'nil) 
          (boolvars 't) 
          (simplify 'nil) 
          (quiet 'nil) 
          (readable 't) 
          (allvars 'nil)) 
 
  → 
res

Arguments

svtv — Symbolic test vector created by defsvtv.
    Guard (svtv-p svtv).

inalist — Alist mapping input names to 4vec values.

skip — List of output names that should NOT be computed.

include — List of output names that SHOULD be computed.

boolvars — For symbolic execution, assume inputs are Boolean-valued.

simplify — For symbolic execution, apply svex rewriting to the SVTV.

quiet — Don't print inputs/outputs.

readable — Print input/output alists readably.

allvars — For symbolic execution, bind all variables, instead of skipping those not bound in the inalist.

Returns

res — Alist mapping output names to 4vec values.
    Type (svex-env-p res).

Svtv-run runs a simulation of the given symbolic-test-vector on the given inputs and returns the output values.

The input names and output names referred to above are the variable symbols used in the defsvtv form. For example,

(defsvtv my-test
  :inputs
  '(("clk"           1   ~)
    ("dwire"         _   _   _  dat  _)
    ("cwire"         _ ctrl  _   _   _))
  :overrides
  '(("inst.signal"   _   _   _  ov   _))
  :outputs
  '(("firstout"      _   _   _ outa  _)
    ("secondout"     _   _   _   _   _ outb))
  :internals
  '(("inst2.myint"   _  intl)))

In this STV, the input names are dat, ctrl, and ov, and the output names are outa, outb, and intl. See the section stvs-and-testing of the sv-tutorial for more examples.

Definitions and Theorems

Function: svtv-run-fn

(defun acl2::svtv-run-fn (svtv inalist skip include boolvars
                               simplify quiet readable allvars)
 (declare (xargs :guard (svtv-p svtv)))
 (let ((__function__ 'svtv-run))
  (declare (ignorable __function__))
  (b*
   (((svtv svtv) svtv)
    (inalist (ec-call (svex-env-fix$inline inalist)))
    ((with-fast inalist))
    (svtv.inmasks (make-fast-alist svtv.inmasks))
    (boolmasks
     (hons-copy
       (and boolvars
            (svar-boolmasks-limit-to-bound-vars (alist-keys inalist)
                                                svtv.inmasks))))
    (outs
     (b*
      (((unless (or skip include))
        svtv.outexprs)
       (outkeys
         (or include
             (difference (mergesort (svex-alist-keys svtv.outexprs))
                         (mergesort skip)))))
      (fal-extract outkeys svtv.outexprs)))
    (res
     (mbe
      :logic
      (svex-alist-eval-for-symbolic
          outs (make-fast-alist inalist)
          (cons (cons ':vars (alist-keys svtv.inmasks))
                (cons (cons ':boolmasks boolmasks)
                      (cons (cons ':simplify simplify)
                            (cons (cons ':allvars allvars) 'nil)))))
      :exec (svex-alist-eval outs inalist))))
   (clear-memoize-table 'svex-eval)
   (and (not quiet)
        (progn$ (cw "~%SVTV Inputs:~%")
                (if readable (svtv-print-alist-readable inalist)
                  (svtv-print-alist inalist))
                (cw "~%SVTV Outputs:~%")
                (if readable (svtv-print-alist-readable res)
                  (svtv-print-alist res))
                (cw "~%")))
   (make-fast-alist res))))

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

(defthm acl2::svex-env-p-of-svtv-run
  (b* ((res (acl2::svtv-run-fn svtv inalist skip include boolvars
                               simplify quiet readable allvars)))
    (svex-env-p res))
  :rule-classes :rewrite)

Theorem: svtv-run-normalize-irrelevant-inputs

(defthm svtv-run-normalize-irrelevant-inputs
  (implies (syntaxp (not (and (equal boolvars ''t)
                              (equal quiet ''nil)
                              (equal simplify ''nil)
                              (equal readable ''t))))
           (equal (svtv-run svtv inalist
                            :skip skip
                            :include include
                            :boolvars boolvars
                            :allvars allvars
                            :simplify simplify
                            :quiet quiet
                            :readable readable)
                  (svtv-run svtv inalist
                            :skip skip
                            :include include))))

Theorem: alistp-of-svtv-run

(defthm alistp-of-svtv-run
  (alistp (svtv-run svtv inalist
                    :skip skip
                    :include include
                    :boolvars boolvars
                    :allvars allvars
                    :simplify simplify
                    :quiet quiet
                    :readable readable)))

Theorem: lookup-in-svtv-run-under-iff

(defthm lookup-in-svtv-run-under-iff
  (iff (assoc key
              (svtv-run svtv inalist
                        :include include
                        :skip skip
                        :boolvars boolvars
                        :allvars allvars
                        :simplify simplify
                        :quiet quiet
                        :readable readable))
       (and (member key (svtv->outs svtv))
            (if include (member key include)
              (not (member key skip))))))

Theorem: lookup-in-svtv-run-consp

(defthm lookup-in-svtv-run-consp
  (iff (consp (assoc key
                     (svtv-run svtv inalist
                               :include include
                               :skip skip
                               :boolvars boolvars
                               :allvars allvars
                               :simplify simplify
                               :quiet quiet
                               :readable readable)))
       (and (member key (svtv->outs svtv))
            (if include (member key include)
              (not (member key skip))))))

Theorem: 4vec-p-lookup-in-svtv-run

(defthm 4vec-p-lookup-in-svtv-run
  (iff (4vec-p (cdr (assoc key
                           (svtv-run svtv inalist
                                     :include include
                                     :skip skip
                                     :boolvars boolvars
                                     :allvars allvars
                                     :simplify simplify
                                     :quiet quiet
                                     :readable readable))))
       (and (member key (svtv->outs svtv))
            (if include (member key include)
              (not (member key skip))))))

Theorem: lookup-in-svtv-run-with-include

(defthm lookup-in-svtv-run-with-include
  (implies (and (syntaxp (and (quotep include)
                              (not (equal include ''nil))))
                (member signal include))
           (equal (assoc signal
                         (svtv-run svtv inalist
                                   :include include
                                   :skip skip
                                   :boolvars boolvars
                                   :allvars allvars
                                   :simplify simplify
                                   :quiet quiet
                                   :readable readable))
                  (assoc signal (svtv-run svtv inalist)))))

Theorem: lookup-in-svtv-run-with-skip

(defthm lookup-in-svtv-run-with-skip
  (implies (and (syntaxp (and (quotep skip)
                              (not (equal skip ''nil))))
                (not (member signal skip)))
           (equal (assoc signal
                         (svtv-run svtv inalist
                                   :include nil
                                   :skip skip
                                   :boolvars boolvars
                                   :allvars allvars
                                   :simplify simplify
                                   :quiet quiet
                                   :readable readable))
                  (assoc signal (svtv-run svtv inalist)))))

Theorem: svex-env-boundp-of-svtv-run

(defthm svex-env-boundp-of-svtv-run
  (iff (svex-env-boundp key
                        (svtv-run svtv inalist
                                  :include include
                                  :skip skip
                                  :boolvars boolvars
                                  :allvars allvars
                                  :simplify simplify
                                  :quiet quiet
                                  :readable readable))
       (and (if include (member-equal (svar-fix key) include)
              (not (member-equal (svar-fix key) skip)))
            (svex-lookup key (svtv->outexprs svtv)))))

Theorem: svex-env-lookup-in-svtv-run-with-include

(defthm svex-env-lookup-in-svtv-run-with-include
 (implies (and (syntaxp (and (quotep include)
                             (not (equal include ''nil))))
               (member (svar-fix signal) include))
          (equal (svex-env-lookup signal
                                  (svtv-run svtv inalist
                                            :include include
                                            :skip skip
                                            :boolvars boolvars
                                            :allvars allvars
                                            :simplify simplify
                                            :quiet quiet
                                            :readable readable))
                 (svex-env-lookup signal (svtv-run svtv inalist)))))

Theorem: svex-env-lookup-in-svtv-run-with-skip

(defthm svex-env-lookup-in-svtv-run-with-skip
 (implies (and (syntaxp (and (quotep skip)
                             (not (equal skip ''nil))))
               (not (member (svar-fix signal) skip)))
          (equal (svex-env-lookup signal
                                  (svtv-run svtv inalist
                                            :include nil
                                            :skip skip
                                            :boolvars boolvars
                                            :allvars allvars
                                            :simplify simplify
                                            :quiet quiet
                                            :readable readable))
                 (svex-env-lookup signal (svtv-run svtv inalist)))))

Theorem: alist-keys-of-svtv-run

(defthm alist-keys-of-svtv-run
  (equal (alist-keys (svtv-run svtv env))
         (svex-alist-keys (svtv->outexprs svtv))))

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

(defthm acl2::svtv-run-fn-of-svtv-fix-svtv
  (equal (acl2::svtv-run-fn (svtv-fix svtv)
                            inalist skip include boolvars
                            simplify quiet readable allvars)
         (acl2::svtv-run-fn svtv inalist skip include boolvars
                            simplify quiet readable allvars)))

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

(defthm acl2::svtv-run-fn-svtv-equiv-congruence-on-svtv
  (implies
       (svtv-equiv svtv acl2::svtv-equiv)
       (equal (acl2::svtv-run-fn svtv inalist skip include boolvars
                                 simplify quiet readable allvars)
              (acl2::svtv-run-fn acl2::svtv-equiv
                                 inalist skip include boolvars
                                 simplify quiet readable allvars)))
  :rule-classes :congruence)

Subtopics

Svtv-run-defsvtv$

Run an SVTV without first defining it.

Stv-run

Same as svtv-run.