		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-read-include

Read an `include directive.

Signature
(vl-read-include echars config) → (mv filename prefix remainder)
Arguments: echars — Characters we're preprocessing. We assume that `include was just read and removed from echars.
Guard (vl-echarlist-p echars).; config — Guard (vl-loadconfig-p config).
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 config)
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (vl-loadconfig-p config))))
 (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 config))
         (mv nil nil remainder)))
    ((unless filename)
     (mv
       (cw "Preprocessor error (~s0): invalid `include directive.~%"
           (if (consp echars)
               (vl-location-string (vl-echar->loc (car echars)))
               "at end of file"))
       nil echars)))
   (mv filename (append ws1 prefix)
       remainder))))

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

(defthm return-type-of-vl-read-include.filename
        (b* (((mv ?filename ?prefix ?remainder)
              (vl-read-include echars config)))
            (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 config)))
  (implies
       (force (vl-echarlist-p echars))
       (vl-echarlist-p (mv-nth 1 (vl-read-include echars config)))))
 :rule-classes
 ((:rewrite)
  (:type-prescription
       :corollary
       (true-listp (mv-nth 1 (vl-read-include echars config))))))

Theorem: remainder-of-vl-read-include

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

Theorem: append-of-vl-read-include

(defthm append-of-vl-read-include
        (equal (append (mv-nth 1 (vl-read-include echars config))
                       (mv-nth 2 (vl-read-include echars config)))
               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 config)))
                 (equal (mv-nth 2 (vl-read-include echars config))
                        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 config)))
            (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 config))
          (< (acl2-count (mv-nth 2 (vl-read-include echars config)))
             (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.