• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
          • Preprocessor
            • Vl-iframe-p
              • Vl-iframe
              • Make-vl-iframe
              • Change-vl-iframe
              • Honsed-vl-iframe
              • Make-honsed-vl-iframe
              • Vl-iframe->some-thing-satisfiedp
              • Vl-iframe->initially-activep
              • Vl-iframe->already-saw-elsep
            • Preprocessor-ifdef-minutia
            • Vl-preprocess-loop
            • Vl-read-until-end-of-define
            • Vl-expand-define
            • Vl-read-include
            • Vl-process-ifdef
            • Vl-substitute-into-macro-text
            • Vl-preprocess
            • Vl-define
            • Vl-process-define
            • Vl-process-undef
            • Preprocessor-include-minutia
            • Vl-split-define-text
            • Vl-read-timescale
            • Vl-line-up-define-formals-and-actuals
            • Vl-process-else
            • Vl-process-endif
            • Vl-istack-p
            • Vl-is-compiler-directive-p
            • Vl-check-remaining-formals-all-have-defaults
            • Vl-safe-previous-n
            • Vl-safe-next-n
            • Vl-defines
            • *vl-preprocess-clock*
          • Vl-loadconfig
          • Lexer
          • Vl-loadstate
          • Parser
          • 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-read-files
          • Vl-find-file
          • 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
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Preprocessor

Vl-iframe-p

`ifdef stack frame objects.

(vl-iframe-p x) is a defaggregate of the following fields.

  • initially-activep — Invariant (booleanp initially-activep).
  • some-thing-satisfiedp — Invariant (booleanp some-thing-satisfiedp).
  • already-saw-elsep — Invariant (booleanp already-saw-elsep).

Source link: vl-iframe-p

Iframes ("ifdef frames") are essential in our approach to handling `ifdef directives. Our main preprocessing function, vl-preprocess-loop, takes three arguments that have to do with handling ifdefs:

  • defines is the current vl-defines-p alist. For now, just assume that we are able to appropriately keep this list updated as we encounter defines and undefs.
  • activep is a boolean which is true whenever the characters are are now reading from the file ought to be given to the lexer -- the idea is that when we encounter an `ifdef whose condition isn't satisfied, we turn off activep until the closing `endif is encountered.
  • istack is a stack of vl-iframe-p objects which explain how to manage activep as we descend through a nest of `ifdef, `ifndef, `elsif, `else, and `endif directives.

Let us temporarily ignore nested directives. Then, our task would be to decide when activep should be turned on during sequences like this:

`if[n]def THING
  stuff1
`elsif THING2
  stuff2
`elsif THING3
  stuff3
`else
  stuff4
`endif

The semantics of this (Section 19.4) are essentially: figure out the first THING that is satisfied, include its stuff, and ignore the rest. So for instance, if THING2 and THING3 are both satisfied, we still only want to include stuff2 since it comes first.

To implement this, the basic idea is that when we encounter an `ifdef or `ifndef directive, we construct an iframe that helps us set activep correctly. The first two fields of the iframe are:

some-thing-satisfiedp
which indicates if any of the THINGs we have seen so far was satisfied, and
already-saw-elsep
which indicates whether we have seen an `else and is used only as a sanity check to prevent multiple `else clauses.

And as we descend through the above sequences, we update the iframe and ensure that activep is set exactly when the current THING is satisfied and no previous THING was satisfied.

But the story is not quite complete yet, because we also have to handle nested ifdefs. For example, imagine we have:

`ifdef OUTER
  ...
  `ifdef INNER_THING1
    stuff1
  `elsif INNER2_THING2
    stuff2
  `else
    stuff3
  `endif
  ...
`endif

This is almost the same, except that now we only want to turn on activep when OUTER is also satisfied. To keep track of this, we add another field to our iframe objects:

initially-activep
which indicates whether activep was set when we encountered the `ifdef or ifndef for this iframe.

Now, activep should be enabled exactly when:

  • (inner criteria): the current THING is satisfied and no previous THING was sastified, and
  • (outer-criteria): initially-activep was also set, i.e., this chunk of code is not being blocked by some THING in an outer ifdef tree.

Subtopics

Vl-iframe
Raw constructor for vl-iframe-p structures.
Make-vl-iframe
Constructor macro for vl-iframe-p structures.
Change-vl-iframe
A copying macro that lets you create new vl-iframe-p structures, based on existing structures.
Honsed-vl-iframe
Raw constructor for honsed vl-iframe-p structures.
Make-honsed-vl-iframe
Constructor macro for honsed vl-iframe-p structures.
Vl-iframe->some-thing-satisfiedp
Access the some-thing-satisfiedp field of a vl-iframe-p structure.
Vl-iframe->initially-activep
Access the initially-activep field of a vl-iframe-p structure.
Vl-iframe->already-saw-elsep
Access the already-saw-elsep field of a vl-iframe-p structure.