• 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
        • Defmodules-fn
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Defmodules

Defmodules-fn

Load and simplify some modules.

Signature

(defmodules-fn loadconfig simpconfig &key (state 'state)) 
  → 
(mv trans state)

Arguments

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

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

Returns

trans — Type (vl-translation-p trans), given the guard.

state — Type (state-p1 state), given the guard.

Definitions and Theorems

Function: defmodules-fn-fn

(defun defmodules-fn-fn (loadconfig simpconfig state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (vl-loadconfig-p loadconfig)
                             (vl-simpconfig-p simpconfig))))
 (let ((__function__ 'defmodules-fn))
  (declare (ignorable __function__))
  (b*
   (((mv loadresult state)
     (xf-cwtime (vl-load loadconfig)))
    ((vl-loadresult loadresult)
     (if (vl-simpconfig->compress-p simpconfig)
         (xf-cwtime (hons-copy loadresult))
       loadresult))
    ((mv good bad)
     (xf-cwtime (vl-simplify loadresult.design simpconfig)))
    (reportcard (vl-design-origname-reportcard good))
    (-
     (vl-cw-ps-seq (vl-cw "Successfully simplified ~x0 module~s1.~%"
                          (len (vl-design->mods good))
                          (if (vl-plural-p (vl-design->mods good))
                              "s"
                            ""))
                   (vl-println "")
                   (vl-println "Warnings for successful modules:")
                   (vl-print-reportcard reportcard)
                   (vl-println "")))
    (- (fast-alist-free reportcard))
    (reportcard (vl-design-origname-reportcard bad))
    (failmods (vl-design->mods bad))
    (-
     (vl-cw-ps-seq
       (if (atom failmods)
           ps
         (vl-ps-seq (vl-cw "Failed to simplify ~x0 module~s1: "
                           (len failmods)
                           (if (vl-plural-p failmods) "s" ""))
                    (vl-print-strings-with-commas
                         (vl-modulelist->names failmods)
                         4)
                    (vl-println "")
                    (vl-println "Warnings for failed descriptions:")
                    (vl-print-reportcard reportcard)
                    (vl-println "")))))
    (- (fast-alist-free reportcard))
    (result (make-vl-translation :good good
                                 :bad bad
                                 :orig loadresult.design
                                 :filemap loadresult.filemap
                                 :defines loadresult.defines)))
   (mv result state))))

Theorem: vl-translation-p-of-defmodules-fn.trans

(defthm vl-translation-p-of-defmodules-fn.trans
  (implies (and (force (state-p state))
                (force (vl-loadconfig-p loadconfig))
                (force (vl-simpconfig-p simpconfig)))
           (b* (((mv acl2::?trans acl2::?state)
                 (defmodules-fn-fn loadconfig simpconfig state)))
             (vl-translation-p trans)))
  :rule-classes :rewrite)

Theorem: state-p1-of-defmodules-fn.state

(defthm state-p1-of-defmodules-fn.state
  (implies (and (force (state-p state))
                (force (vl-loadconfig-p loadconfig))
                (force (vl-simpconfig-p simpconfig)))
           (b* (((mv acl2::?trans acl2::?state)
                 (defmodules-fn-fn loadconfig simpconfig state)))
             (state-p1 state)))
  :rule-classes :rewrite)