		Search-engine friendly clone of the ACL2 documentation.

Vl-lucidocc

Vl-lucidocc-slice

An indexed occurrence of an identifier.

This is a product type, introduced by deftagsum in support of vl-lucidocc.

Fields

left — vl-expr
right — vl-expr
ctx — vl-context1: The general context where the usage occurred. Knowing where the occurrence came from is useful when we need to report about multiply driven signals.
ss — vl-scopestack: Scopestack where this occurrence was found. Used in multidrive detection.

We use this to record occurrences of an identifier with a bit- or part-select. For individual selects like foo[3], both left and right will be the same.

Subtopics

Make-vl-lucidocc-slice: Basic constructor macro for vl-lucidocc-slice structures.
Vl-lucidocc-slice->ss: Get the ss field from a vl-lucidocc-slice.
Vl-lucidocc-slice->right: Get the right field from a vl-lucidocc-slice.
Vl-lucidocc-slice->left: Get the left field from a vl-lucidocc-slice.
Vl-lucidocc-slice->ctx: Get the ctx field from a vl-lucidocc-slice.
Change-vl-lucidocc-slice: Modifying constructor for vl-lucidocc-slice structures.