		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-in->width

Get the bit-length for a particular input simulation variable.

Signature
(stv-in->width x stv) → width
Arguments: x — Guard (symbolp x).; stv — Guard (processed-stv-p stv).
Returns: width — Type (natp width).

For instance, if you have an STV input line like:

("a_bus"  _ _ _ a1 _ a2 _ _)

Then (stv-in->width 'a1 stv) will return the width of a_bus, say 128.

If x isn't one of the STV's inputs, we cause a runtime error and logically return 0.

Definitions and Theorems

Function: stv-in->width

(defun stv-in->width (x stv)
       (declare (xargs :guard (and (symbolp x)
                                   (processed-stv-p stv))))
       (let ((__function__ 'stv-in->width))
            (declare (ignorable __function__))
            (b* (((processed-stv stv) stv)
                 ((compiled-stv cstv) stv.compiled-stv)
                 (look (hons-assoc-equal x cstv.in-usersyms))
                 ((unless look)
                  (raise "Unknown input: ~x0~%" x)
                  0))
                (len (cdr look)))))

Theorem: natp-of-stv-in->width

(defthm natp-of-stv-in->width
        (b* ((width (stv-in->width x stv)))
            (natp width))
        :rule-classes :type-prescription)