		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-lint-report

Signature
(vl-lint-report config loadresult lintresult state) → state
Arguments: config — Guard (vl-lintconfig-p config).; loadresult — Guard (vl-loadresult-p loadresult).; lintresult — Guard (vl-lintresult-p lintresult).
Returns: state — Type (state-p1 state), given (state-p1 state).

Definitions and Theorems

Function: vl-lint-report

(defun vl-lint-report (config loadresult lintresult state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (vl-lintconfig-p config)
                             (vl-loadresult-p loadresult)
                             (vl-lintresult-p lintresult))))
 (let ((__function__ 'vl-lint-report))
  (declare (ignorable __function__))
  (b*
   (((vl-lintresult lintresult))
    ((vl-loadresult loadresult))
    ((vl-lintconfig config))
    (reportcard lintresult.reportcard)
    (suppressed (vl-reportcard-keep-suppressed reportcard))
    (reportcard (vl-reportcard-remove-suppressed reportcard))
    (sd-probs lintresult.sd-probs)
    ((mv major minor)
     (cwtime (sd-filter-problems sd-probs nil nil)))
    (major (reverse major))
    (minor (reverse minor))
    (- (cw "~%vl-lint: saving results...~%~%"))
    (othertypes
         (difference (mergesort (vl-reportcard-types reportcard))
                     (mergesort (append *warnings-covered*
                                        *warnings-ignored*))))
    (state
     (with-ps-file
      "vl-basic.txt"
      (vl-ps-update-autowrap-col 68)
      (vl-lint-print-warnings "vl-basic.txt"
                              "Basic" *basic-warnings* reportcard)))
    (state
     (with-ps-file
      "vl-trunc.txt"
      (vl-ps-update-autowrap-col 68)
      (vl-print
       "
NOTE: see the bottom of this file for an explanation of what these warnings
mean and how to avoid them.

")
      (vl-lint-print-warnings "vl-trunc.txt" "Truncation/Extension"
                              *trunc-warnings* reportcard)
      (vl-print
       "

UNDERSTANDING THESE WARNINGS.

1. VL-WARN-TRUNCATION warnings are issued when the left-hand side of an
assignment statement is not as wide as the right-hand side.

False positives here can typically be suppressed by using part-selects to make
the intended truncations explicit.  For instance:

    wire [47:0] foo ;
    wire [63:0] bar ;

    assign foo = bar ;        // implicit truncation, causes warning
    assign foo = bar[47:0] ;  // explicit truncation, no warning

    assign foo = condition ? bar : 0 ;      // implicit truncation, causes warning
    assign foo = condition ? bar[47:0] : 0; // explicit truncation, no warning


2. VL-WARN-EXTENSION warnings are the opposite: they are issued when the
left-hand side is wider than the right-hand side would have been on its own.

False-positives can again typically be suppressed by explicitly concatenting in
zeroes, or by using part-selects to cut the left-hand side to the right size.
For instance:

    wire [47:0] foo ;
    wire [63:0] bar ;

    assign bar = foo ;             // implicit extension, causes warning
    assign bar = { 16'b0, foo } ;  // explicit extension, no warning
    assign bar[47:0] = foo;        // no extension, no warning


Note that we consider certain truncation and extension warnings to be \"minor\"
and do not report them here.  Such warnings are unlikely to be a problem, but
you can see \"vl-trunc-minor.txt\" to review them.")))
    (state
     (with-ps-file
        "vl-fussy.txt"
        (vl-ps-update-autowrap-col 68)
        (vl-lint-print-warnings "vl-fussy.txt" "Fussy Size Warnings"
                                *fussy-size-warnings* reportcard)))
    (state (with-ps-file
                "vl-fussy-minor.txt"
                (vl-ps-update-autowrap-col 68)
                (vl-lint-print-warnings "vl-fussy-minor.txt"
                                        "Minor Fussy Size Warnings"
                                        *fussy-size-minor-warnings*
                                        reportcard)))
    (state
     (with-ps-file
          "vl-lucid.txt"
          (vl-ps-update-autowrap-col 68)
          (vl-lint-print-warnings "vl-lucid.txt" "Lucidity Checking"
                                  *lucid-warnings* reportcard)))
    (state
         (with-ps-file "vl-lucid-vars.txt"
                       (vl-ps-update-autowrap-col 68)
                       (vl-lint-print-warnings
                            "vl-lucid-vars.txt" "Lucidity Checking"
                            *lucid-variable-warnings* reportcard)))
    (state
     (with-ps-file
         "vl-sv-use-set.txt"
         (vl-ps-update-autowrap-col 68)
         (vl-lint-print-warnings "vl-sv-use-set.txt"
                                 "SV Use/Set Checking"
                                 *sv-use-set-warnings* reportcard)))
    (state
     (with-ps-file
      "vl-eliminated-mods.txt"
      (vl-ps-update-autowrap-col 68)
      (vl-print
       "
Note: These modules were eliminated because they were never instantiated anywhere in the top module's hierarchy.
")
      (vl-print-eliminated-descs lintresult.design
                                 lintresult.design-orig)))
    (state
         (if (not major)
             (progn$ (cw "; No Skip-Detect Warnings.~%")
                     state)
           (progn$ (cw "vl-skipdet.txt: ~x0 Skip-Detect Warnings.~%"
                       (len major))
                   (with-ps-file "vl-skipdet.txt"
                                 (vl-ps-update-autowrap-col 68)
                                 (vl-cw "Skip-Detect Warnings.~%~%")
                                 (sd-pp-problemlist-long major)))))
    (state
     (with-ps-file
      "vl-trunc-minor.txt"
      (vl-ps-update-autowrap-col 68)
      (vl-print
       "
NOTE: see the bottom of this file for an explanation of what these warnings
mean and how to avoid them.

")
      (vl-lint-print-warnings "vl-trunc-minor.txt"
                              "Minor Truncation/Extension"
                              *trunc-minor-warnings* reportcard)
      (vl-print
       "

UNDERSTANDING THESE WARNINGS.

1.  VL-WARN-TRUNCATION-32 warnings are generated for any assignments that are
being truncated and whose right-hand sides are 32-bits wide.  This is a minor
warning because it typically arises from assignments where plain integers are
involved, e.g., if foo and bar are 10 bits wide, then a truncation-32 warning
will be generated for:

    assign foo = bar ^ 5;

This is because \"5\" has an implementation-dependent width (of at least 32
bits), and in VL-Lint we treat it as being 32-bits wide.  So, the above
describes a 32-bit XOR that is then truncated down to 10 bits.  Fixing these
warnings is usually easy: just explicitly specify the sizes of the numbers
involved, e.g., a \"corrected\" version might be:

    assign foo = bar ^ 10'd 5;

This is generally a good idea since it avoids any implementation-dependent
sizing (which can occasionally affect the results of expressions).


2.  VL-WARN-EXTENSION-MINOR warnings are generated for any assignments where
the width of the left-hand side is used to size the expression, and where the
right-hand side involves only addition operations.  For instance, given:

    wire [9:0] foo;
    wire [9:0] bar;
    wire [9:0] sum;
    wire carry;

Then an assignment like this:

    assign { carry, sum } = foo + bar;

would result in a minor extension warning.  These warnings are typically quite
minor since you frequently want to get the carry out of a sum.  But you could
suppress them by writing something like this:

    Variant 1: assign {carry, sum} = {1'b0,foo} + bar;
    Variant 2: assign {carry, sum} = foo + bar + 11'b0;

or similar, to make explicit on the right-hand side that you want an 11-bit
wide addition instead of a 10-bit wide addition.")))
    (state
     (if (not minor)
         (prog2$ (cw "; No Minor Skip-Detect Warnings.~%")
                 state)
      (prog2$
       (cw "vl-skipdet-minor.txt: ~x0 Minor Skip-Detect Warnings.~%"
           (len minor))
       (with-ps-file "vl-skipdet-minor.txt"
                     (vl-ps-update-autowrap-col 68)
                     (vl-cw "Minor Skip-Detect Warnings.~%~%")
                     (sd-pp-problemlist-long minor)))))
    (state
     (with-ps-file
       "vl-smells.txt"
       (vl-ps-update-autowrap-col 68)
       (vl-lint-print-warnings "vl-smells.txt" "Code-Smell Warnings"
                               *smell-warnings* reportcard)))
    (state
     (with-ps-file
        "vl-smells-minor.txt"
        (vl-ps-update-autowrap-col 68)
        (vl-lint-print-warnings "vl-smells-minor.txt"
                                "Minor Code-Smell Warnings"
                                *smell-minor-warnings* reportcard)))
    (state
     (with-ps-file
         "vl-same-ports.txt"
         (vl-ps-update-autowrap-col 68)
         (vl-lint-print-warnings "vl-same-ports.txt"
                                 "Same-ports Warnings"
                                 *same-ports-warnings* reportcard)))
    (state (with-ps-file
                "vl-same-ports-minor.txt"
                (vl-ps-update-autowrap-col 68)
                (vl-lint-print-warnings "vl-same-ports-minor.txt"
                                        "Minor same-ports Warnings"
                                        *same-ports-minor-warnings*
                                        reportcard)))
    (state
     (with-ps-file
         "vl-other.txt"
         (vl-ps-update-autowrap-col 68)
         (vl-lint-print-warnings "vl-other.txt" "Other/Unclassified"
                                 othertypes reportcard)))
    (state
         (with-ps-file
              "vl-suppressed.txt"
              (vl-ps-update-autowrap-col 58)
              (vl-lint-print-all-warnings "vl-suppressed.txt"
                                          "suppressed" suppressed)))
    (- (cw "~%"))
    (state
       (cwtime
            (with-ps-file "vl-warnings.json"
                          (vl-print "{\"warnings\":")
                          (vl-jp-reportcard reportcard
                                            :no-html config.no-html)
                          (vl-print ",\"locations\":")
                          (vl-jp-design-locations lintresult.design)
                          (vl-println "}"))
            :name write-warnings-json))
    (state
       (cwtime
            (with-ps-file "vl-locations.json"
                          (vl-print "{\"locations\":")
                          (vl-jp-design-locations lintresult.design)
                          (vl-println "}"))
            :name write-locations-json))
    (state
      (cwtime (with-ps-file
                   "vl-ifdefs.txt"
                   (vl-print-ifdef-report-main loadresult.ifdefmap))
              :name write-ifdef-report))
    (state
     (cwtime
         (with-ps-file
              "vl-ifdef-usage.json"
              (vl-jp-definfo loadresult.defines
                             loadresult.ifdefmap loadresult.defmap))
         :name write-ifdef-usage.json))
    (state
       (cwtime
            (with-ps-file "vl-warnings-suppressed.json"
                          (vl-print "{\"warnings\":")
                          (vl-jp-reportcard suppressed)
                          (vl-print ",\"locations\":")
                          (vl-jp-design-locations lintresult.design)
                          (vl-println "}"))
            :name write-warnings-json)))
   state)))

Theorem: state-p1-of-vl-lint-report

(defthm state-p1-of-vl-lint-report
 (implies
   (state-p1 state)
   (b* ((state (vl-lint-report config loadresult lintresult state)))
     (state-p1 state)))
 :rule-classes :rewrite)