		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-nedgeflop-e-wires

Signature
(vl-nedgeflop-e-wires exprs walist) → wires
Arguments: exprs — Guard (vl-exprlist-p exprs).; walist — Guard (vl-wirealist-p walist).
Returns: wires — Type (true-listp wires).

Definitions and Theorems

Function: vl-nedgeflop-e-wires

(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: true-listp-of-vl-nedgeflop-e-wires

(defthm true-listp-of-vl-nedgeflop-e-wires
  (b* ((wires (vl-nedgeflop-e-wires exprs walist)))
    (true-listp wires))
  :rule-classes :type-prescription)

Theorem: len-of-vl-nedgeflop-e-wires

(defthm len-of-vl-nedgeflop-e-wires
  (equal (len (vl-nedgeflop-e-wires exprs walist))
         (len exprs)))

Theorem: consp-of-vl-nedgeflop-e-wires

(defthm consp-of-vl-nedgeflop-e-wires
  (equal (consp (vl-nedgeflop-e-wires exprs walist))
         (consp exprs)))

Theorem: vl-nedgeflop-e-wires-under-iff

(defthm vl-nedgeflop-e-wires-under-iff
  (iff (vl-nedgeflop-e-wires exprs walist)
       (consp exprs)))