Extracts a delay amount from a vl-maybe-gatedelay.
(vl-maybe-gatedelay->delay x) → (mv warnings del)
Function:
(defun vl-maybe-gatedelay->delay (x) (declare (xargs :guard (vl-maybe-gatedelay-p x))) (let ((__function__ 'vl-maybe-gatedelay->delay)) (declare (ignorable __function__)) (b* ((x (vl-maybe-gatedelay-fix x)) ((unless (mbe :logic (vl-gatedelay-p x) :exec (and x t))) (mv nil nil)) ((vl-gatedelay x) x) (warnings nil) ((unless (and (vl-expr-resolved-p x.rise) (vl-expr-resolved-p x.fall) (or (not x.high) (vl-expr-resolved-p x.high)))) (mv (warn :type :vl-gatedelay->svex-fail :msg "gatedelay not resolved: ~x0" :args (list x)) nil)) (val (vl-resolved->val x.rise)) ((unless (and (eql val (vl-resolved->val x.fall)) (or (not x.high) (eql val (vl-resolved->val x.high))))) (mv (warn :type :vl-gatedelay->svex-fail :msg "Complex gatedelay ~x0" :args (list x)) nil)) ((when (< val 0)) (mv (warn :type :vl-gatedelay->svex-fail :msg "Negative gatedelay ~x0" :args (list x)) nil))) (mv nil val))))
Theorem:
(defthm vl-warninglist-p-of-vl-maybe-gatedelay->delay.warnings (b* (((mv ?warnings ?del) (vl-maybe-gatedelay->delay x))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm maybe-natp-of-vl-maybe-gatedelay->delay.del (b* (((mv ?warnings ?del) (vl-maybe-gatedelay->delay x))) (maybe-natp del)) :rule-classes :type-prescription)
Theorem:
(defthm vl-maybe-gatedelay->delay-of-vl-maybe-gatedelay-fix-x (equal (vl-maybe-gatedelay->delay (vl-maybe-gatedelay-fix x)) (vl-maybe-gatedelay->delay x)))
Theorem:
(defthm vl-maybe-gatedelay->delay-vl-maybe-gatedelay-equiv-congruence-on-x (implies (vl-maybe-gatedelay-equiv x x-equiv) (equal (vl-maybe-gatedelay->delay x) (vl-maybe-gatedelay->delay x-equiv))) :rule-classes :congruence)