• 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-simpconfig
          • Vl-hierarchy-sv-translation
          • Vl-expr-svex-translation
          • Vl-design->svex-modalist
          • Vl-svstmt
        • Vl-to-sv-main
        • Vl-simplify-sv
        • Vl-user-paramsettings->unparam-names
        • Vl-user-paramsettings->modnames
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-to-svex

Vl-design->sv-design

Turn a VL design into an SVEX hierarchical design.

Signature

(vl-design->sv-design topmod x config) 
  → 
(mv err design good bad)

Arguments

topmod — Guard (stringp topmod).

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

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

Returns

design — Type (sv::design-p design).

good — Type (vl-design-p good).

bad — Type (vl-design-p bad).

Definitions and Theorems

Function: vl-design->sv-design

(defun vl-design->sv-design (topmod x config)
  (declare (xargs :guard (and (stringp topmod)
                              (vl-design-p x)
                              (vl-simpconfig-p config))))
  (let ((__function__ 'vl-design->sv-design))
    (declare (ignorable __function__))
    (b* (((mv err modalist good bad)
          (vl-to-sv-main (list topmod) x config))
         (design (sv::make-design :modalist modalist
                                  :top topmod)))
      (mv err design good bad))))

Theorem: design-p-of-vl-design->sv-design.design

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

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

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

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

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

Theorem: modalist-addr-p-of-vl-design->sv-design

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

Subtopics

Vl-simpconfig

Options for how to simplify Verilog modules.

Vl-hierarchy-sv-translation

Discussion of the strategy for translating VL modules (and structs, interfaces, etc.) to SV modules.

Vl-expr-svex-translation

Compilation from (sized) vl expressions into sv::svex expressions.

Vl-design->svex-modalist

Translate a simplified VL design into an SVEX modalist.

Vl-svstmt

Discussion of creating svex assignments from combinational/latch-style always blocks.