• 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-gateinstlist

Make a list of basic binary gate instances, e.g., AND, OR, XOR, NAND, NOR, or XNOR gates.

Signature

(vl-make-binary-gateinstlist type outs 
                             as bs &key atts (loc '*vl-fakeloc*)) 
 
  → 
insts

Arguments

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

outs — Guard (vl-exprlist-p outs).

as — Guard (vl-exprlist-p as).

bs — Guard (vl-exprlist-p bs).

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

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

Returns

insts — Type (vl-gateinstlist-p insts).

Definitions and Theorems

Function: vl-make-binary-gateinstlist-fn

(defun vl-make-binary-gateinstlist-fn (type outs as bs atts loc)
  (declare (xargs :guard (and (vl-gatetype-p type)
                              (vl-exprlist-p outs)
                              (vl-exprlist-p as)
                              (vl-exprlist-p bs)
                              (vl-atts-p atts)
                              (vl-location-p loc))))
  (declare (xargs :guard (and (member-eq type
                                         (list :vl-and :vl-nand
                                               :vl-nor :vl-or
                                               :vl-xor :vl-xnor))
                              (same-lengthp outs as)
                              (same-lengthp outs bs))))
  (let ((__function__ 'vl-make-binary-gateinstlist))
    (declare (ignorable __function__))
    (if (atom outs)
        nil
      (cons (vl-make-binary-gateinst type (car outs)
                                     (car as)
                                     (car bs)
                                     :atts atts
                                     :loc loc)
            (vl-make-binary-gateinstlist type (cdr outs)
                                         (cdr as)
                                         (cdr bs)
                                         :atts atts
                                         :loc loc)))))

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

(defthm vl-gateinstlist-p-of-vl-make-binary-gateinstlist
  (b*
   ((insts
         (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))
   (vl-gateinstlist-p insts))
  :rule-classes :rewrite)

Theorem: len-of-vl-make-binary-gateinstlist

(defthm len-of-vl-make-binary-gateinstlist
  (equal (len (vl-make-binary-gateinstlist type outs as bs
                                           :atts atts
                                           :loc loc))
         (len outs)))

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

(defthm vl-make-binary-gateinstlist-fn-of-vl-gatetype-fix-type
  (equal (vl-make-binary-gateinstlist-fn (vl-gatetype-fix type)
                                         outs as bs atts loc)
         (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))

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

(defthm
 vl-make-binary-gateinstlist-fn-vl-gatetype-equiv-congruence-on-type
 (implies
  (vl-gatetype-equiv type type-equiv)
  (equal
   (vl-make-binary-gateinstlist-fn type outs as bs atts loc)
   (vl-make-binary-gateinstlist-fn type-equiv outs as bs atts loc)))
 :rule-classes :congruence)

Theorem: vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-outs

(defthm vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-outs
  (equal (vl-make-binary-gateinstlist-fn type (vl-exprlist-fix outs)
                                         as bs atts loc)
         (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))

Theorem: vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-outs

(defthm
 vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-outs
 (implies
  (vl-exprlist-equiv outs outs-equiv)
  (equal
   (vl-make-binary-gateinstlist-fn type outs as bs atts loc)
   (vl-make-binary-gateinstlist-fn type outs-equiv as bs atts loc)))
 :rule-classes :congruence)

Theorem: vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-as

(defthm vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-as
 (equal
      (vl-make-binary-gateinstlist-fn type outs (vl-exprlist-fix as)
                                      bs atts loc)
      (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))

Theorem: vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-as

(defthm
  vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-as
 (implies
  (vl-exprlist-equiv as as-equiv)
  (equal
   (vl-make-binary-gateinstlist-fn type outs as bs atts loc)
   (vl-make-binary-gateinstlist-fn type outs as-equiv bs atts loc)))
 :rule-classes :congruence)

Theorem: vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-bs

(defthm vl-make-binary-gateinstlist-fn-of-vl-exprlist-fix-bs
 (equal
   (vl-make-binary-gateinstlist-fn type outs as (vl-exprlist-fix bs)
                                   atts loc)
   (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))

Theorem: vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-bs

(defthm
  vl-make-binary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-bs
 (implies
  (vl-exprlist-equiv bs bs-equiv)
  (equal
   (vl-make-binary-gateinstlist-fn type outs as bs atts loc)
   (vl-make-binary-gateinstlist-fn type outs as bs-equiv atts loc)))
 :rule-classes :congruence)

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

(defthm vl-make-binary-gateinstlist-fn-of-vl-atts-fix-atts
 (equal
  (vl-make-binary-gateinstlist-fn type outs as bs (vl-atts-fix atts)
                                  loc)
  (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))

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

(defthm
    vl-make-binary-gateinstlist-fn-vl-atts-equiv-congruence-on-atts
 (implies
  (vl-atts-equiv atts atts-equiv)
  (equal
   (vl-make-binary-gateinstlist-fn type outs as bs atts loc)
   (vl-make-binary-gateinstlist-fn type outs as bs atts-equiv loc)))
 :rule-classes :congruence)

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

(defthm vl-make-binary-gateinstlist-fn-of-vl-location-fix-loc
  (equal (vl-make-binary-gateinstlist-fn
              type
              outs as bs atts (vl-location-fix loc))
         (vl-make-binary-gateinstlist-fn type outs as bs atts loc)))

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

(defthm
 vl-make-binary-gateinstlist-fn-vl-location-equiv-congruence-on-loc
 (implies
  (vl-location-equiv loc loc-equiv)
  (equal
   (vl-make-binary-gateinstlist-fn type outs as bs atts loc)
   (vl-make-binary-gateinstlist-fn type outs as bs atts loc-equiv)))
 :rule-classes :congruence)