		Search-engine friendly clone of the ACL2 documentation.

4v-operations

4v-xdet

X-detection or identity circuit.

(4v-xdet a) returns the value specified by the following truth table:

  a  |  out
-----+-------
  T  |   F
  F  |   F
  X  |   X
  Z  |   X
-----+-------

This is a special operation that does not correspond to any sort of hardware circuit, but that is useful for efficiently implementing the x-detection semantics of Verilog's vector arithmetic operations.

Definitions and Theorems

Function: 4v-xdet$inline

(defun 4v-xdet$inline (a)
  (declare (xargs :guard t))
  (4vcases a (t (4vf))
           (f (4vf))
           (& (4vx))))

Theorem: 4v-xdet-truth-table

(defthm 4v-xdet-truth-table
  (and (equal (4v-xdet (4vt)) (4vf))
       (equal (4v-xdet (4vf)) (4vf))
       (equal (4v-xdet (4vx)) (4vx))
       (equal (4v-xdet (4vz)) (4vx)))
  :rule-classes nil)

Theorem: 4v-equiv-implies-equal-4v-xdet-1

(defthm 4v-equiv-implies-equal-4v-xdet-1
  (implies (4v-equiv a a-equiv)
           (equal (4v-xdet a) (4v-xdet a-equiv)))
  :rule-classes (:congruence))