• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
          • Make-implicit-wires
          • Resolve-indexing
          • Origexprs
          • Argresolve
          • Portdecl-sign
          • Designwires
          • 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
        • Latchcode
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • 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-nonatom :op :vl-unary-bitnot
                                   :args (list in1)))
       (:vl-udp-? |*sized-1'b1*|)
       (:vl-udp-b
            (make-vl-nonatom
                 :op :vl-binary-bitor
                 :args (list in1
                             (make-vl-nonatom :op :vl-unary-bitnot
                                              :args (list 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-nonatom :op :vl-binary-bitand
                        :args (list match-expr1 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)