Vl-udpsymbol-p
Symbols that can occur in a UDP table
These are basically taken from Verilog-2005 Table 8-1.
- :vl-udp-0 — logic 0.
- :vl-udp-1 — logic 1.
- :vl-udp-x — unknown. Permitted in input/outputs of all UDPs and
current state of sequential UDPs.
- :vl-udp-? — iteration of 0, 1, and X. Not permitted in outputs.
- :vl-udp-b — iteration of 0 and 1. Permitted in inputs of all
udps and current state of sequential udps, not in outputs.
- :vl-udp-- — no change. Permitted only in the output field of a
sequential UDP.
- :vl-udp-* — any value change on input, same as (??).
- :vl-udp-r — rising edge on input, same as (01).
- :vl-udp-f — falling edge on input, same as (10).
- :vl-udp-p — any potential positive edge on the input, iteration of
(01), (0x), (x1).
- :vl-udp-n — any potential negative edge on the input, iteration of
(10), (1x), (x0).
This is an ordinary defenum.
Function: vl-udpsymbol-p
(defun vl-udpsymbol-p (x)
(declare (xargs :guard t))
(or (eq x ':vl-udp-0)
(eq x ':vl-udp-1)
(eq x ':vl-udp-x)
(eq x ':vl-udp-?)
(eq x ':vl-udp-b)
(eq x ':vl-udp--)
(eq x ':vl-udp-*)
(eq x ':vl-udp-r)
(eq x ':vl-udp-f)
(eq x ':vl-udp-p)
(eq x ':vl-udp-n)))Theorem: type-when-vl-udpsymbol-p
(defthm type-when-vl-udpsymbol-p
(implies (vl-udpsymbol-p x)
(if (symbolp x)
(if (not (equal x 't))
(not (equal x 'nil))
'nil)
'nil))
:rule-classes :compound-recognizer)
