• 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-design->sv-design

Vl-design->svex-modalist

Translate a simplified VL design into an SVEX modalist.

Signature

(vl-design->svex-modalist x &key (config '*vl-default-simpconfig*)) 
  → 
(mv reportcard svexmods)

Arguments

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

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

Returns

reportcard — Type (vl-reportcard-p reportcard).

svexmods — Type (and (sv::modalist-p svexmods) (sv::svarlist-addr-p (sv::modalist-vars svexmods))) .

This expects the input to be a VL modulelist that is unparametrized, with resolved selects/ranges, always blocks processed into flop/latch primitives, and all expressions sized. A suitable series of transforms is implemented in vl-simplify-sv.

See vl-hierarchy-sv-translation for discussion of our approach to this translation.

Definitions and Theorems

Function: vl-design->svex-modalist-fn

(defun vl-design->svex-modalist-fn (x config)
 (declare (xargs :guard (and (vl-design-p x)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-design->svex-modalist))
   (declare (ignorable __function__))
   (b* (((vl-design x) (vl-design-fix x))
        ((local-stobjs elabindex)
         (mv reportcard modalist elabindex))
        (elabindex (vl-elabindex-init x))
        ((mv reportcard1 modalist elabindex)
         (vl-modulelist->svex-modalist x.mods elabindex config nil))
        ((mv reportcard2 modalist elabindex)
         (vl-interfacelist->svex-modalist
              x.interfaces elabindex config modalist))
        (reportcard
             (vl-clean-reportcard
                  (append-without-guard reportcard1 reportcard2))))
     (vl-scopestacks-free)
     (mv reportcard modalist elabindex))))

Theorem: vl-reportcard-p-of-vl-design->svex-modalist.reportcard

(defthm vl-reportcard-p-of-vl-design->svex-modalist.reportcard
  (b* (((mv ?reportcard ?svexmods)
        (vl-design->svex-modalist-fn x config)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-design->svex-modalist.svexmods

(defthm return-type-of-vl-design->svex-modalist.svexmods
  (b* (((mv ?reportcard ?svexmods)
        (vl-design->svex-modalist-fn x config)))
    (and (sv::modalist-p svexmods)
         (sv::svarlist-addr-p (sv::modalist-vars svexmods))))
  :rule-classes :rewrite)

Theorem: vl-design->svex-modalist-fn-of-vl-design-fix-x

(defthm vl-design->svex-modalist-fn-of-vl-design-fix-x
  (equal (vl-design->svex-modalist-fn (vl-design-fix x)
                                      config)
         (vl-design->svex-modalist-fn x config)))

Theorem: vl-design->svex-modalist-fn-vl-design-equiv-congruence-on-x

(defthm vl-design->svex-modalist-fn-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-design->svex-modalist-fn x config)
                  (vl-design->svex-modalist-fn x-equiv config)))
  :rule-classes :congruence)

Theorem: vl-design->svex-modalist-fn-of-vl-simpconfig-fix-config

(defthm vl-design->svex-modalist-fn-of-vl-simpconfig-fix-config
  (equal (vl-design->svex-modalist-fn x (vl-simpconfig-fix config))
         (vl-design->svex-modalist-fn x config)))

Theorem: vl-design->svex-modalist-fn-vl-simpconfig-equiv-congruence-on-config

(defthm
 vl-design->svex-modalist-fn-vl-simpconfig-equiv-congruence-on-config
 (implies (vl-simpconfig-equiv config config-equiv)
          (equal (vl-design->svex-modalist-fn x config)
                 (vl-design->svex-modalist-fn x config-equiv)))
 :rule-classes :congruence)