		Search-engine friendly clone of the ACL2 documentation.

Mlib

Vl-consteval

An evaluator for a small set of "constant expressions" in Verilog.

Signature
(vl-consteval x ss) → (mv successp ans)
Arguments: x — Expression to try to evaluate.
Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).
Returns: successp — Indicates whether we successfully sized and evaluated x to a constant.
Type (booleanp successp).; ans — On success, a resolved, constant expression with the appropriate width and size.
Type (vl-expr-p ans).

This is a careful, limited evaluator for a small subset of Verilog expressions. It is intended to be safe for use in contexts such as:

Wire ranges, e.g., wire [width-1:0] foo
Selects from wires, e.g., foo[width-1:0]
Parameter values arguments, e.g., mymod #(.size(width*2)) ...

Where there is no explicit left-hand side. This evaluator does not know how to look up identifiers like width. Instead, it is generally meant to be useful after `defined constants and parameters have already been expanded.

Note that in general it is not safe to call this function on arbitrary Verilog expressions to do constant folding. That is, this function does not know about any surrounding expression or left-hand side, which could alter the widths (and hence the values) produced by certain operations.

However, we think this function is safe to use on top-level indexes into arrays, range expressions, parameter values, etc., where there is no left-hand side context.

This function can fail for a number of reasons. For it to succeed, the expression can contain only resolved constant values. That is, things like "weird" integers with X/Z bits aren't allowed. Neither are any identifiers, function calls, and so forth. The operators in the expression must be supported by vl-consteval-main, and the evaluation must proceed without "run-time errors" such as division by zero.

Definitions and Theorems

Function: vl-consteval

(defun vl-consteval (x ss)
  (declare (xargs :guard (and (vl-expr-p x)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-consteval))
    (declare (ignorable __function__))
    (b* ((x (vl-expr-fix x))
         ((mv successp ?warnings sized-x)
          (vl-expr-size nil x
                        ss *vl-fake-elem-for-vl-consteval* nil))
         ((unless (and successp
                       (posp (vl-expr->finalwidth sized-x))
                       (vl-expr->finaltype sized-x)))
          (mv nil x))
         ((mv okp ans)
          (vl-consteval-main sized-x ss))
         ((unless okp) (mv nil x)))
      (mv t ans))))

Theorem: booleanp-of-vl-consteval.successp

(defthm booleanp-of-vl-consteval.successp
  (b* (((mv ?successp ?ans)
        (vl-consteval x ss)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-expr-p-of-vl-consteval.ans

(defthm vl-expr-p-of-vl-consteval.ans
  (b* (((mv ?successp ?ans)
        (vl-consteval x ss)))
    (vl-expr-p ans))
  :rule-classes :rewrite)

Theorem: vl-expr-resolved-p-of-vl-consteval

(defthm vl-expr-resolved-p-of-vl-consteval
  (b* (((mv ?successp ?ans)
        (vl-consteval x ss)))
    (implies successp (vl-expr-resolved-p ans)))
  :rule-classes :rewrite)

Theorem: vl-expr-welltyped-p-of-vl-consteval

(defthm vl-expr-welltyped-p-of-vl-consteval
  (b* (((mv ?successp ?ans)
        (vl-consteval x ss)))
    (implies successp (vl-expr-welltyped-p ans)))
  :rule-classes :rewrite)

Theorem: vl-expr->finalwidth-of-vl-consteval

(defthm vl-expr->finalwidth-of-vl-consteval
  (b* (((mv ?successp ?ans)
        (vl-consteval x ss)))
    (implies successp
             (posp (vl-expr->finalwidth ans))))
  :rule-classes :type-prescription)

Theorem: vl-expr->finaltype-of-vl-consteval

(defthm vl-expr->finaltype-of-vl-consteval
  (b* (((mv ?successp ?ans)
        (vl-consteval x ss)))
    (implies successp
             (vl-exprtype-p (vl-expr->finaltype ans))))
  :rule-classes :rewrite)

Theorem: vl-consteval-of-vl-expr-fix-x

(defthm vl-consteval-of-vl-expr-fix-x
  (equal (vl-consteval (vl-expr-fix x) ss)
         (vl-consteval x ss)))

Theorem: vl-consteval-vl-expr-equiv-congruence-on-x

(defthm vl-consteval-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-consteval x ss)
                  (vl-consteval x-equiv ss)))
  :rule-classes :congruence)

Theorem: vl-consteval-of-vl-scopestack-fix-ss

(defthm vl-consteval-of-vl-scopestack-fix-ss
  (equal (vl-consteval x (vl-scopestack-fix ss))
         (vl-consteval x ss)))

Theorem: vl-consteval-vl-scopestack-equiv-congruence-on-ss

(defthm vl-consteval-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-consteval x ss)
                  (vl-consteval x ss-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-consteval-$bits
Vl-consteval-shiftop
Vl-consteval-concat
Vl-consteval-ans
Vl-consteval-unary-reduxop
Vl-consteval-binop
Vl-consteval-cmpop
Vl-consteval-usertype-bits
Vl-consteval-binlogic
Vl-clog2: Implementation of the $clog2 system function.
Vl-consteval-basictype-bits
Vl-consteval-wideunary
Vl-consteval-main: Recursive helper for vl-consteval
*vl-fake-elem-for-vl-consteval*