• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Vwsim
      • Fgl
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
        • Printer
          • Ps
          • Verilog-printing
            • Vl-pp-expr
            • Vl-fmt
            • Vl-progindent
              • Vl-progindent-block
            • Vl-ppc-module
            • Vl-mimic-linestart
            • Vl-maybe-escape-identifier
            • Vl-print-ext-wirename
            • Vl-maybe-strip-outer-linestart
            • Vl-pp-module
            • Vl-print-wirename
            • Vl-print-loc
            • Vl-pp-genblob-guts
            • Vl-pp-describe
            • Vl-print-modname
            • Vl-pp-modinst
            • Vl-pps-module
            • Vl-ppc-modulelist
            • Vl-pp-origexpr
            • Vl-binaryop-precedence
            • Vl-pp-interface
            • Vl-pps-expr
            • Vl-pp-modulename-link
            • Vl-ppcs-module
            • Vl-pp-paramdecl
            • Vl-pp-modulename-link-aux
            • Vl-pp-interfacelist
            • Vl-pp-genblob
            • Vl-pp-vardecl-aux
            • Vl-pp-repetition
            • Vl-pp-packagelist
            • Vl-pp-package
            • Vl-pp-modulelist
            • Vl-pp-modinstlist
            • Vl-pp-modelement
            • Vl-pp-bind
            • Vl-pp-arguments
            • Vl-maybe-escape-string
            • Vl-ps-update-mimic-linebreaks
            • Vl-pp-definition-scope-summary
            • Vl-pp-bindlist
            • Vl-pp-ansi-portdecl
            • Vl-cw-obj
            • Vl-ps-update-show-atts
            • Vl-ps-update-copious-parens
            • Vl-pps-modulelist
            • Vl-ppcs-modulelist
            • Vl-pp-vardecl-atts-begin
            • Vl-pp-portdecl
            • Vl-pp-clkdecl
            • Vl-gatetype-string
            • Vl-coretypename-string
            • Vl-pps-origexpr
            • Vl-pp-vardecl-atts-end
            • Vl-pp-propport
            • Vl-pp-modinst-atts-begin
            • Vl-pp-gateinst-atts-begin
            • Vl-pp-gateinst
            • Vl-pp-gatedelay
            • Vl-pp-foreachstmt-loopvars
            • Vl-pp-dpiimport
            • Vl-nettypename-string
            • Vl-fwdtypedefkind-string
            • Vl-expr-precedence
            • Vl-atts-find-paramname
            • Vl-randomqualifier-string
            • Vl-ps-update-use-origexprs
            • Vl-pp-taskdecl
            • Vl-pp-scope-summary
            • Vl-pp-namedparamvaluelist
            • Vl-pp-modport-port
            • Vl-pp-gatestrength
            • Vl-pp-fundecl
            • Vl-pp-design
            • Vl-pp-assign
            • Vl-distweighttype-string
            • Vl-blocktype-startstring
            • Vl-blocktype-endstring
            • Vl-asserttype-string
            • Vl-assertdeferral-string
            • Vl-alwaystype-string
            • Vl-pp-vardecllist-comma-separated
            • Vl-pp-scopetype
            • Vl-pp-repeateventcontrol
            • Vl-pp-regularport
            • Vl-pp-plainarglist
            • Vl-pp-plainarg
            • Vl-pp-paramvaluelist
            • Vl-pp-namedarglist
            • Vl-pp-interfaceportlist
            • Vl-pp-interfaceport
            • Vl-pp-forloop-assigns
            • Vl-pp-exprdistlist-with-commas
            • Vl-pp-dpiexport
            • Vl-pp-distitem
            • Vl-pp-delayoreventcontrol
            • Vl-direction-string
            • Vl-cstrength-string
            • Vl-casetype-string
            • Vl-casecheck-string
            • Vl-pp-vardecllist-indented
            • Vl-pp-typedeflist-indented
            • Vl-pp-typedef
            • Vl-pp-set-portnames
            • Vl-pp-sequence
            • Vl-pp-regularportlist
            • Vl-pp-propspec
            • Vl-pp-propportlist
            • Vl-pp-property
            • Vl-pp-paramdecllist-indented
            • Vl-pp-namedparamvalue
            • Vl-pp-namedarg
            • Vl-pp-modport-portlist
            • Vl-pp-importlist-indented
            • Vl-pp-eventcontrol
            • Vl-pp-delaycontrol
            • Vl-pp-defaultdisablelist
            • Vl-pp-defaultdisable
            • Vl-pp-covergroup
            • Vl-pp-constint
            • Vl-pp-clkskew
            • Vl-pp-clkassign
            • Vl-pp-cassertionlist
            • Vl-pp-alias
            • Vl-leftright-string
            • Vl-pps-range
            • Vl-pp-weirdint
            • Vl-pp-vardecllist
            • Vl-pp-typedeflist
            • Vl-pp-taskdecllist
            • Vl-pp-specialkey
            • Vl-pp-sequencelist
            • Vl-pp-scopename
            • Vl-pp-rhs
            • Vl-pp-propertylist
            • Vl-pp-programlist
            • Vl-pp-program
            • Vl-pp-portlist
            • Vl-pp-portdecllist
            • Vl-pp-paramvalue
            • Vl-pp-paramdecllist
            • Vl-pp-paramargs
            • Vl-pp-modport
            • Vl-pp-modelementlist
            • Vl-pp-initiallist
            • Vl-pp-import
            • Vl-pp-gclkdecllist
            • Vl-pp-gclkdecl
            • Vl-pp-gateinstlist
            • Vl-pp-fwdtypedeflist
            • Vl-pp-fwdtypedef
            • Vl-pp-fundecllist
            • Vl-pp-exprdist
            • Vl-pp-elabtasklist
            • Vl-pp-dpiimportlist
            • Vl-pp-dpiexportlist
            • Vl-pp-distlist
            • Vl-pp-covergrouplist
            • Vl-pp-config
            • Vl-pp-clkdecllist
            • Vl-pp-clkassignlist
            • Vl-pp-class
            • Vl-pp-assertionlist
            • Vl-pp-alwayslist
            • Vl-vardecl-hiddenp
            • Vl-pp-vardecl
            • Vl-pp-value
            • Vl-pp-udplist
            • Vl-pp-udp
            • Vl-pp-string
            • Vl-pp-rangelist
            • Vl-pp-lifetime
            • Vl-pp-initial
            • Vl-pp-importlist
            • Vl-pp-genvar
            • Vl-pp-finallist
            • Vl-pp-final
            • Vl-pp-extint
            • Vl-pp-elabtask
            • Vl-pp-configlist
            • Vl-pp-classlist
            • Vl-pp-assignlist
            • Vl-pp-always
            • Vl-lifetime-string
            • Vl-dpiprop->string
            • Vl-dpifntask->string
            • Vl-pp-time
            • Vl-pp-real
            • Vl-pp-port
            • Vl-expr-dollarsign-p
            • Vl-dpispec->string
            • Vl-ps->copious-parens-p
            • Vl-ps->show-atts-p
            • Vl-ps->mimic-linebreaks-p
            • Vl-ps->use-origexprs-p
            • Vl-progindent-block-start
            • Vl-progindent-block-end
            • Vl-cw
          • Basic-printing
          • Printing-locally
          • Formatted-printing
          • Accessing-printed-output
          • Json-printing
          • Vl-printedlist
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Verilog-printing

