Vl-expr-names-for-implicit
Collect up wire names that might need to be implicitly declared.
- Signature
(vl-expr-names-for-implicit x) → names
- Arguments
- x — Guard (vl-expr-p x).
- Returns
- names — Type (string-listp names).
Experimentation with NCVerilog and VCS reveals that only certain
names within expressions lead to implicit wires being declared. See especially
the vl/linttest/implicit tests for a test suite of sorts. Here are some
findings:
- If we have a plain name on the left-hand side, like assign foo = 0, then
we get an implicit wire.
- If we instead have something like assign foo.bar = 0, then we're
referencing something elsewhere and we don't want to create implicit wires
named foo or bar.
- When foo is not previously declared, both NCVerilog and VCS reject
assign foo[0] = 0. So I don't think we want to collect names that have
indexing or part-selects applied to them. On the other hand, NCVerilog rejects
but VCS accepts (with warnings) gates such as buf mybuf(o, foo[0]), and
seems to infer a wire for foo. We will try to mimic NCVerilog's behavior
since it is more consistent, and not infer wires that are being indexed
into.
- Suppose we explicitly declare wire [3:0] vec;. Then both NCVerilog
and VCS reject assign vec[w] = 0 where w is undeclared, instead of
inferring an implicit wire w. So I think we do not want to collect names
from within the indices and part-selects. However, distressingly, NCV
and VCS both accept buf myand2(o, vec[w]);, so what is the rule? I think
it seems most sensible to not infer implicit wires within the index
expressions.
- Within gate connections, NCV and VCS allow implicit wires in many
expressions, e.g., w1 + w2, myfun(w), both sides of inside
expressions, etc. (These kinds of expressions aren't allowed in the LHS of
assignments, so we don't worry about them there.)
- In submodule connections, NCV allows implicit wires to be inferred inside
of assignment patterns like triple_t'{a:implicit_w1,b:implicit_w2,...}.
Our version of VCS says this isn't yet implemented.
Theorem: return-type-of-vl-expr-names-for-implicit.names
(defthm return-type-of-vl-expr-names-for-implicit.names
(b* ((?names (vl-expr-names-for-implicit x)))
(string-listp names))
:rule-classes :rewrite)
Theorem: return-type-of-vl-exprlist-names-for-implicit.names
(defthm return-type-of-vl-exprlist-names-for-implicit.names
(b* ((?names (vl-exprlist-names-for-implicit x)))
(string-listp names))
:rule-classes :rewrite)
Theorem: true-listp-of-vl-expr-names-for-implicit
(defthm true-listp-of-vl-expr-names-for-implicit
(true-listp (vl-expr-names-for-implicit x))
:rule-classes :type-prescription)
Theorem: true-listp-of-vl-exprlist-names-for-implicit
(defthm true-listp-of-vl-exprlist-names-for-implicit
(true-listp (vl-exprlist-names-for-implicit x))
:rule-classes :type-prescription)
Theorem: vl-expr-names-for-implicit-of-vl-expr-fix-x
(defthm vl-expr-names-for-implicit-of-vl-expr-fix-x
(equal (vl-expr-names-for-implicit (vl-expr-fix x))
(vl-expr-names-for-implicit x)))
Theorem: vl-exprlist-names-for-implicit-of-vl-exprlist-fix-x
(defthm vl-exprlist-names-for-implicit-of-vl-exprlist-fix-x
(equal (vl-exprlist-names-for-implicit (vl-exprlist-fix x))
(vl-exprlist-names-for-implicit x)))
Theorem: vl-expr-names-for-implicit-vl-expr-equiv-congruence-on-x
(defthm vl-expr-names-for-implicit-vl-expr-equiv-congruence-on-x
(implies (vl-expr-equiv x x-equiv)
(equal (vl-expr-names-for-implicit x)
(vl-expr-names-for-implicit x-equiv)))
:rule-classes :congruence)
Theorem: vl-exprlist-names-for-implicit-vl-exprlist-equiv-congruence-on-x
(defthm
vl-exprlist-names-for-implicit-vl-exprlist-equiv-congruence-on-x
(implies (vl-exprlist-equiv x x-equiv)
(equal (vl-exprlist-names-for-implicit x)
(vl-exprlist-names-for-implicit x-equiv)))
:rule-classes :congruence)
Theorem: vl-expr-names-for-implicit-nrev-removal
(defthm vl-expr-names-for-implicit-nrev-removal
(equal (vl-expr-names-for-implicit-nrev x nrev)
(append nrev (vl-expr-names-for-implicit x))))
Theorem: vl-exprlist-names-for-implicit-nrev-removal
(defthm vl-exprlist-names-for-implicit-nrev-removal
(equal (vl-exprlist-names-for-implicit-nrev x nrev)
(append nrev
(vl-exprlist-names-for-implicit x))))
Subtopics
- Vl-expr-names-for-implicit-nrev
- Vl-exprlist-names-for-implicit
