• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
        • Scopestack
        • Filtering-by-name
        • Vl-namefactory
        • Substitution
        • Allexprs
        • Hid-tools
        • Vl-consteval
        • Range-tools
        • Lvalexprs
        • Hierarchy
        • Finding-by-name
        • Expr-tools
        • Expr-slicing
        • Stripping-functions
        • Stmt-tools
        • Modnamespace
        • Vl-parse-expr-from-str
        • Welltyped
        • Reordering-by-name
        • Flat-warnings
        • Genblob
        • Expr-building
          • Vl-make-binary-gateinstlist
          • Vl-make-binary-gateinst
          • Vl-make-unary-gateinstlist
          • Vl-make-bitselect
          • Vl-make-unary-gateinst
          • Vl-make-partselect
          • Vl-make-msb-to-lsb-bitselects
          • Vl-make-list-of-bitselects
          • Vl-default-n-bit-expr
        • Datatype-tools
        • Syscalls
        • Relocate
        • Expr-cleaning
        • Namemangle
        • Caremask
        • Port-tools
        • Lvalues
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Expr-building

Vl-make-unary-gateinst

Make a unary (buf or not) gate instance.

Signature

(vl-make-unary-gateinst type out in &key atts (loc '*vl-fakeloc*)) 
  → 
inst

Arguments

type — Guard (vl-gatetype-p type).

out — Guard (vl-expr-p out).

in — Guard (vl-expr-p in).

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

loc — Guard (vl-location-p loc).

Returns

inst — Type (vl-gateinst-p inst).

Definitions and Theorems

Function: vl-make-unary-gateinst-fn

(defun vl-make-unary-gateinst-fn (type out in atts loc)
 (declare (xargs :guard (and (vl-gatetype-p type)
                             (vl-expr-p out)
                             (vl-expr-p in)
                             (vl-atts-p atts)
                             (vl-location-p loc))))
 (declare (xargs :guard (member type (list :vl-buf :vl-not))))
 (let ((__function__ 'vl-make-unary-gateinst))
  (declare (ignorable __function__))
  (progn$ (or (and (equal (vl-expr->finalwidth out) 1)
                   (equal (vl-expr->finalwidth in) 1))
              (raise "Expected expressions of width 1."))
          (make-vl-gateinst
               :type type
               :args (list (make-vl-plainarg :expr (vl-expr-fix out)
                                             :dir :vl-output)
                           (make-vl-plainarg :expr (vl-expr-fix in)
                                             :dir :vl-input))
               :atts atts
               :loc loc))))

Theorem: vl-gateinst-p-of-vl-make-unary-gateinst

(defthm vl-gateinst-p-of-vl-make-unary-gateinst
  (b* ((inst (vl-make-unary-gateinst-fn type out in atts loc)))
    (vl-gateinst-p inst))
  :rule-classes :rewrite)

Theorem: vl-make-unary-gateinst-fn-of-vl-gatetype-fix-type

(defthm vl-make-unary-gateinst-fn-of-vl-gatetype-fix-type
  (equal (vl-make-unary-gateinst-fn (vl-gatetype-fix type)
                                    out in atts loc)
         (vl-make-unary-gateinst-fn type out in atts loc)))

Theorem: vl-make-unary-gateinst-fn-vl-gatetype-equiv-congruence-on-type

(defthm
     vl-make-unary-gateinst-fn-vl-gatetype-equiv-congruence-on-type
 (implies
     (vl-gatetype-equiv type type-equiv)
     (equal (vl-make-unary-gateinst-fn type out in atts loc)
            (vl-make-unary-gateinst-fn type-equiv out in atts loc)))
 :rule-classes :congruence)

Theorem: vl-make-unary-gateinst-fn-of-vl-expr-fix-out

(defthm vl-make-unary-gateinst-fn-of-vl-expr-fix-out
  (equal (vl-make-unary-gateinst-fn type (vl-expr-fix out)
                                    in atts loc)
         (vl-make-unary-gateinst-fn type out in atts loc)))

Theorem: vl-make-unary-gateinst-fn-vl-expr-equiv-congruence-on-out

(defthm vl-make-unary-gateinst-fn-vl-expr-equiv-congruence-on-out
 (implies
     (vl-expr-equiv out out-equiv)
     (equal (vl-make-unary-gateinst-fn type out in atts loc)
            (vl-make-unary-gateinst-fn type out-equiv in atts loc)))
 :rule-classes :congruence)

Theorem: vl-make-unary-gateinst-fn-of-vl-expr-fix-in

(defthm vl-make-unary-gateinst-fn-of-vl-expr-fix-in
  (equal (vl-make-unary-gateinst-fn type out (vl-expr-fix in)
                                    atts loc)
         (vl-make-unary-gateinst-fn type out in atts loc)))

Theorem: vl-make-unary-gateinst-fn-vl-expr-equiv-congruence-on-in

(defthm vl-make-unary-gateinst-fn-vl-expr-equiv-congruence-on-in
 (implies
     (vl-expr-equiv in in-equiv)
     (equal (vl-make-unary-gateinst-fn type out in atts loc)
            (vl-make-unary-gateinst-fn type out in-equiv atts loc)))
 :rule-classes :congruence)

Theorem: vl-make-unary-gateinst-fn-of-vl-atts-fix-atts

(defthm vl-make-unary-gateinst-fn-of-vl-atts-fix-atts
  (equal (vl-make-unary-gateinst-fn type out in (vl-atts-fix atts)
                                    loc)
         (vl-make-unary-gateinst-fn type out in atts loc)))

Theorem: vl-make-unary-gateinst-fn-vl-atts-equiv-congruence-on-atts

(defthm vl-make-unary-gateinst-fn-vl-atts-equiv-congruence-on-atts
 (implies
     (vl-atts-equiv atts atts-equiv)
     (equal (vl-make-unary-gateinst-fn type out in atts loc)
            (vl-make-unary-gateinst-fn type out in atts-equiv loc)))
 :rule-classes :congruence)

Theorem: vl-make-unary-gateinst-fn-of-vl-location-fix-loc

(defthm vl-make-unary-gateinst-fn-of-vl-location-fix-loc
 (equal
  (vl-make-unary-gateinst-fn type out in atts (vl-location-fix loc))
  (vl-make-unary-gateinst-fn type out in atts loc)))

Theorem: vl-make-unary-gateinst-fn-vl-location-equiv-congruence-on-loc

(defthm
      vl-make-unary-gateinst-fn-vl-location-equiv-congruence-on-loc
 (implies
     (vl-location-equiv loc loc-equiv)
     (equal (vl-make-unary-gateinst-fn type out in atts loc)
            (vl-make-unary-gateinst-fn type out in atts loc-equiv)))
 :rule-classes :congruence)