• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • 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-udptable-assignrhs

Signature

(vl-udptable-assignrhs inexprs lines warnings) 
  → 
(mv okp warnings expr)

Arguments

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

lines — Guard (vl-udptable-p lines).

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

Returns

okp — Type (booleanp okp).

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

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

Definitions and Theorems

Function: vl-udptable-assignrhs

(defun vl-udptable-assignrhs (inexprs lines warnings)
 (declare (xargs :guard (and (vl-exprlist-p inexprs)
                             (vl-udptable-p lines)
                             (vl-warninglist-p warnings))))
 (declare (xargs :guard (consp inexprs)))
 (let ((__function__ 'vl-udptable-assignrhs))
  (declare (ignorable __function__))
  (b*
   (((when (atom lines))
     (mv t (ok) |*sized-1'bx*|))
    ((vl-udpline line1) (car lines))
    ((when line1.current)
     (mv
      nil
      (fatal
        :type :vl-bad-udp-line
        :msg "Combinational UDP, but line has a current state? ~x0."
        :args (list line1))
      |*sized-1'bx*|))
    ((unless (same-lengthp inexprs line1.inputs))
     (mv nil
         (fatal :type :vl-bad-udp-line
                :msg "UDP has ~x0 inputs, but line has ~x1: ~x2."
                :args (list (len inexprs)
                            (len line1.inputs)
                            line1.inputs))
         |*sized-1'bx*|))
    ((mv okp warnings match-expr)
     (vl-udpline-match-expr inexprs line1.inputs warnings))
    ((unless okp)
     (mv nil warnings |*sized-1'bx*|))
    (then-expr (case line1.output (:vl-udp-0 |*sized-1'b0*|)
                     (:vl-udp-1 |*sized-1'b1*|)
                     (:vl-udp-x |*sized-1'bx*|)
                     (otherwise nil)))
    ((unless then-expr)
     (mv nil
         (fatal :type :vl-bad-udp-output
                :msg "UDP line output must be 0/1/x, but is ~x0."
                :args (list line1.output))
         |*sized-1'bx*|))
    ((mv okp warnings else-expr)
     (vl-udptable-assignrhs inexprs (cdr lines)
                            warnings))
    ((unless okp)
     (mv nil warnings |*sized-1'bx*|))
    (rhs (make-vl-qmark :test match-expr
                        :then then-expr
                        :else else-expr)))
   (mv t (ok) rhs))))

Theorem: booleanp-of-vl-udptable-assignrhs.okp

(defthm booleanp-of-vl-udptable-assignrhs.okp
  (b* (((mv ?okp ?warnings ?expr)
        (vl-udptable-assignrhs inexprs lines warnings)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: vl-warninglist-p-of-vl-udptable-assignrhs.warnings

(defthm vl-warninglist-p-of-vl-udptable-assignrhs.warnings
  (b* (((mv ?okp ?warnings ?expr)
        (vl-udptable-assignrhs inexprs lines warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-expr-p-of-vl-udptable-assignrhs.expr

(defthm vl-expr-p-of-vl-udptable-assignrhs.expr
  (b* (((mv ?okp ?warnings ?expr)
        (vl-udptable-assignrhs inexprs lines warnings)))
    (vl-expr-p expr))
  :rule-classes :rewrite)