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

Make a list of unary (buf or not) gate instances.

Signature

(vl-make-unary-gateinstlist type 
                            outs ins &key atts (loc '*vl-fakeloc*)) 
 
  → 
insts

Arguments

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

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

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

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-unary-gateinstlist-fn

(defun vl-make-unary-gateinstlist-fn (type outs ins atts loc)
  (declare (xargs :guard (and (vl-gatetype-p type)
                              (vl-exprlist-p outs)
                              (vl-exprlist-p ins)
                              (vl-atts-p atts)
                              (vl-location-p loc))))
  (declare (xargs :guard (and (member type (list :vl-buf :vl-not))
                              (same-lengthp outs ins))))
  (let ((__function__ 'vl-make-unary-gateinstlist))
    (declare (ignorable __function__))
    (if (atom outs)
        nil
      (cons (vl-make-unary-gateinst type (car outs)
                                    (car ins)
                                    :atts atts
                                    :loc loc)
            (vl-make-unary-gateinstlist type (cdr outs)
                                        (cdr ins)
                                        :atts atts
                                        :loc loc)))))

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

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

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

(defthm vl-make-unary-gateinstlist-fn-of-vl-gatetype-fix-type
  (equal (vl-make-unary-gateinstlist-fn (vl-gatetype-fix type)
                                        outs ins atts loc)
         (vl-make-unary-gateinstlist-fn type outs ins atts loc)))

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

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

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

(defthm vl-make-unary-gateinstlist-fn-of-vl-exprlist-fix-outs
  (equal (vl-make-unary-gateinstlist-fn type (vl-exprlist-fix outs)
                                        ins atts loc)
         (vl-make-unary-gateinstlist-fn type outs ins atts loc)))

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

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

Theorem: vl-make-unary-gateinstlist-fn-of-vl-exprlist-fix-ins

(defthm vl-make-unary-gateinstlist-fn-of-vl-exprlist-fix-ins
 (equal
      (vl-make-unary-gateinstlist-fn type outs (vl-exprlist-fix ins)
                                     atts loc)
      (vl-make-unary-gateinstlist-fn type outs ins atts loc)))

Theorem: vl-make-unary-gateinstlist-fn-vl-exprlist-equiv-congruence-on-ins

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

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

(defthm vl-make-unary-gateinstlist-fn-of-vl-atts-fix-atts
 (equal
     (vl-make-unary-gateinstlist-fn type outs ins (vl-atts-fix atts)
                                    loc)
     (vl-make-unary-gateinstlist-fn type outs ins atts loc)))

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

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

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

(defthm vl-make-unary-gateinstlist-fn-of-vl-location-fix-loc
  (equal (vl-make-unary-gateinstlist-fn
              type
              outs ins atts (vl-location-fix loc))
         (vl-make-unary-gateinstlist-fn type outs ins atts loc)))

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

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