(vl-nedgeflop-e-wires exprs walist) → wires
Function:
(defun vl-nedgeflop-e-wires (exprs walist) (declare (xargs :guard (and (vl-exprlist-p exprs) (vl-wirealist-p walist)))) (let ((__function__ 'vl-nedgeflop-e-wires)) (declare (ignorable __function__)) (b* (((mv okp warnings wires) (vl-msb-exprlist-bitlist exprs walist nil)) ((unless (and okp (not warnings) (same-lengthp exprs wires))) (raise "Expected exactly ~x0 wires for N-edge 1-bit flop." (len exprs)) (replicate (len exprs) 'error))) wires)))
Theorem:
(defthm true-listp-of-vl-nedgeflop-e-wires (b* ((wires (vl-nedgeflop-e-wires exprs walist))) (true-listp wires)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-nedgeflop-e-wires (equal (len (vl-nedgeflop-e-wires exprs walist)) (len exprs)))
Theorem:
(defthm consp-of-vl-nedgeflop-e-wires (equal (consp (vl-nedgeflop-e-wires exprs walist)) (consp exprs)))
Theorem:
(defthm vl-nedgeflop-e-wires-under-iff (iff (vl-nedgeflop-e-wires exprs walist) (consp exprs)))