		Search-engine friendly clone of the ACL2 documentation.

Vl-lex

Vl-lex-1step-or-number

Match any integral_number or 1step.

Signature
(vl-lex-1step-or-number echars breakp st warnings) → (mv token? remainder warnings)
Arguments: echars — Guard (and (vl-echarlist-p echars) (consp echars) (vl-decimal-digit-p (vl-echar->char (car echars)))) .; breakp — Guard (booleanp breakp).; st — Guard (vl-lexstate-p st).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).

This is a ugly function that allows us to treat 1step in a special way. No other SystemVerilog keyword begins with a number and 1step is not listed in the keywords table in the standard. However, we find that for instance in some other tools we are permitted to write:

wire #1 step;

This seems to indicate that #1step delay values are indeed to be treated as atomic tokens and spaces should not be permitted within them. We therefore handle them directly in the lexer.

Definitions and Theorems

Function: vl-lex-1step-or-number

(defun vl-lex-1step-or-number (echars breakp st warnings)
 (declare
  (xargs
       :guard
       (and (and (vl-echarlist-p echars)
                 (consp echars)
                 (vl-decimal-digit-p (vl-echar->char (car echars))))
            (booleanp breakp)
            (vl-lexstate-p st)
            (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-lex-1step-or-number))
   (declare (ignorable __function__))
   (b* (((unless (and (eql (vl-echar->char (car echars)) #\1)
                      (vl-lexstate->onestepp st)))
         (vl-lex-number echars breakp st warnings))
        ((mv step remainder)
         (vl-read-literal "step" (cdr echars)))
        ((when step)
         (mv (make-vl-plaintoken :etext (cons (car echars) step)
                                 :type :vl-1step
                                 :breakp breakp)
             remainder (ok))))
     (vl-lex-number echars breakp st warnings))))

Theorem: vl-warninglist-p-of-vl-lex-1step-or-number.warnings

(defthm vl-warninglist-p-of-vl-lex-1step-or-number.warnings
  (b* (((mv ?token? ?remainder ?warnings)
        (vl-lex-1step-or-number echars breakp st warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-token-p-of-vl-lex-1step-or-number

(defthm vl-token-p-of-vl-lex-1step-or-number
 (implies
  (and (force (vl-echarlist-p echars))
       (booleanp breakp))
  (equal
   (vl-token-p
        (mv-nth 0
                (vl-lex-1step-or-number echars breakp st warnings)))
   (if (mv-nth 0
               (vl-lex-1step-or-number echars breakp st warnings))
       t
     nil))))

Theorem: true-listp-of-vl-lex-1step-or-number

(defthm true-listp-of-vl-lex-1step-or-number
 (equal
   (true-listp
        (mv-nth 1
                (vl-lex-1step-or-number echars breakp st warnings)))
   (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
    (true-listp echars)
    (true-listp
       (mv-nth
            1
            (vl-lex-1step-or-number echars breakp st warnings)))))))

Theorem: vl-echarlist-p-of-vl-lex-1step-or-number

(defthm vl-echarlist-p-of-vl-lex-1step-or-number
 (implies
  (force (vl-echarlist-p echars))
  (equal
   (vl-echarlist-p
        (mv-nth 1
                (vl-lex-1step-or-number echars breakp st warnings)))
   t)))

Theorem: append-of-vl-lex-1step-or-number

(defthm append-of-vl-lex-1step-or-number
 (implies
  (and (mv-nth 0
               (vl-lex-1step-or-number echars breakp st warnings))
       (force (vl-echarlist-p echars))
       (booleanp breakp))
  (equal
   (append
    (vl-token->etext
        (mv-nth 0
                (vl-lex-1step-or-number echars breakp st warnings)))
    (mv-nth 1
            (vl-lex-1step-or-number echars breakp st warnings)))
   echars)))

Theorem: no-change-loser-of-vl-lex-1step-or-number

(defthm no-change-loser-of-vl-lex-1step-or-number
 (implies
  (not (mv-nth 0
               (vl-lex-1step-or-number echars breakp st warnings)))
  (equal (mv-nth 1
                 (vl-lex-1step-or-number echars breakp st warnings))
         echars)))

Theorem: acl2-count-of-vl-lex-1step-or-number-weak

(defthm acl2-count-of-vl-lex-1step-or-number-weak
 (<=
   (acl2-count
        (mv-nth 1
                (vl-lex-1step-or-number echars breakp st warnings)))
   (acl2-count echars))
 :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-lex-1step-or-number-strong

(defthm acl2-count-of-vl-lex-1step-or-number-strong
 (implies
  (and (mv-nth 0
               (vl-lex-1step-or-number echars breakp st warnings))
       t)
  (<
   (acl2-count
        (mv-nth 1
                (vl-lex-1step-or-number echars breakp st warnings)))
   (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))

Subtopics

Vl-lex-1step-or-number-token/remainder-thms: Token and remainder theorems for vl-lex-1step-or-number, automatically generated by def-token/remainder-thms.