		Search-engine friendly clone of the ACL2 documentation.

Cblock-path-checking

Vl-cblock-pathcheck

Check whether a list of variables are always assigned to in every execution of the always block, i.e., whether this really is a purely combinational block.

Signature
(vl-cblock-pathcheck vars stmt) → *
Arguments: vars — Guard (string-listp vars).; stmt — Guard (vl-stmt-p stmt).

Definitions and Theorems

Function: vl-cblock-pathcheck

(defun vl-cblock-pathcheck (vars stmt)
  (declare (xargs :guard (and (string-listp vars)
                              (vl-stmt-p stmt))))
  (declare (xargs :guard (vl-stmt-cblock-p stmt)))
  (let ((__function__ 'vl-cblock-pathcheck))
    (declare (ignorable __function__))
    (if (atom vars)
        t
      (and (vl-stmt-cblock-pathcheck1 (car vars)
                                      stmt)
           (vl-cblock-pathcheck (cdr vars)
                                stmt)))))