Match
(vl-careless-match-latch x warnings) → (mv warnings test lhs rhs delay)
Function:
(defun vl-careless-match-latch (x warnings) (declare (xargs :guard (and (vl-always-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-careless-match-latch)) (declare (ignorable __function__)) (b* (((mv ctrl condition lhs rhs delay) (vl-match-latch-main x)) ((unless ctrl) (mv warnings nil nil nil nil)) ((vl-eventcontrol ctrl) ctrl) (lhs-wires (mergesort (vl-expr-names lhs))) (rhs-wires (mergesort (vl-expr-names rhs))) (condition-wires (mergesort (vl-expr-names condition))) (lhs/rhs-overlap (intersect lhs-wires rhs-wires)) (warnings (if lhs/rhs-overlap (warn :type :vl-warn-loopy-latch :msg "~a0: some wires on the left-hand side of the latch ~ are also mentioned in the rhs, which might mean a ~ combinational loop when the latch is enabled. Loopy ~ wires: ~&1." :args (list x lhs/rhs-overlap)) warnings)) (lhs/condition-overlap (intersect lhs-wires condition-wires)) (warnings (if lhs/condition-overlap (warn :type :vl-warn-weird-latch :msg "~a0: some wires on the left-hand side of the latch ~ are also mentioned in the enable condition, which is ~ strange and might indicate some kind of weird race. ~ Wires: ~&1." :args (list x lhs/condition-overlap)) warnings)) (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-careless-match-latch.warnings (implies (and (force (vl-always-p x)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?test ?lhs ?rhs ?delay) (vl-careless-match-latch x warnings))) (vl-warninglist-p warnings))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-careless-match-latch.test (implies (and (force (vl-always-p x)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?test ?lhs ?rhs ?delay) (vl-careless-match-latch x warnings))) (equal (vl-expr-p test) (if test t nil)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-careless-match-latch.lhs (implies (and (force (vl-always-p x)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?test ?lhs ?rhs ?delay) (vl-careless-match-latch x warnings))) (and (equal (vl-expr-p lhs) (if test t nil)) (iff lhs test)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-careless-match-latch.rhs (implies (and (force (vl-always-p x)) (force (vl-warninglist-p warnings))) (b* (((mv ?warnings ?test ?lhs ?rhs ?delay) (vl-careless-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-careless-match-latch.ticks (maybe-natp (mv-nth 4 (vl-careless-match-latch x warnings))) :rule-classes :type-prescription)