Match
(vl-careful-match-latch x warnings) → (mv warnings test lhs rhs delay)
Function:
(defun vl-careful-match-latch (x warnings) (declare (xargs :guard (and (vl-always-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-careful-match-latch)) (declare (ignorable __function__)) (b* (((mv ctrl condition lhs rhs delay) (vl-match-latch-main x)) ((unless (and ctrl (vl-idexpr-p lhs))) (mv warnings nil nil nil nil)) ((unless (vl-idexpr-p lhs)) (mv (warn :type :vl-latch-fail :msg "~a0: failing to infer a latch because the left-hand ~ side, ~a1, isn't a simple identifier." :args (list x lhs)) nil nil nil nil)) ((vl-eventcontrol ctrl) ctrl) (lhs-name (vl-idexpr->name lhs)) (rhs-wires (vl-expr-names rhs)) (condition-wires (vl-expr-names condition)) ((when (member-equal lhs-name rhs-wires)) (mv (warn :type :vl-latch-fail :msg "~a0: failing to infer a latch because the register ~ being assigned to, ~s1, occurs in the rhs expression, ~ ~a2. This suggests there may be a combinational loop ~ when the latch is enabled." :args (list x lhs-name rhs)) nil nil nil nil)) ((when (member-equal lhs-name condition-wires)) (mv (warn :type :vl-latch-fail :msg "~a0: failing to infer a latch because the register ~ being assigned to, ~s1, occurs in its own enable ~ expression, ~a2. This seems very strange and might ~ indicate some kind of weird race." :args (list x lhs-name condition)) nil nil nil nil)) (need-wires (if ctrl.starp nil (append rhs-wires condition-wires))) (have-wires (if ctrl.starp nil (vl-idexprlist->names (vl-evatomlist->exprs ctrl.atoms)))) ((unless (subsetp-equal need-wires have-wires)) (mv (warn :type :vl-latch-fail :msg "~a0: failing to infer a latch since the sensitivity ~ list omits ~&1." :args (list x (set-difference-equal need-wires have-wires))) nil nil nil nil)) (warnings (if (subsetp-equal have-wires need-wires) warnings (warn :type :vl-sensitivity-list :msg "~a0: sensitivity list appears to include ~&1 ~ unnecessarily, which might slow down simulations." :args (list x (set-difference-equal have-wires need-wires)))))) (mv warnings condition lhs rhs delay))))
Theorem:
(defthm vl-warninglist-p-of-vl-careful-match-latch.warnings (implies (and (force (vl-always-p x)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?test ?lhs ?rhs ?delay) (vl-careful-match-latch x warnings))) (vl-warninglist-p warnings))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-careful-match-latch.test (implies (and (force (vl-always-p x)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?test ?lhs ?rhs ?delay) (vl-careful-match-latch x warnings))) (equal (vl-expr-p test) (if test t nil)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-careful-match-latch.lhs (implies (and (force (vl-always-p x)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?test ?lhs ?rhs ?delay) (vl-careful-match-latch x warnings))) (and (equal (vl-expr-p lhs) (if test t nil)) (equal (vl-idexpr-p lhs) (if test t nil)) (iff lhs test)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-careful-match-latch.rhs (implies (and (force (vl-always-p x)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?test ?lhs ?rhs ?delay) (vl-careful-match-latch x warnings))) (and (equal (vl-expr-p rhs) (if test t nil)) (iff rhs test)))) :rule-classes :rewrite)
Theorem:
(defthm maybe-natp-of-vl-careful-match-latch.ticks (maybe-natp (mv-nth 4 (vl-careful-match-latch x warnings))) :rule-classes :type-prescription)