Vl-plain-wire-name
(vl-plain-wire-name name) is given name, a string, and
typically returns the symbol ACL2::name.
- Signature
(vl-plain-wire-name name) → emodwire
- Arguments
- name — Guard (stringp name).
- Returns
- emodwire — Type (vl-emodwire-p emodwire).
Typically, for a wire named foo, we generate the symbol
ACL2::|foo|. But there are three special cases.
The symbols ACL2::T and ACL2::F were historically given a special
interpretation by the EMOD hardware simulator, and represented the constant
true and false functions. These wires no longer have a special meaning in
ESIM, but throughout VL our notion of emodwires still assumes that T and F
stand for constant true and false, and, e.g., we still rely on this in e-conversion. We might eventually get away from this by using a transform
analagous to weirdint-elim to introduce T/F wires and eliminate
constants.
The symbol ACL2::NIL is also special, but for a different and more
fundamental reason: NIL has a special meaning in ACL2::patterns, so to
make sure that every vl-emodwire-p is a good atom in the sense of
patterns, we do not allow NIL to even be an emodwire.
At any rate, if we encounter a Verilog wire named T, F, or
NIL, we must use some other name. What other name should we use? We want
to pick something that will not clash with other wire names, but which reflects
the original name of the wire.
We have chosen to use T[0], F[0], and NIL[0] as the
replacements. This should not be too confusing since, e.g., in Verilog
T[0] is typically a valid way to reference a wire named T.
Definitions and Theorems
Function: vl-plain-wire-name$inline
(defun vl-plain-wire-name$inline (name)
(declare (xargs :guard (stringp name)))
(let ((__function__ 'vl-plain-wire-name))
(declare (ignorable __function__))
(mbe :logic
(cond ((equal name "T")
(make-vl-emodwire :basename "T"
:index 0))
((equal name "F")
(make-vl-emodwire :basename "F"
:index 0))
((equal name "NIL")
(make-vl-emodwire :basename "NIL"
:index 0))
(t (make-vl-emodwire :basename (string-fix name)
:index nil)))
:exec
(let ((len (length name)))
(cond ((and (= len 1) (eql (char name 0) #\T))
(make-vl-emodwire :basename "T"
:index 0))
((and (= len 1) (eql (char name 0) #\F))
(make-vl-emodwire :basename "F"
:index 0))
((and (= len 3)
(eql (char name 0) #\N)
(eql (char name 1) #\I)
(eql (char name 2) #\L))
(make-vl-emodwire :basename "NIL"
:index 0))
(t (make-vl-emodwire :basename name
:index nil)))))))
Theorem: vl-emodwire-p-of-vl-plain-wire-name
(defthm vl-emodwire-p-of-vl-plain-wire-name
(b* ((emodwire (vl-plain-wire-name$inline name)))
(vl-emodwire-p emodwire))
:rule-classes :rewrite)
