• Top
  • Documentation
  • Books
  • 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-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-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-default-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • Svl
    • X86isa
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-load-summary

Vl-default-load-summary

Signature

(vl-default-load-summary config result) → nil

Arguments

config — Guard (vl-loadconfig-p config).

result — Guard (vl-loadresult-p result).

Definitions and Theorems

Function: vl-default-load-summary

(defun vl-default-load-summary (config result)
 (declare (xargs :guard (and (vl-loadconfig-p config)
                             (vl-loadresult-p result))))
 (declare (ignore config))
 (let ((__function__ 'vl-default-load-summary))
   (declare (ignorable __function__))
   (b*
    (((vl-loadresult result) result)
     ((vl-design result.design)
      result.design)
     (- (cw "Load Summary:"))
     (- (cw " - ~x0 modules.~%"
            (len result.design.mods)))
     (- (cw " - ~x0 interfaces.~%"
            (len result.design.interfaces)))
     (- (cw " - ~x0 packages.~%"
            (len result.design.packages)))
     (- (cw " - ~x0 programs.~%"
            (len result.design.programs)))
     (- (cw " - ~x0 configs.~%"
            (len result.design.configs)))
     (- (cw " - ~x0 user-defined primitives.~%"
            (len result.design.udps)))
     (regular-warnings
          (mergesort (vl-design-flat-warnings result.design)))
     (all-warnings
          (mergesort (append-without-guard result.design.warnings
                                           regular-warnings)))
     (- (or (not all-warnings)
            (cw "Total number of warnings: ~x0.~%"
                (len all-warnings))))
     (floating-warnings (mergesort result.design.warnings))
     (- (or (not floating-warnings)
            (vl-cw-ps-seq (vl-ps-update-autowrap-col 68)
                          (vl-cw "~x0 floating warning~s1:~%"
                                 (len floating-warnings)
                                 (if (vl-plural-p floating-warnings)
                                     "s"
                                   ""))
                          (vl-print-warnings floating-warnings)
                          (vl-println ""))))
     (multidef-warnings (vl-keep-warnings '(:vl-warn-multidef)
                                          regular-warnings))
     (- (or (not multidef-warnings)
            (vl-cw-ps-seq
                 (vl-ps-update-autowrap-col 68)
                 (vl-cw "~x0 multiply defined module warning~s1:~%"
                        (len multidef-warnings)
                        (if (vl-plural-p multidef-warnings)
                            "s"
                          ""))
                 (vl-print-warnings multidef-warnings)
                 (vl-println "")))))
    nil)))