• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
        • Vl-to-sv
        • Vl-design->sv-design
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-to-svex

Vl-to-sv

Turn a VL design into an SVEX hierarchical design, with options given by a vl-simpconfig object.

Signature

(vl-to-sv x config) → (mv err modalist good bad)

Arguments

x — Guard (vl-design-p x).

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

Returns

err — An error message if any required modules had fatal errors after elaboration.

modalist — The SV sv::modalist translated from the input design.
    Type (sv::modalist-p modalist).

good — The post-elaboration VL design, except those parts that had fatal warnings.
    Type (vl-design-p good).

bad — The parts of the VL design that had fatal warnings after elaboration.
    Type (vl-design-p bad).

Definitions and Theorems

Function: vl-to-sv

(defun vl-to-sv (x config)
 (declare (xargs :guard (and (vl-design-p x)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-to-sv))
  (declare (ignorable __function__))
  (b*
   ((x (vl-design-fix x))
    ((vl-simpconfig config))
    (x (if config.already-annotated x
         (cwtime (vl-annotate-design x config))))
    (x (cwtime (vl-design-addnames x)))
    (pre-topmods
     (append
       config.pre-elab-topmods
       (vl-user-paramsettings->modnames config.user-paramsettings)))
    (post-topmods (append config.post-elab-topmods
                          (vl-user-paramsettings->unparam-names
                               config.user-paramsettings)))
    (x (if config.pre-elab-filter
           (cwtime (vl-remove-unnecessary-elements pre-topmods x))
         x))
    ((mv good bad)
     (cwtime (vl-simplify-sv x config)))
    ((vl-design good) good)
    (bad-mods
         (difference (mergesort post-topmods)
                     (mergesort (vl-modulelist->names good.mods))))
    ((when (and (not config.allow-bad-topmods)
                bad-mods))
     (cw "Reportcard for good mods:~%")
     (cw-unformatted
          (vl-reportcard-to-string (vl-design-reportcard good)))
     (cw "Reportcard for bad mods:~%")
     (cw-unformatted
          (vl-reportcard-to-string (vl-design-reportcard bad)))
     (mv
      (msg
       "The following modules were not among the good simplified ~
                  modules: ~x0~%"
       bad-mods)
      nil good bad))
    (good.mods (redundant-mergesort good.mods))
    ((unless (uniquep (vl-modulelist->names good.mods)))
     (mv (msg "Name clash -- duplicated module names: ~&0."
              (duplicated-members (vl-modulelist->names good.mods)))
         nil good bad))
    (good1 (change-vl-design good :mods good.mods))
    (good2 (if config.post-elab-filter
               (vl-remove-unnecessary-elements post-topmods good1)
             good1))
    ((mv reportcard modalist)
     (xf-cwtime (vl-design->svex-modalist good2
                                          :config config)))
    (good (vl-apply-reportcard good2 reportcard)))
   (cw "~%")
   (cw-unformatted
    "--- VL->SV Translation Report -------------------------------------------------")
   (cw "~%")
   (cw-unformatted (vl-reportcard-to-string reportcard))
   (and
     (vl-design->warnings good)
     (progn$
          (cw "Warnings for the top-level design:~%")
          (cw-unformatted
               (vl-warnings-to-string (vl-design->warnings good)))))
   (cw-unformatted
    "-------------------------------------------------------------------------------")
   (cw "~%~%")
   (and
    bad-mods
    (progn$
     (cw "Reportcard for bad mods:~%")
     (cw-unformatted
          (vl-reportcard-to-string (vl-design-reportcard bad)))
     (cw-unformatted
      "-------------------------------------------------------------------------------")
     (cw "~%~%")))
   (mv nil modalist good bad))))

Theorem: modalist-p-of-vl-to-sv.modalist

(defthm modalist-p-of-vl-to-sv.modalist
  (b* (((mv ?err ?modalist ?good ?bad)
        (vl-to-sv x config)))
    (sv::modalist-p modalist))
  :rule-classes :rewrite)

Theorem: vl-design-p-of-vl-to-sv.good

(defthm vl-design-p-of-vl-to-sv.good
  (b* (((mv ?err ?modalist ?good ?bad)
        (vl-to-sv x config)))
    (vl-design-p good))
  :rule-classes :rewrite)

Theorem: vl-design-p-of-vl-to-sv.bad

(defthm vl-design-p-of-vl-to-sv.bad
  (b* (((mv ?err ?modalist ?good ?bad)
        (vl-to-sv x config)))
    (vl-design-p bad))
  :rule-classes :rewrite)

Theorem: modalist-addr-p-of-vl-to-sv-core

(defthm modalist-addr-p-of-vl-to-sv-core
  (b* (((mv ?err ?modalist ?good ?bad)
        (vl-to-sv x config)))
    (sv::svarlist-addr-p (sv::modalist-vars modalist))))