		Search-engine friendly clone of the ACL2 documentation.

Lex-numbers

Vl-read-decimal-value

Matches unsigned_number | x_digit { _ } | z_digit { _ }.

Signature
(vl-read-decimal-value echars) → (mv prefix remainder)
Arguments: echars — Guard (vl-echarlist-p echars).

This doesn't correspond to a named production in the Verilog grammars, but captures everything that's legal after the decimal_base part of a decimal_number. That is, we're basically refactoring decimal_number as follows:

decimal-number ::= unsigned_number
                 | [size] decimal_base decimal_value

decimal_value ::= unsigned_number
                | x_digit { _ }
                | z_digit { _ }

Neither Verilog-2005 and SystemVerilog-2012 explicitly rules out spaces in the x_digit and z_digit cases here, so arguably the spec allows for syntax like 10 'd x__ __ __. However, this seems crazy and none of Verilog-XL, NCVerilog, or VCS accepts such syntax, so we think this is just a minor oversight in the standards.

Definitions and Theorems

Function: vl-read-decimal-value

(defun vl-read-decimal-value (echars)
  (declare (xargs :guard (vl-echarlist-p echars)))
  (let ((__function__ 'vl-read-decimal-value))
    (declare (ignorable __function__))
    (b* (((when (atom echars)) (mv nil echars))
         ((unless (or (vl-x-digit-echar-p (car echars))
                      (vl-z-digit-echar-p (car echars))))
          (vl-read-unsigned-number echars))
         ((mv prefix remainder)
          (vl-read-while-underscore (cdr echars))))
      (mv (cons (car echars) prefix)
          remainder))))

Theorem: prefix-of-vl-read-decimal-value

(defthm prefix-of-vl-read-decimal-value
 (and
   (true-listp (mv-nth 0 (vl-read-decimal-value echars)))
   (implies
        (force (vl-echarlist-p echars))
        (vl-echarlist-p (mv-nth 0 (vl-read-decimal-value echars)))))
 :rule-classes
 ((:rewrite)
  (:type-prescription
       :corollary
       (true-listp (mv-nth 0 (vl-read-decimal-value echars))))))

Theorem: remainder-of-vl-read-decimal-value

(defthm remainder-of-vl-read-decimal-value
 (and
   (equal (true-listp (mv-nth 1 (vl-read-decimal-value echars)))
          (true-listp echars))
   (implies
        (force (vl-echarlist-p echars))
        (vl-echarlist-p (mv-nth 1 (vl-read-decimal-value echars)))))
 :rule-classes
 ((:rewrite)
  (:type-prescription
     :corollary
     (implies
          (true-listp echars)
          (true-listp (mv-nth 1 (vl-read-decimal-value echars)))))))

Theorem: append-of-vl-read-decimal-value

(defthm append-of-vl-read-decimal-value
  (equal (append (mv-nth 0 (vl-read-decimal-value echars))
                 (mv-nth 1 (vl-read-decimal-value echars)))
         echars))

Theorem: no-change-loser-of-vl-read-decimal-value

(defthm no-change-loser-of-vl-read-decimal-value
  (implies (not (mv-nth 0 (vl-read-decimal-value echars)))
           (equal (mv-nth 1 (vl-read-decimal-value echars))
                  echars)))

Theorem: acl2-count-of-vl-read-decimal-value-weak

(defthm acl2-count-of-vl-read-decimal-value-weak
  (<= (acl2-count (mv-nth 1 (vl-read-decimal-value echars)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-read-decimal-value-strong

(defthm acl2-count-of-vl-read-decimal-value-strong
  (implies (mv-nth 0 (vl-read-decimal-value echars))
           (< (acl2-count (mv-nth 1 (vl-read-decimal-value echars)))
              (acl2-count echars)))
  :rule-classes ((:rewrite) (:linear)))

Subtopics

Vl-read-decimal-value-prefix/remainder-thms: Prefix and remainder theorems for vl-read-decimal-value, automatically generated by def-prefix/remainder-thms.