Vl-progindent

Indent until wherever the next line should start, suitable for however many nested constructs are currently open.

Signature
(vl-progindent &key (ps 'ps)) → ps

When we go into a construct such as a module, function body, always statement, begin block, for loop, and so forth, we would like to progressively increase our indentation level. We (arbitrarily) choose to indent by 2 columns for every ``open'' construct, i.e., we want our output to look something like this:

module foo;
  function bar (...);
    begin
      integer a = 1;
      for(integer b = 0; ...; ...)
        foo[b] = a + ...;
    end
  endfunction
endmodule

To implement progressive indentation, we tinker with the autowrap-col and autowrap-ind; see ps for background. We generally expect that autowrap-col starts out at something like 80 or more, while autowrap-ind starts at 5.

It seems nice for the autowrap-ind to consistently be set to a little bit past our current progressive indent level. The autowrap-ind controls how far we'll indent after a long line goes past the right margin. If we're wrapping such a line in, e.g., the for loop above, then we probably want to indent to: 8 columns for the foo loop itself, then some extra since it was a long line we were autowrapping.

So my convention is that vl-progindent will always indent to 5 less than the autowrap-ind. Note also that whenever we increase the progindent level, we bump the right margin out, so that the visual width of each line is roughly constant no matter how far indented over it gets.

Definitions and Theorems

Function: vl-progindent-fn

(defun vl-progindent-fn (ps)
       (declare (xargs :stobjs (ps)))
       (declare (xargs :guard t))
       (let ((__function__ 'vl-progindent))
            (declare (ignorable __function__))
            (vl-indent (nfix (- (vl-ps->autowrap-ind) 5)))))

Subtopics

Vl-progindent-block
Like vl-ps-seq, but increase the progressive indentation while for all of the statements in the block.