		Search-engine friendly clone of the ACL2 documentation.

Vl-eventcontrol

Representation of an event controller like @(posedge clk) or @(a or b).

This is a product type introduced by defprod.

starp — booleanp: True to represent @(*), or nil for any other kind of event controller.
atoms — vl-evatomlist: A list of vl-evatom-ps that describe the various events. Verilog allows two kinds of syntax for these lists, e.g., one can write @(a or b) or @(a, b). The meaning is identical in either case, so we just use a list of atoms.

Event controls are described in Section 9.7. We represent each event controller as a vl-eventcontrol-p aggregates.

Vl-eventcontrol-fix: Fixing function for vl-eventcontrol structures.
Vl-eventcontrol-equiv: Basic equivalence relation for vl-eventcontrol structures.
Make-vl-eventcontrol: Basic constructor macro for vl-eventcontrol structures.
Vl-eventcontrol-p: Recognizer for vl-eventcontrol structures.
Vl-eventcontrol->starp: Get the starp field from a vl-eventcontrol.
Vl-eventcontrol->atoms: Get the atoms field from a vl-eventcontrol.
Change-vl-eventcontrol: Modifying constructor for vl-eventcontrol structures.