• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • 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-translation
            • Make-vl-translation
            • Change-vl-translation
            • Vl-translation-has-module
              • Honsed-vl-translation
              • Make-honsed-vl-translation
              • Vl-translation-get-esim
              • Vl-translation->orig
              • Vl-translation->good
              • Vl-translation->filemap
              • Vl-translation->defines
              • Vl-translation->bad
            • Vl-simplify
            • Defmodules-fn
          • Esim-simplify-update-fns
          • Esim-tutorial
          • Esim-vl
        • Vl2014
        • Sv
        • Vwsim
        • Fgl
        • Vl
        • Svl
        • X86isa
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Vl-translation-p

    Vl-translation-has-module

    Check whether a module was successfully translated.

    Signature
    (vl-translation-has-module modname x) → *
    Arguments
    modname — Guard (stringp modname).
    x — Guard (vl-translation-p x).

    The modname should be the desired module's name as a string, e.g., "fadd". If the module's name includes parameters, you will need to say which version you want, e.g., "adder$width=4".

    We return t only when the module was successfully translated with no "fatal" warnings. (See vl-translation-p; failed modules are found in the translation's failmods field, whereas successful modules are kept in the mods field.)

    Definitions and Theorems

    Function: vl-translation-has-module

    (defun vl-translation-has-module (modname x)
      (declare (xargs :guard (and (stringp modname)
                                  (vl-translation-p x))))
      (let ((__function__ 'vl-translation-has-module))
        (declare (ignorable __function__))
        (if (vl-find-module modname
                            (vl-design->mods (vl-translation->good x)))
            t
          nil)))