• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Vl-loadstate
        • Lexer
        • Parser
          • Parse-expressions
          • Parse-udps
          • Parse-statements
          • Parse-property
          • Vl-genelements
            • Vl-parse-generate-block
            • Vl-parse-genelements-until
            • Vl-parse-genloop
            • Vl-parse-genif
            • Vl-parse-generate
            • Vl-parse-genelement
            • Vl-parse-gencaselist
            • Vl-parse-gencase
          • Parse-paramdecls
          • Parse-blockitems
          • Parse-utils
          • Parse-insts
          • Parse-functions
          • Parse-assignments
          • Parse-clocking
          • Parse-strengths
          • Vl-parse-genvar-declaration
          • Vl-parse
          • Parse-netdecls
          • Parse-asserts
          • Vl-maybe-parse-lifetime
          • Parse-dpi-import-export
          • Parse-ports
          • Parse-timeunits
          • Seq
          • Parse-packages
          • Parse-eventctrl
        • Vl-load-merge-descriptions
        • Vl-find-basename/extension
        • Vl-load-file
        • Vl-loadresult
        • Scope-of-defines
        • Vl-find-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-read-file
        • Vl-includeskips-report-gather
        • Vl-load-main
        • Extended-characters
        • Vl-load
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-preprocess-debug
        • Vl-write-preprocessor-debug-file
        • Vl-read-file-report-gather
        • Vl-load-descriptions
        • Vl-load-files
        • Translate-off
        • Vl-load-read-file-hook
        • Vl-read-file-report
        • Vl-loadstate-pad
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-loadstate->warnings
        • Vl-iskips-report
        • Vl-descriptionlist
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Parser

Vl-genelements

Parser for elements contained within modules, interfaces, etc., including generate constructs.

The structure of these is a little confusing -- here is some clarification:

• vl-parse-generate parses a generate construct if the current token is one of for, if, case, or begin. If the first token isn't any of these keywords, it returns NIL.
• vl-parse-genelement parses a generate construct or modelement and returns a list of genelements (because parsing a single modelement may produce more than one, e.g. in the case of a netdeclaration with implicit assignment.)
• vl-parse-generate-block parses a generate construct or modelement and returns a vl-genblock.

Definitions and Theorems

Function: vl-parse-generate-fn

(defun vl-parse-generate-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-generate))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when (vl-is-token? :vl-kwd-for)
         (loopblk := (vl-parse-genloop))
         (return loopblk))
   (when (vl-is-token? :vl-kwd-if)
         (ifblk := (vl-parse-genif))
         (return ifblk))
   (when (vl-is-token? :vl-kwd-case)
         (caseblk := (vl-parse-gencase))
         (return caseblk))
   (when
    (vl-is-token? :vl-kwd-begin)
    (loc := (vl-current-loc))
    (:= (vl-match))
    (when (vl-is-token? :vl-colon)
          (:= (vl-match))
          (blkname := (vl-match-token :vl-idtoken)))
    (elts := (vl-parse-genelements-until :vl-kwd-end))
    (:= (vl-match-token :vl-kwd-end))
    (when blkname
          (:= (vl-parse-endblock-name (vl-idtoken->name blkname)
                                      "begin/end")))
    (return
     (make-vl-genbegin
          :block (make-vl-genblock
                      :name (and blkname (vl-idtoken->name blkname))
                      :elems elts
                      :loc loc))))
   (return nil))))

Function: vl-parse-genelement-fn

(defun vl-parse-genelement-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (xargs :measure-debug t))
  (declare (ignorable config))
  (let ((__function__ 'vl-parse-genelement))
    (declare (ignorable __function__))
    (seq tokstream (gen :w= (vl-parse-generate))
         (when gen (return (list gen)))
         (items := (vl-parse-modelement))
         (return (vl-modelementlist->genelements items)))))

Function: vl-parse-generate-block-fn

(defun vl-parse-generate-block-fn
       (directly-under-condp tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (xargs :measure-debug t))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-generate-block))
  (declare (ignorable __function__))
  (seq
   tokstream (loc := (vl-current-loc))
   (gen :w= (vl-parse-generate))
   (when
     gen
     (return
          (if directly-under-condp
              (vl-genelement-case
                   gen
                   :vl-genbegin gen.block
                   :vl-genif (make-vl-genblock :loc loc
                                               :elems (list gen)
                                               :condnestp t)
                   :vl-gencase (make-vl-genblock :loc loc
                                                 :elems (list gen)
                                                 :condnestp t)
                   :otherwise (make-vl-genblock :loc loc
                                                :elems (list gen)))
            (vl-genelement-case
                 gen
                 :vl-genbegin gen.block
                 :otherwise (make-vl-genblock :loc loc
                                              :elems (list gen))))))
   (items := (vl-parse-modelement))
   (return (make-vl-genblock
                :loc loc
                :elems (vl-modelementlist->genelements items))))))

