• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
          • Parse-expressions
          • Parse-udps
          • Vl-genelements
            • Vl-parse-genelements-until
            • Vl-parse-genloop
            • Vl-parse-genif
            • Vl-parse-generate-block
            • Vl-parse-generate
            • Vl-parse-genelement
            • Vl-parse-gencaselist
            • Vl-parse-gencase
          • Parse-paramdecls
          • Parse-blockitems
          • Parse-utils
          • Parse-insts
          • Parse-datatype
          • Parse-functions
          • Parse-datatypes
          • Parse-strengths
          • Vl-parse-genvar-declaration
          • Vl-parse
          • Parse-ports
          • Seq
          • Parse-packages
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-find-file
        • Vl-read-files
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • 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 single genelement. If multiple modelements are produced by parsing the one modelement, it consolidates them into an unnamed begin/end block.

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))
         (return (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 (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 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))
 (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))
         (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))
     (when (and (consp (vl-tokstream->tokens))
                (vl-is-token? :vl-kwd-else))
           (:= (vl-match))
           (else := (vl-parse-generate-block)))
     (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-default)
    (:= (vl-match))
    (:= (vl-match-token :vl-colon))
    (blk :w= (vl-parse-generate-block))
    ((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))
   ((rest . default)
    := (vl-parse-gencaselist))
   (return (cons (cons (cons exprs blk) rest)
                 default)))))

Subtopics

Vl-parse-genelements-until

Vl-parse-genloop

Vl-parse-genif

Vl-parse-generate-block

Vl-parse-generate

Vl-parse-genelement

Vl-parse-gencaselist

Vl-parse-gencase