		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 mod ialist) → approx-bits
Arguments: x — Guard (vl-expr-p x).; mod — Guard (vl-module-p mod).; ialist — Guard (equal ialist (vl-make-moditem-alist mod)).
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.

This is mostly similar to the vl-wirealist-p facilities, but we trade some accuracy to be especially forgiving. We don't really try to avoid name clashes that could be caused by using escaped identifiers. We also correct for other errors in some questionable ways:

If we encounter an unresolved bit- or part-select from w, or if we encounter a plain w that is not defined, we just return "w[0]".
We don't do any index checking, so if we see an out-of-bounds bit- or part-select we just return strings that refer to non-existent bits.
If we encounter a plain, undefined wire w, we just return "w[0]".

It is somewhat wrong to fudge like this, but these cases won't be hit in well-formed modules, and they allow us to handle expressions even in malformed modules in a mostly correct way without having to consider how to handle problems with collecting bits.

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 mod ialist)))
    (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 mod ialist)))
    (string-listp bits))
  :rule-classes :rewrite)

Subtopics

Vl-exprlist-approx-bits