• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
          • Vl-delta-p
            • Vl-warn-delta
            • Vl-starting-delta
            • Vl-free-delta
            • Dwarn
          • Vl-delta-fix
          • Make-vl-delta
          • Vl-delta-equiv
          • Change-vl-delta
          • Vl-delta->warnings
          • Vl-delta->vardecls
          • Vl-delta->modinsts
          • Vl-delta->gateinsts
          • Vl-delta->assigns
          • Vl-delta->addmods
          • Vl-delta->nf
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-delta-p

Vl-warn-delta

Add a warning to a delta.

Signature

(vl-warn-delta warning &key (delta 'delta)) → delta

Arguments

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

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

Returns

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

Usually you will want to use dwarn instead because it allows you to construct the warning inline. But, occasionally, the warning to add has already been constructed, in which case vl-warn-delta is what you want.

Definitions and Theorems

Function: vl-warn-delta-fn

(defun vl-warn-delta-fn (warning delta)
  (declare (xargs :guard (and (vl-warning-p warning)
                              (vl-delta-p delta))))
  (let ((__function__ 'vl-warn-delta))
    (declare (ignorable __function__))
    (change-vl-delta delta
                     :warnings (cons (vl-warning-fix warning)
                                     (vl-delta->warnings delta)))))

Theorem: vl-delta-p-of-vl-warn-delta

(defthm vl-delta-p-of-vl-warn-delta
  (b* ((delta (vl-warn-delta-fn warning delta)))
    (vl-delta-p delta))
  :rule-classes :rewrite)

Theorem: vl-warn-delta-fn-of-vl-warning-fix-warning

(defthm vl-warn-delta-fn-of-vl-warning-fix-warning
  (equal (vl-warn-delta-fn (vl-warning-fix warning)
                           delta)
         (vl-warn-delta-fn warning delta)))

Theorem: vl-warn-delta-fn-vl-warning-equiv-congruence-on-warning

(defthm vl-warn-delta-fn-vl-warning-equiv-congruence-on-warning
  (implies (vl-warning-equiv warning warning-equiv)
           (equal (vl-warn-delta-fn warning delta)
                  (vl-warn-delta-fn warning-equiv delta)))
  :rule-classes :congruence)

Theorem: vl-warn-delta-fn-of-vl-delta-fix-delta

(defthm vl-warn-delta-fn-of-vl-delta-fix-delta
  (equal (vl-warn-delta-fn warning (vl-delta-fix delta))
         (vl-warn-delta-fn warning delta)))

Theorem: vl-warn-delta-fn-vl-delta-equiv-congruence-on-delta

(defthm vl-warn-delta-fn-vl-delta-equiv-congruence-on-delta
  (implies (vl-delta-equiv delta delta-equiv)
           (equal (vl-warn-delta-fn warning delta)
                  (vl-warn-delta-fn warning delta-equiv)))
  :rule-classes :congruence)