• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
        • Unparameterization
        • Elaborate
        • Addnames
        • Annotate
          • Increment-elim
          • Make-implicit-wires
          • Basic-bind-elim
          • Argresolve
          • Basicsanity
          • Portdecl-sign
          • Enum-names
          • Port-resolve
          • Udp-elim
            • Vl-udp-vardecls-from-portdecls
            • Vl-udps-to-modules
            • Vl-udpline-match-expr
            • Vl-combinational-udptable-synth
            • Vl-udptable-assignrhs
            • Vl-udp-to-module
            • Vl-udp-vardecl-from-portdecl
            • Vl-design-udp-elim
          • Vl-annotate-design
          • Vl-annotate-module
        • Clean-warnings
        • Eliminitial
        • Custom-transform-hooks
        • Problem-modules
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Udp-elim

Vl-udpline-match-expr

Signature

(vl-udpline-match-expr inexprs entries warnings) 
  → 
(mv okp warnings match-expr)

Arguments

inexprs — Expressions for the input variables, in order.
    Guard (vl-exprlist-p inexprs).

entries — Inputs from the UDP table, in corresponding order.
    Guard (vl-udpentrylist-p entries).

warnings — Guard (vl-warninglist-p warnings).

Returns

okp — Type (booleanp okp).

warnings — Type (vl-warninglist-p warnings).

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

Definitions and Theorems

Function: vl-udpline-match-expr

(defun vl-udpline-match-expr (inexprs entries warnings)
 (declare (xargs :guard (and (vl-exprlist-p inexprs)
                             (vl-udpentrylist-p entries)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard (and (consp inexprs)
                             (same-lengthp inexprs entries))))
 (let ((__function__ 'vl-udpline-match-expr))
  (declare (ignorable __function__))
  (b*
   ((in1 (vl-expr-fix (car inexprs)))
    (entry1 (vl-udpentry-fix (car entries)))
    ((when (mbe :logic (vl-udpedge-p entry1)
                :exec (consp entry1)))
     (mv
      nil
      (fatal
       :type :vl-bad-udp-entry
       :msg
       "Expected no edges in combinational UDP lines, but found ~a0."
       :args (list entry1))
      |*sized-1'bx*|))
    ((unless (or (eq entry1 :vl-udp-0)
                 (eq entry1 :vl-udp-1)
                 (eq entry1 :vl-udp-?)
                 (eq entry1 :vl-udp-b)))
     (mv
      nil
      (fatal
       :type :vl-bad-udp-entry
       :msg
       "UDP levels other than 0/1/?/b are not supported, but found ~a0."
       :args (list entry1))
      |*sized-1'bx*|))
    (match-expr1
     (case
      entry1 (:vl-udp-1 in1)
      (:vl-udp-0 (make-vl-unary :op :vl-unary-bitnot
                                :arg in1))
      (:vl-udp-? |*sized-1'b1*|)
      (:vl-udp-b
          (make-vl-binary :op :vl-binary-bitor
                          :left in1
                          :right (make-vl-unary :op :vl-unary-bitnot
                                                :arg in1)))))
    ((when (atom (cdr inexprs)))
     (mv t (ok) match-expr1))
    ((mv okp warnings rest-expr)
     (vl-udpline-match-expr (cdr inexprs)
                            (cdr entries)
                            warnings))
    ((unless okp)
     (mv nil warnings rest-expr)))
   (mv t warnings
       (make-vl-binary :op :vl-binary-bitand
                       :left match-expr1
                       :right rest-expr)))))

Theorem: booleanp-of-vl-udpline-match-expr.okp

(defthm booleanp-of-vl-udpline-match-expr.okp
  (b* (((mv ?okp ?warnings ?match-expr)
        (vl-udpline-match-expr inexprs entries warnings)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-udpline-match-expr.warnings

(defthm vl-warninglist-p-of-vl-udpline-match-expr.warnings
  (b* (((mv ?okp ?warnings ?match-expr)
        (vl-udpline-match-expr inexprs entries warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-expr-p-of-vl-udpline-match-expr.match-expr

(defthm vl-expr-p-of-vl-udpline-match-expr.match-expr
  (b* (((mv ?okp ?warnings ?match-expr)
        (vl-udpline-match-expr inexprs entries warnings)))
    (vl-expr-p match-expr))
  :rule-classes :rewrite)