• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
        • Vl-translation-p
        • Vl-simplify
          • Vl-warn-problem-modulelist
          • Propagating-errors
          • Vl-simpconfig
          • Vl-simplify-main
            • Vl-simplify-maybe-clean-params
          • Vl-warn-problem-module
          • Vl-design-problem-mods
        • Defmodules-fn
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-simplify

Vl-simplify-main

Core transformation sequence for using VL to generate E modules.

Signature

(vl-simplify-main design config) → (mv good bad)

Arguments

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

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

Returns

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

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

Definitions and Theorems

Function: vl-simplify-main

(defun vl-simplify-main (design config)
 (declare (xargs :guard (and (vl-design-p design)
                             (vl-simpconfig-p config))))
 (let ((__function__ 'vl-simplify-main))
  (declare (ignorable __function__))
  (b*
   (((vl-simpconfig config) config)
    (good (vl-design-fix design))
    (bad (make-vl-design))
    (- (cw "Simplifying ~x0 modules.~%"
           (len (vl-design->mods good))))
    (good
      (xf-cwtime (vl-design-problem-mods good config.problem-mods)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-expand-functions good)))
    (good (vl-simplify-maybe-clean-params good config))
    (good (xf-cwtime (vl-design-lvaluecheck good)))
    (good (xf-cwtime (vl-design-check-reasonable good)))
    (good (xf-cwtime (vl-design-check-complete good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-unparameterize good)))
    (good (xf-cwtime (vl-design-post-unparam-hook good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-rangeresolve good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-selresolve good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good
       (xf-cwtime (vl-design-stmtrewrite good config.unroll-limit)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-oprewrite good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-exprsize good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-wildelim good)))
    (good (xf-cwtime (vl-design-always-backend good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-elim-unused-vars good)))
    (good (xf-cwtime (vl-design-drop-blankports good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-delayredux good)))
    (good (xf-cwtime (vl-design-split good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (- (vl-gc))
    (good (xf-cwtime (vl-design-replicate good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-blankargs good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-trunc good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-optimize good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-occform good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (- (vl-gc))
    (good (xf-cwtime (vl-design-weirdint-elim good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-gatesplit good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-gate-elim good)))
    (good (xf-cwtime (vl-design-addinstnames good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-elim-supplies good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-optimize good)))
    (good (xf-cwtime (vl-design-pre-toe-hook good)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    ((mv good bad)
     (xf-cwtime (vl-design-to-e good bad)))
    ((mv good bad)
     (xf-cwtime (vl-design-propagate-errors* good bad)))
    (good (xf-cwtime (vl-design-clean-warnings good)))
    (bad (xf-cwtime (vl-design-clean-warnings bad))))
   (mv good bad))))

Theorem: vl-design-p-of-vl-simplify-main.good

(defthm vl-design-p-of-vl-simplify-main.good
  (b* (((mv ?good ?bad)
        (vl-simplify-main design config)))
    (vl-design-p good))
  :rule-classes :rewrite)

Theorem: vl-design-p-of-vl-simplify-main.bad

(defthm vl-design-p-of-vl-simplify-main.bad
  (b* (((mv ?good ?bad)
        (vl-simplify-main design config)))
    (vl-design-p bad))
  :rule-classes :rewrite)

Subtopics

Vl-simplify-maybe-clean-params

Wrapper to hide the case split for optional clean-params.