		Search-engine friendly clone of the ACL2 documentation.

Selfassigns

Vl-expr-approx-bits

Collect strings representing (approximately) the individual bits of wires involved in an expression.

Signature
(vl-expr-approx-bits x ss) → approx-bits
Arguments: x — Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).
Returns: approx-bits — Type (string-listp approx-bits).

We try to return a list of strings like "foo[3]" that are approximately the bits indicated by the expression. This routine is at the core of our selfassigns check, which is just an informal heuristic and doesn't need to be particularly correct or accurate.

Theorem: return-type-of-vl-expr-approx-bits.approx-bits

(defthm return-type-of-vl-expr-approx-bits.approx-bits
  (b* ((?approx-bits (vl-expr-approx-bits x ss)))
    (string-listp approx-bits))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-approx-bits.bits

(defthm return-type-of-vl-exprlist-approx-bits.bits
  (b* ((?bits (vl-exprlist-approx-bits x ss)))
    (string-listp bits))
  :rule-classes :rewrite)

Theorem: vl-expr-approx-bits-of-vl-expr-fix-x

(defthm vl-expr-approx-bits-of-vl-expr-fix-x
  (equal (vl-expr-approx-bits (vl-expr-fix x) ss)
         (vl-expr-approx-bits x ss)))

Theorem: vl-expr-approx-bits-of-vl-scopestack-fix-ss

(defthm vl-expr-approx-bits-of-vl-scopestack-fix-ss
  (equal (vl-expr-approx-bits x (vl-scopestack-fix ss))
         (vl-expr-approx-bits x ss)))

Theorem: vl-exprlist-approx-bits-of-vl-exprlist-fix-x

(defthm vl-exprlist-approx-bits-of-vl-exprlist-fix-x
  (equal (vl-exprlist-approx-bits (vl-exprlist-fix x)
                                  ss)
         (vl-exprlist-approx-bits x ss)))

Theorem: vl-exprlist-approx-bits-of-vl-scopestack-fix-ss

(defthm vl-exprlist-approx-bits-of-vl-scopestack-fix-ss
  (equal (vl-exprlist-approx-bits x (vl-scopestack-fix ss))
         (vl-exprlist-approx-bits x ss)))

Theorem: vl-expr-approx-bits-vl-expr-equiv-congruence-on-x

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

Theorem: vl-expr-approx-bits-vl-scopestack-equiv-congruence-on-ss

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

Theorem: vl-exprlist-approx-bits-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-approx-bits-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-exprlist-approx-bits x ss)
                  (vl-exprlist-approx-bits x-equiv ss)))
  :rule-classes :congruence)

Theorem: vl-exprlist-approx-bits-vl-scopestack-equiv-congruence-on-ss

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

Subtopics

Vl-exprlist-approx-bits