• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
        • *vl-1-bit-approx-mux*
        • *vl-1-bit-mux*
        • Nedgeflop
        • Vl-primitive-mkport
        • *vl-1-bit-assign*
        • *vl-1-bit-zmux*
        • Vl-primitive-mkwire
        • *vl-1-bit-bufif1*
        • *vl-1-bit-bufif0*
        • *vl-1-bit-delay-1*
        • *vl-1-bit-ceq*
        • *vl-1-bit-buf*
        • *vl-1-bit-rcmos*
        • *vl-1-bit-latch*
        • *vl-1-bit-cmos*
        • *vl-1-bit-power*
        • *vl-1-bit-rpmos*
        • *vl-1-bit-rnmos*
        • *vl-1-bit-pmos*
        • *vl-1-bit-nmos*
        • *vl-1-bit-ground*
        • *vl-1-bit-tranif1*
        • *vl-1-bit-tranif0*
        • *vl-1-bit-rtranif1*
        • *vl-1-bit-rtranif0*
        • *vl-1-bit-rtran*
        • *vl-1-bit-tran*
        • *vl-1-bit-notif1*
        • *vl-1-bit-notif0*
        • *vl-1-bit-and*
        • *vl-1-bit-xor*
        • *vl-1-bit-xnor*
        • *vl-1-bit-pullup*
        • *vl-1-bit-pulldown*
        • *vl-1-bit-or*
        • *vl-1-bit-not*
        • *vl-1-bit-nor*
        • *vl-1-bit-nand*
        • *vl-1-bit-z*
        • *vl-1-bit-x*
        • *vl-1-bit-t*
        • *vl-1-bit-f*
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Primitives

Vl-primitive-mkport

Convenient way to generate a port for a primitive.

Signature

(vl-primitive-mkport name dir) 
  → 
(mv expr port portdecl vardecl)

Arguments

name — Guard (stringp name).

dir — Guard (vl-direction-p dir).

Returns

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

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

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

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

This is like vl-occform-mkport, but our primitives are all one-bit things so we leave out the ranges to make them prettier.

Definitions and Theorems

Function: vl-primitive-mkport

(defun vl-primitive-mkport (name dir)
  (declare (xargs :guard (and (stringp name)
                              (vl-direction-p dir))))
  (let ((__function__ 'vl-primitive-mkport))
    (declare (ignorable __function__))
    (b* ((name (hons-copy (string-fix name)))
         (expr (vl-idexpr name 1 :vl-unsigned))
         (port (make-vl-regularport :name name
                                    :expr expr
                                    :loc *vl-fakeloc*))
         (portdecl (make-vl-portdecl :name name
                                     :type *vl-plain-old-wire-type*
                                     :dir dir
                                     :loc *vl-fakeloc*))
         (vardecl (make-vl-vardecl :name name
                                   :type *vl-plain-old-wire-type*
                                   :nettype :vl-wire
                                   :loc *vl-fakeloc*
                                   :atts '(("VL_PORT_IMPLICIT")))))
      (mv expr port portdecl vardecl))))

Theorem: vl-expr-p-of-vl-primitive-mkport.expr

(defthm vl-expr-p-of-vl-primitive-mkport.expr
  (b* (((mv ?expr ?port ?portdecl ?vardecl)
        (vl-primitive-mkport name dir)))
    (vl-expr-p expr))
  :rule-classes :rewrite)

Theorem: vl-port-p-of-vl-primitive-mkport.port

(defthm vl-port-p-of-vl-primitive-mkport.port
  (b* (((mv ?expr ?port ?portdecl ?vardecl)
        (vl-primitive-mkport name dir)))
    (vl-port-p port))
  :rule-classes :rewrite)

Theorem: vl-portdecl-p-of-vl-primitive-mkport.portdecl

(defthm vl-portdecl-p-of-vl-primitive-mkport.portdecl
  (b* (((mv ?expr ?port ?portdecl ?vardecl)
        (vl-primitive-mkport name dir)))
    (vl-portdecl-p portdecl))
  :rule-classes :rewrite)

Theorem: vl-vardecl-p-of-vl-primitive-mkport.vardecl

(defthm vl-vardecl-p-of-vl-primitive-mkport.vardecl
  (b* (((mv ?expr ?port ?portdecl ?vardecl)
        (vl-primitive-mkport name dir)))
    (vl-vardecl-p vardecl))
  :rule-classes :rewrite)

Theorem: vl-primitive-mkport-of-str-fix-name

(defthm vl-primitive-mkport-of-str-fix-name
  (equal (vl-primitive-mkport (str-fix name) dir)
         (vl-primitive-mkport name dir)))

Theorem: vl-primitive-mkport-streqv-congruence-on-name

(defthm vl-primitive-mkport-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-primitive-mkport name dir)
                  (vl-primitive-mkport name-equiv dir)))
  :rule-classes :congruence)

Theorem: vl-primitive-mkport-of-vl-direction-fix-dir

(defthm vl-primitive-mkport-of-vl-direction-fix-dir
  (equal (vl-primitive-mkport name (vl-direction-fix dir))
         (vl-primitive-mkport name dir)))

Theorem: vl-primitive-mkport-vl-direction-equiv-congruence-on-dir

(defthm vl-primitive-mkport-vl-direction-equiv-congruence-on-dir
  (implies (vl-direction-equiv dir dir-equiv)
           (equal (vl-primitive-mkport name dir)
                  (vl-primitive-mkport name dir-equiv)))
  :rule-classes :congruence)