		Search-engine friendly clone of the ACL2 documentation.

Occform

Vl-occform-argfix

Make extensions explicit for arguments to occform modules.

Signature
(vl-occform-argfix x mod ialist warnings) → (mv warnings new-expr)
Arguments: x — Argument to some operator, sizes already computed.
Guard (vl-expr-p x).; mod — Module where x occurs.
Guard (vl-module-p mod).; ialist — For fast lookups.
Guard (equal ialist (vl-make-moditem-alist mod)).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; new-expr — Type (vl-expr-p new-expr).

See vl-atom-welltyped-p and note that our internal representation of sized expressions leaves zero/sign extensions of identifiers implicit. This is unfortunate because it means that, e.g., if we have something like:

wire [3:0] a;
wire [4:0] b;
assign lhs = a + b;

And we translate it into:

VL_5_BIT_PLUS my_adder (lhs, a, b);

Then the sizes of the arguments appear to be wrong in the pretty-printed representation of the output. We would rather produce something like:

VL_5_BIT_PLUS my_adder (lhs, {1'b0, a}, b);

So that the extensions are explicit. It's relatively easy to do this, now, because since we're going to give this operands as an argument to a submodule, its signedness is no longer relevant.

Definitions and Theorems

Function: vl-occform-argfix

(defun vl-occform-argfix (x mod ialist warnings)
 (declare
    (xargs :guard (and (vl-expr-p x)
                       (vl-module-p mod)
                       (vl-warninglist-p warnings)
                       (equal ialist (vl-make-moditem-alist mod)))))
 (declare (xargs :guard (and (posp (vl-expr->finalwidth x))
                             (vl-expr->finaltype x))))
 (let ((__function__ 'vl-occform-argfix))
  (declare (ignorable __function__))
  (b*
   ((x (vl-expr-fix x))
    ((unless (vl-idexpr-p x)) (mv (ok) x))
    (name (vl-idexpr->name x))
    (item (vl-fast-find-moduleitem name mod ialist))
    ((unless item)
     (mv (fatal :type :vl-occform-bad-id
                :msg "No declaration found for ~a0."
                :args (list x))
         x))
    (tag (tag item))
    ((unless (eq tag :vl-vardecl))
     (mv
      (fatal
       :type :vl-occform-bad-id
       :msg
       "Trying to occform identifier ~a0, which has some strange type ~x1."
       :args (list x (tag item)))
      x))
    ((unless (vl-simplevar-p item))
     (mv
      (fatal
       :type :vl-occform-bad-id
       :msg
       "Trying to occform identifier ~a0, which is not a simple var."
       :args (list x))
      x)))
   (vl-occform-extend-id x (vl-simplevar->range item)
                         warnings))))

Theorem: vl-warninglist-p-of-vl-occform-argfix.warnings

(defthm vl-warninglist-p-of-vl-occform-argfix.warnings
  (b* (((mv ?warnings ?new-expr)
        (vl-occform-argfix x mod ialist warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-expr-p-of-vl-occform-argfix.new-expr

(defthm vl-expr-p-of-vl-occform-argfix.new-expr
  (b* (((mv ?warnings ?new-expr)
        (vl-occform-argfix x mod ialist warnings)))
    (vl-expr-p new-expr))
  :rule-classes :rewrite)

Theorem: vl-expr->finalwidth-of-vl-occform-argfix

(defthm vl-expr->finalwidth-of-vl-occform-argfix
  (equal (vl-expr->finalwidth
              (mv-nth 1
                      (vl-occform-argfix x mod ialist warnings)))
         (vl-expr->finalwidth x)))

Theorem: vl-occform-argfix-of-vl-expr-fix-x

(defthm vl-occform-argfix-of-vl-expr-fix-x
  (equal (vl-occform-argfix (vl-expr-fix x)
                            mod ialist warnings)
         (vl-occform-argfix x mod ialist warnings)))

Theorem: vl-occform-argfix-vl-expr-equiv-congruence-on-x

(defthm vl-occform-argfix-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-occform-argfix x mod ialist warnings)
                  (vl-occform-argfix x-equiv mod ialist warnings)))
  :rule-classes :congruence)

Theorem: vl-occform-argfix-of-vl-module-fix-mod

(defthm vl-occform-argfix-of-vl-module-fix-mod
  (equal (vl-occform-argfix x (vl-module-fix mod)
                            ialist warnings)
         (vl-occform-argfix x mod ialist warnings)))

Theorem: vl-occform-argfix-vl-module-equiv-congruence-on-mod

(defthm vl-occform-argfix-vl-module-equiv-congruence-on-mod
  (implies (vl-module-equiv mod mod-equiv)
           (equal (vl-occform-argfix x mod ialist warnings)
                  (vl-occform-argfix x mod-equiv ialist warnings)))
  :rule-classes :congruence)

Theorem: vl-occform-argfix-of-vl-warninglist-fix-warnings

(defthm vl-occform-argfix-of-vl-warninglist-fix-warnings
  (equal (vl-occform-argfix x mod
                            ialist (vl-warninglist-fix warnings))
         (vl-occform-argfix x mod ialist warnings)))

Theorem: vl-occform-argfix-vl-warninglist-equiv-congruence-on-warnings

(defthm
      vl-occform-argfix-vl-warninglist-equiv-congruence-on-warnings
  (implies (vl-warninglist-equiv warnings warnings-equiv)
           (equal (vl-occform-argfix x mod ialist warnings)
                  (vl-occform-argfix x mod ialist warnings-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-occform-extend-id