• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
        • Scopestack
        • Hid-tools
        • Filtering-by-name
        • Vl-interface-mocktype
        • Stripping-functions
        • Genblob
        • Expr-tools
        • Extract-vl-types
        • Hierarchy
          • Vl-design-toplevel
          • Vl-remove-unnecessary-elements
          • Vl-necessary-elements-transitive
          • Vl-interfacelist-everinstanced
          • Vl-dependent-elements-transitive
          • Vl-necessary-elements-direct
          • Vl-modulelist-everinstanced
          • Vl-dependent-elements-direct
          • Vl-design-deporder-modules
          • Vl-design-check-complete
          • Vl-design-upgraph
          • Immdeps
            • Immdeps-main
            • Vl-immdeps
              • Vl-immdeps-p
              • Vl-immdeps-add-error
              • Vl-immdeps-add-item
              • Vl-immdeps-add-definition
              • Vl-immdeps-add-pkgdep
              • Vl-immdeps-fix
              • Vl-immdeps-add-raw-dependency
              • Vl-immdeps-equiv
              • Make-vl-immdeps
              • Vl-immdeps->warnings
              • Vl-immdeps->deps
              • Vl-immdeps->all-okp
              • Change-vl-immdeps
            • Immdeps-top
            • Vl-immdepgraph
            • Vl-depgraph
          • Vl-design-downgraph
          • Vl-collect-dependencies
          • Vl-hierarchy-free
        • Range-tools
        • Finding-by-name
        • Stmt-tools
        • Modnamespace
        • Flat-warnings
        • Reordering-by-name
        • Datatype-tools
        • Syscalls
        • Allexprs
        • Lvalues
        • Port-tools
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-immdeps

Vl-immdeps-add-pkgdep

Safely add a dependency onto a package. If the package doesn't exist, add a warning instead of a dependency.

Signature

(vl-immdeps-add-pkgdep pkgname ans &key (ss 'ss) (ctx 'ctx)) 
  → 
new-ans

Arguments

pkgname — Guard (stringp pkgname).

ans — Guard (vl-immdeps-p ans).

ss — Guard (vl-scopestack-p ss).

ctx — Guard (any-p ctx).

Returns

new-ans — Type (vl-immdeps-p new-ans).

Definitions and Theorems

Function: vl-immdeps-add-pkgdep-fn

(defun vl-immdeps-add-pkgdep-fn (pkgname ans ss ctx)
  (declare (xargs :guard (and (stringp pkgname)
                              (vl-immdeps-p ans)
                              (vl-scopestack-p ss)
                              (any-p ctx))))
  (let ((__function__ 'vl-immdeps-add-pkgdep))
    (declare (ignorable __function__))
    (b* ((pkgname (string-fix pkgname))
         (pkg (vl-scopestack-find-package pkgname ss))
         ((unless pkg)
          (vl-immdeps-add-error
               ans
               :type :vl-missing-package
               :msg "~a0: reference to unknown package ~a1."
               :args (list ctx pkgname)
               :fatalp t))
         (ans (vl-immdeps-add-raw-dependency pkgname ans)))
      ans)))

Theorem: vl-immdeps-p-of-vl-immdeps-add-pkgdep

(defthm vl-immdeps-p-of-vl-immdeps-add-pkgdep
  (b* ((new-ans (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)))
    (vl-immdeps-p new-ans))
  :rule-classes :rewrite)

Theorem: vl-immdeps-add-pkgdep-fn-of-str-fix-pkgname

(defthm vl-immdeps-add-pkgdep-fn-of-str-fix-pkgname
  (equal (vl-immdeps-add-pkgdep-fn (str-fix pkgname)
                                   ans ss ctx)
         (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)))

Theorem: vl-immdeps-add-pkgdep-fn-streqv-congruence-on-pkgname

(defthm vl-immdeps-add-pkgdep-fn-streqv-congruence-on-pkgname
  (implies
       (streqv pkgname pkgname-equiv)
       (equal (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)
              (vl-immdeps-add-pkgdep-fn pkgname-equiv ans ss ctx)))
  :rule-classes :congruence)

Theorem: vl-immdeps-add-pkgdep-fn-of-vl-immdeps-fix-ans

(defthm vl-immdeps-add-pkgdep-fn-of-vl-immdeps-fix-ans
  (equal (vl-immdeps-add-pkgdep-fn pkgname (vl-immdeps-fix ans)
                                   ss ctx)
         (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)))

Theorem: vl-immdeps-add-pkgdep-fn-vl-immdeps-equiv-congruence-on-ans

(defthm vl-immdeps-add-pkgdep-fn-vl-immdeps-equiv-congruence-on-ans
  (implies
       (vl-immdeps-equiv ans ans-equiv)
       (equal (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)
              (vl-immdeps-add-pkgdep-fn pkgname ans-equiv ss ctx)))
  :rule-classes :congruence)

Theorem: vl-immdeps-add-pkgdep-fn-of-vl-scopestack-fix-ss

(defthm vl-immdeps-add-pkgdep-fn-of-vl-scopestack-fix-ss
 (equal (vl-immdeps-add-pkgdep-fn pkgname ans (vl-scopestack-fix ss)
                                  ctx)
        (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)))

Theorem: vl-immdeps-add-pkgdep-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
      vl-immdeps-add-pkgdep-fn-vl-scopestack-equiv-congruence-on-ss
  (implies
       (vl-scopestack-equiv ss ss-equiv)
       (equal (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)
              (vl-immdeps-add-pkgdep-fn pkgname ans ss-equiv ctx)))
  :rule-classes :congruence)

Theorem: vl-immdeps-add-pkgdep-fn-of-identity-ctx

(defthm vl-immdeps-add-pkgdep-fn-of-identity-ctx
  (equal (vl-immdeps-add-pkgdep-fn pkgname ans ss (identity ctx))
         (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)))

Theorem: vl-immdeps-add-pkgdep-fn-equal-congruence-on-ctx

(defthm vl-immdeps-add-pkgdep-fn-equal-congruence-on-ctx
  (implies
       (equal ctx ctx-equiv)
       (equal (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx)
              (vl-immdeps-add-pkgdep-fn pkgname ans ss ctx-equiv)))
  :rule-classes :congruence)