		Search-engine friendly clone of the ACL2 documentation.

Vl-simpledelay-p

Recognize simple delays like #5.

Signature
(vl-simpledelay-p x) → *
Arguments: x — Guard (vl-gatedelay-p x).

Verilog lets you give much richer delay specifications, e.g., you can specify separate delays for transitions to 1, 0, and Z, and you can even provide different minimum, typical, and maximum delays for each kind of transition. See vl-gatedelay-p.

These complex delays are generally too complicated for us to handle. Instead, we just try to support simple delays for some fixed number of ticks.

Definitions and Theorems

Function: vl-simpledelay-p

(defun vl-simpledelay-p (x)
  (declare (xargs :guard (vl-gatedelay-p x)))
  (let ((__function__ 'vl-simpledelay-p))
    (declare (ignorable __function__))
    (b* (((vl-gatedelay x) x))
      (and (vl-expr-resolved-p x.rise)
           (vl-expr-resolved-p x.fall)
           (eql (vl-resolved->val x.rise)
                (vl-resolved->val x.fall))
           (or (not x.high)
               (and (vl-expr-resolved-p x.high)
                    (eql (vl-resolved->val x.rise)
                         (vl-resolved->val x.high))))))))

Subtopics

Vl-simpledelay->amount: Get the number of ticks for a simple delay.