		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Run-vl-lint-main

Signature
(run-vl-lint-main design config) → result
Arguments: design — Guard (vl-design-p design).; config — Guard (vl-lintconfig-p config).
Returns: result — Type (vl-lintresult-p result).

Definitions and Theorems

Function: run-vl-lint-main

(defun run-vl-lint-main (design config)
 (declare (xargs :guard (and (vl-design-p design)
                             (vl-lintconfig-p config))))
 (let ((__function__ 'run-vl-lint-main))
  (declare (ignorable __function__))
  (b*
   (((vl-lintconfig config) config)
    (design-orig design)
    (- (vl-lint-suppress-large-integer-problems t))
    (simpconfig (change-vl-simpconfig *vl-default-simpconfig*
                                      :sv-simplify nil
                                      :elab-limit config.elab-limit
                                      :sc-limit config.stmt-limit))
    (design (vl-annotate-design design simpconfig))
    (design
      (xf-cwtime
           (vl-design-drop-user-submodules design config.dropmods)))
    (design0
       (vl-design-remove-unnecessary-modules config.topmods design))
    (design
     (xf-cwtime
      (vl-design-check-globalparams design config.global-packages)))
    (design (xf-cwtime (vl-design-duplicate-detect design)))
    (design (xf-cwtime (vl-design-alwaysstyle design)))
    (design (xf-cwtime (vl-design-addnames design)))
    (design (xf-cwtime (vl-design-oddexpr-check design)))
    (typosp (not config.no-typo))
    (design (xf-cwtime (vl-design-lucid design
                                        :modportsp t
                                        :paramsp t
                                        :typosp typosp
                                        :generatesp nil)))
    (design (xf-cwtime (vl-design-check-namespace design)))
    (design (xf-cwtime (vl-design-check-case design)))
    (design (xf-cwtime (vl-design-duperhs-check design)))
    (design (xf-cwtime (vl-design-condcheck design)))
    (design (xf-cwtime (vl-design-leftright-check design)))
    (design (xf-cwtime (vl-design-dupeinst-check design)))
    (design (xf-cwtime (vl-centaur-seqcheck-hook design)))
    (design (xf-cwtime (vl-design-logicassign design)))
    (design (xf-cwtime (vl-design-elaborate design simpconfig)))
    ((mv design stubnames)
     (vl-design-lint-stubs design))
    (design (xf-cwtime (vl-design-dupeinst-check design)))
    (design (xf-cwtime (vl-design-lucid design
                                        :modportsp nil
                                        :paramsp nil
                                        :typosp nil
                                        :generatesp t)))
    (design (xf-cwtime (vl-design-check-selfassigns design)))
    (design (xf-cwtime (vl-design-qmarksize-check design)))
    (design (xf-cwtime (vl-design-arith-compare-check design)))
    (design (xf-cwtime (vl-design-unpacked-range-check design)))
    (sd-probs (xf-cwtime (sd-analyze-design design0)))
    ((mv reportcard modalist)
     (xf-cwtime (vl-design->svex-modalist design
                                          :config simpconfig)))
    (design (xf-cwtime (vl-apply-reportcard design reportcard)))
    (design (if (not config.no-sv-use-set)
                (xf-cwtime (vl-design-sv-use-set design modalist))
              design))
    (design
     (xf-cwtime
      (vl-design-remove-unnecessary-modules config.topmods design)))
    (design (xf-cwtime (vl-design-clean-warnings design)))
    (design (xf-cwtime (vl-design-suppress-file-warnings
                            design config.ignore-files)))
    (design (xf-cwtime (vl-design-suppress-lint-warnings design)))
    (design
        (xf-cwtime (vl-design-lint-ignoreall design config.ignore)))
    (design
     (xf-cwtime (vl-lint-apply-quiet (append stubnames config.quiet)
                                     design)))
    (sd-probs (xf-cwtime (vl-delete-sd-problems-for-modnames
                              (append stubnames config.quiet)
                              sd-probs)))
    (reportcard (xf-cwtime (vl-design-origname-reportcard design))))
   (vl-lint-suppress-large-integer-problems nil)
   (make-vl-lintresult :design design
                       :design0 design0
                       :design-orig design-orig
                       :sv-modalist modalist
                       :reportcard reportcard
                       :sd-probs sd-probs))))

Theorem: vl-lintresult-p-of-run-vl-lint-main

(defthm vl-lintresult-p-of-run-vl-lint-main
  (b* ((result (run-vl-lint-main design config)))
    (vl-lintresult-p result))
  :rule-classes :rewrite)