		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-cw-obj

Similar to vl-cw, but the arguments are given as a list instead of as macro arguments.

Signature
(vl-cw-obj msg args &key (ps 'ps)) → ps
Arguments: msg — Guard (stringp msg).

For example:

(vl-cw "hello ~x0 ~x1 ~x2" 3 4 5)
  --->
(vl-cw-obj "hello ~x0 ~x1 ~x2" (list 3 4 5))

This can be useful for grouping up arguments into cons structures.

BOZO I should probably implement something like ~@ and use msg instead.

Definitions and Theorems

Function: vl-cw-obj-fn

(defun vl-cw-obj-fn (msg args ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (stringp msg)))
 (let ((__function__ 'vl-cw-obj))
  (declare (ignorable __function__))
  (cond
       ((<= (len args) 10)
        (vl-fmt msg
                (pairlis$ '(#\0 #\1 #\2 #\3 #\4 #\5 #\6 #\7 #\8 #\9)
                          (list-fix args))))
       (t (prog2$ (raise "vl-cw-obj is limited to 10 arguments.")
                  ps)))))

Theorem: vl-cw-obj-fn-of-str-fix-msg

(defthm vl-cw-obj-fn-of-str-fix-msg
  (equal (vl-cw-obj-fn (str-fix msg) args ps)
         (vl-cw-obj-fn msg args ps)))

Theorem: vl-cw-obj-fn-streqv-congruence-on-msg

(defthm vl-cw-obj-fn-streqv-congruence-on-msg
  (implies (streqv msg msg-equiv)
           (equal (vl-cw-obj-fn msg args ps)
                  (vl-cw-obj-fn msg-equiv args ps)))
  :rule-classes :congruence)