• 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-binary-gateinst

Make a basic binary gate instance, e.g., an AND, OR, XOR, NAND, NOR, or XNOR gate.

Signature

(vl-make-binary-gateinst type out a b &key atts (loc '*vl-fakeloc*)) 
  → 
inst

Arguments

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

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

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

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

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-binary-gateinst-fn

(defun vl-make-binary-gateinst-fn (type out a b atts loc)
 (declare (xargs :guard (and (vl-gatetype-p type)
                             (vl-expr-p out)
                             (vl-expr-p a)
                             (vl-expr-p b)
                             (vl-atts-p atts)
                             (vl-location-p loc))))
 (declare (xargs :guard (member-eq type
                                   (list :vl-and :vl-nand
                                         :vl-nor :vl-or
                                         :vl-xor :vl-xnor))))
 (let ((__function__ 'vl-make-binary-gateinst))
  (declare (ignorable __function__))
  (prog2$ (or (and (equal (vl-expr->finalwidth out) 1)
                   (equal (vl-expr->finalwidth a) 1)
                   (equal (vl-expr->finalwidth b) 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 a)
                                             :dir :vl-input)
                           (make-vl-plainarg :expr (vl-expr-fix b)
                                             :dir :vl-input))
               :atts atts
               :loc loc))))

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

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

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

(defthm vl-make-binary-gateinst-fn-of-vl-gatetype-fix-type
  (equal (vl-make-binary-gateinst-fn (vl-gatetype-fix type)
                                     out a b atts loc)
         (vl-make-binary-gateinst-fn type out a b atts loc)))

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

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

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

(defthm vl-make-binary-gateinst-fn-of-vl-expr-fix-out
  (equal (vl-make-binary-gateinst-fn type (vl-expr-fix out)
                                     a b atts loc)
         (vl-make-binary-gateinst-fn type out a b atts loc)))

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

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

Theorem: vl-make-binary-gateinst-fn-of-vl-expr-fix-a

(defthm vl-make-binary-gateinst-fn-of-vl-expr-fix-a
  (equal (vl-make-binary-gateinst-fn type out (vl-expr-fix a)
                                     b atts loc)
         (vl-make-binary-gateinst-fn type out a b atts loc)))

Theorem: vl-make-binary-gateinst-fn-vl-expr-equiv-congruence-on-a

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

Theorem: vl-make-binary-gateinst-fn-of-vl-expr-fix-b

(defthm vl-make-binary-gateinst-fn-of-vl-expr-fix-b
  (equal (vl-make-binary-gateinst-fn type out a (vl-expr-fix b)
                                     atts loc)
         (vl-make-binary-gateinst-fn type out a b atts loc)))

Theorem: vl-make-binary-gateinst-fn-vl-expr-equiv-congruence-on-b

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

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

(defthm vl-make-binary-gateinst-fn-of-vl-atts-fix-atts
  (equal (vl-make-binary-gateinst-fn type out a b (vl-atts-fix atts)
                                     loc)
         (vl-make-binary-gateinst-fn type out a b atts loc)))

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

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

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

(defthm vl-make-binary-gateinst-fn-of-vl-location-fix-loc
  (equal (vl-make-binary-gateinst-fn
              type out a b atts (vl-location-fix loc))
         (vl-make-binary-gateinst-fn type out a b atts loc)))

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

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