		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-read-include

Read an `include directive.

Signature
(vl-read-include echars ppst) → (mv filename prefix remainder ppst)
Arguments: echars — Characters we're preprocessing. We assume that `include was just read and removed from echars.
Guard (vl-echarlist-p echars).
Returns: filename — Type (or (stringp filename) (not filename)).

We try to read the filename part and return it (without the quotes). Per Section 19.5 of the Verilog spec, the syntax is:

`include "filename"

We are told that filename here can be a relative or absolute path, but there is not any discussion of the actual syntax of the filename (e.g., as it relates to escaping). I believe it should be read as an ordinary string literal. As evidence for this belief:

In Section 19.7 where `line directives are covered, we are told that the filename for `line directives is a string constant, so if there is any justice in the world the filenames for `includes should be the same.
I tried using Verilog-XL and NCVerilog to `include "test\055latch.v", where 055 is the octal character code for the dash character, and both systems were happy with this. So, it seems like these tools are treating it as an ordinary string constant.

NOTE: We are told in Section 19.5 that only whitespace or a comment can appear on the same line as an `include directive. We don't currently try to enforce this restriction since it is somewhat awkward to do so.

Definitions and Theorems

Function: vl-read-include

(defun vl-read-include (echars ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (vl-echarlist-p echars)))
 (let ((__function__ 'vl-read-include))
  (declare (ignorable __function__))
  (b*
   (((mv ws1 remainder)
     (vl-read-while-whitespace echars))
    ((mv filename prefix remainder)
     (if (and (consp remainder)
              (equal (vl-echar->char (car remainder))
                     #\"))
         (vl-read-string remainder
                         (vl-lexstate-init (vl-ppst->config)))
       (mv nil nil remainder)))
    ((unless filename)
     (let
      ((ppst
         (vl-ppst-fatal :msg "~a0: invalid `include directive."
                        :args (list (if (consp echars)
                                        (vl-echar->loc (car echars))
                                      "at end of file")))))
      (mv nil nil echars ppst))))
   (mv filename (append ws1 prefix)
       remainder ppst))))

Theorem: return-type-of-vl-read-include.filename

(defthm return-type-of-vl-read-include.filename
  (b* (((mv ?filename ?prefix ?remainder ?ppst)
        (vl-read-include echars ppst)))
    (or (stringp filename) (not filename)))
  :rule-classes :type-prescription)

Theorem: prefix-of-vl-read-include

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

Theorem: remainder-of-vl-read-include

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

Theorem: append-of-vl-read-include

(defthm append-of-vl-read-include
  (equal (append (mv-nth 1 (vl-read-include echars ppst))
                 (mv-nth 2 (vl-read-include echars ppst)))
         echars))

Theorem: no-change-loser-of-vl-read-include

(defthm no-change-loser-of-vl-read-include
  (implies (not (mv-nth 1 (vl-read-include echars ppst)))
           (equal (mv-nth 2 (vl-read-include echars ppst))
                  echars)))

Theorem: acl2-count-of-vl-read-include-weak

(defthm acl2-count-of-vl-read-include-weak
  (<= (acl2-count (mv-nth 2 (vl-read-include echars ppst)))
      (acl2-count echars))
  :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-read-include-strong

(defthm acl2-count-of-vl-read-include-strong
  (implies (mv-nth 1 (vl-read-include echars ppst))
           (< (acl2-count (mv-nth 2 (vl-read-include echars ppst)))
              (acl2-count echars)))
  :rule-classes ((:rewrite) (:linear)))

Subtopics

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