|
|
|---|
|
|
|
|---|
(vl-lint-report config loadresult lintresult state) → state
Function:
(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:
(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)