		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-make-delay-assigns

Signature
(vl-make-delay-assigns lhses rhses delay-amt atts) → assigns
Arguments: lhses — Guard (vl-exprlist-p lhses).; rhses — Guard (vl-exprlist-p rhses).; delay-amt — Guard (natp delay-amt).; atts — Guard (vl-atts-p atts).
Returns: assigns — Type (vl-assignlist-p assigns).

Definitions and Theorems

Function: vl-make-delay-assigns

(defun vl-make-delay-assigns (lhses rhses delay-amt atts)
  (declare (xargs :guard (and (vl-exprlist-p lhses)
                              (vl-exprlist-p rhses)
                              (natp delay-amt)
                              (vl-atts-p atts))))
  (declare (xargs :guard (equal (len lhses) (len rhses))))
  (let ((__function__ 'vl-make-delay-assigns))
    (declare (ignorable __function__))
    (if (atom lhses)
        nil
      (cons (make-vl-assign :lvalue (car lhses)
                            :expr (car rhses)
                            :delay (vl-make-constdelay delay-amt)
                            :atts atts
                            :loc *vl-fakeloc*)
            (vl-make-delay-assigns (cdr lhses)
                                   (cdr rhses)
                                   delay-amt atts)))))

Theorem: vl-assignlist-p-of-vl-make-delay-assigns

(defthm vl-assignlist-p-of-vl-make-delay-assigns
  (b* ((assigns (vl-make-delay-assigns lhses rhses delay-amt atts)))
    (vl-assignlist-p assigns))
  :rule-classes :rewrite)