Function: vl-parse-genelements-until-fn

(defun vl-parse-genelements-until-fn (endkwd tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (declare (xargs :guard (vl-tokentype-p endkwd)))
 (let ((__function__ 'vl-parse-genelements-until))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when (vl-is-token? endkwd)
         (return nil))
   (when
        (vl-is-token? :vl-kwd-generate)
        (:= (vl-match))
        (elems :w= (vl-parse-genelements-until :vl-kwd-endgenerate))
        (:= (vl-match-token :vl-kwd-endgenerate))
        (rest := (vl-parse-genelements-until endkwd))
        (return (append elems rest)))
   (first :s= (vl-parse-genelement))
   (rest := (vl-parse-genelements-until endkwd))
   (return (append first rest)))))

Function: vl-parse-genloop-fn

(defun vl-parse-genloop-fn (tokstream config)
  (declare (xargs :stobjs (tokstream)))
  (declare (xargs :guard (vl-loadconfig-p config)))
  (declare (ignorable config))
  (declare (xargs :guard (and (consp (vl-tokstream->tokens))
                              (vl-is-token? :vl-kwd-for))))
  (let ((__function__ 'vl-parse-genloop))
    (declare (ignorable __function__))
    (seq tokstream
         (header := (vl-parse-genloop-header))
         (body := (vl-parse-generate-block nil))
         (return (change-vl-genloop header
                                    :body body)))))

Function: vl-parse-genif-fn

(defun vl-parse-genif-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (declare (xargs :guard (and (consp (vl-tokstream->tokens))
                             (vl-is-token? :vl-kwd-if))))
 (let ((__function__ 'vl-parse-genif))
  (declare (ignorable __function__))
  (seq
     tokstream (loc := (vl-current-loc))
     (:= (vl-match))
     (:= (vl-match-token :vl-lparen))
     (test := (vl-parse-expression))
     (:= (vl-match-token :vl-rparen))
     (then :w= (vl-parse-generate-block t))
     (when (and (consp (vl-tokstream->tokens))
                (vl-is-token? :vl-kwd-else))
           (:= (vl-match))
           (else := (vl-parse-generate-block t)))
     (return
          (make-vl-genif :test test
                         :then then
                         :else (or else (make-vl-genblock :loc loc))
                         :loc loc)))))

Function: vl-parse-gencase-fn

(defun vl-parse-gencase-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (declare (xargs :guard (and (consp (vl-tokstream->tokens))
                             (vl-is-token? :vl-kwd-case))))
 (let ((__function__ 'vl-parse-gencase))
  (declare (ignorable __function__))
  (seq
      tokstream (loc := (vl-current-loc))
      (:= (vl-match))
      (:= (vl-match-token :vl-lparen))
      (test := (vl-parse-expression))
      (:= (vl-match-token :vl-rparen))
      ((caselist . default)
       := (vl-parse-gencaselist))
      (return (make-vl-gencase
                   :test test
                   :cases caselist
                   :default (or default (make-vl-genblock :loc loc))
                   :loc loc)))))

Function: vl-parse-gencaselist-fn

(defun vl-parse-gencaselist-fn (tokstream config)
 (declare (xargs :stobjs (tokstream)))
 (declare (xargs :guard (vl-loadconfig-p config)))
 (declare (ignorable config))
 (let ((__function__ 'vl-parse-gencaselist))
  (declare (ignorable __function__))
  (seq
   tokstream
   (when (vl-is-token? :vl-kwd-endcase)
         (:= (vl-match))
         (return (cons nil nil)))
   (when
    (vl-is-token? :vl-kwd-default)
    (:= (vl-match))
    (:= (vl-match-token :vl-colon))
    (blk :w= (vl-parse-generate-block t))
    ((rest . rdefault)
     := (vl-parse-gencaselist))
    (when
     rdefault
     (return-raw
        (vl-parse-error "Multiple default cases in generate case")))
    (return (cons rest blk)))
   (exprs := (vl-parse-1+-expressions-separated-by-commas))
   (:= (vl-match-token :vl-colon))
   (blk :w= (vl-parse-generate-block t))
   ((rest . default)
    := (vl-parse-gencaselist))
   (return (cons (cons (cons exprs blk) rest)
                 default)))))

Subtopics

Vl-parse-generate-block

Vl-parse-genelements-until

Vl-parse-genloop

Vl-parse-genif

Vl-parse-generate

Vl-parse-genelement

Vl-parse-gencaselist

Vl-parse-gencase