		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-$test$plusargs-to-svex

Signature
(vl-$test$plusargs-to-svex expr design) → (mv warnings svex)
Arguments: expr — Guard (vl-expr-p expr).; design — Guard (vl-design-p design).
Returns: warnings — Type (vl-warninglist-p warnings).; svex — Type (and (sv::svex-p svex) (sv::svarlist-addr-p (sv::svex-vars svex))).

Definitions and Theorems

Function: vl-$test$plusargs-to-svex

(defun vl-$test$plusargs-to-svex (expr design)
 (declare (xargs :guard (and (vl-expr-p expr)
                             (vl-design-p design))))
 (let ((__function__ 'vl-$test$plusargs-to-svex))
  (declare (ignorable __function__))
  (b*
   ((expr (vl-expr-fix expr))
    (arg-str
     (vl-expr-case
         expr
         :vl-literal
         (vl-value-case expr.val
                        :vl-constint (vl-integer-to-string expr.val)
                        :vl-string expr.val.value
                        :otherwise nil)
         :otherwise nil))
    ((unless arg-str)
     (mv
      (fatal
       :type :vl-expr-to-svex-fail
       :msg
       "Unsupported $test$plusargs(...) call.  We only ~
                         support literal strings like ~
                         $test$plusargs(\"foo\"). but found ~
                         $test$plusargs(~a0)."
       :args (list expr)
       :acc nil)
      (svex-x)))
    (ans-svex
      (if (vl-$test$plusargs-p arg-str (vl-design->plusargs design))
          (sv::svex-quote (sv::4vec 1 1))
        (sv::svex-quote (sv::4vec 0 0)))))
   (mv nil ans-svex))))

Theorem: vl-warninglist-p-of-vl-$test$plusargs-to-svex.warnings

(defthm vl-warninglist-p-of-vl-$test$plusargs-to-svex.warnings
  (b* (((mv ?warnings ?svex)
        (vl-$test$plusargs-to-svex expr design)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-$test$plusargs-to-svex.svex

(defthm return-type-of-vl-$test$plusargs-to-svex.svex
  (b* (((mv ?warnings ?svex)
        (vl-$test$plusargs-to-svex expr design)))
    (and (sv::svex-p svex)
         (sv::svarlist-addr-p (sv::svex-vars svex))))
  :rule-classes :rewrite)

Theorem: vl-$test$plusargs-to-svex-of-vl-expr-fix-expr

(defthm vl-$test$plusargs-to-svex-of-vl-expr-fix-expr
  (equal (vl-$test$plusargs-to-svex (vl-expr-fix expr)
                                    design)
         (vl-$test$plusargs-to-svex expr design)))

Theorem: vl-$test$plusargs-to-svex-vl-expr-equiv-congruence-on-expr

(defthm vl-$test$plusargs-to-svex-vl-expr-equiv-congruence-on-expr
  (implies (vl-expr-equiv expr expr-equiv)
           (equal (vl-$test$plusargs-to-svex expr design)
                  (vl-$test$plusargs-to-svex expr-equiv design)))
  :rule-classes :congruence)

Theorem: vl-$test$plusargs-to-svex-of-vl-design-fix-design

(defthm vl-$test$plusargs-to-svex-of-vl-design-fix-design
  (equal (vl-$test$plusargs-to-svex expr (vl-design-fix design))
         (vl-$test$plusargs-to-svex expr design)))

Theorem: vl-$test$plusargs-to-svex-vl-design-equiv-congruence-on-design

(defthm
     vl-$test$plusargs-to-svex-vl-design-equiv-congruence-on-design
  (implies (vl-design-equiv design design-equiv)
           (equal (vl-$test$plusargs-to-svex expr design)
                  (vl-$test$plusargs-to-svex expr design-equiv)))
  :rule-classes :congruence)