Group Q.1 - Verification directives. Issues
Issues
83,
90, 94, 105,
106, 107, 108,
111, 126, 133,
134.
66, 67
Discussion
- Semantics of restrict. See:
- http://www.eda-stds.org/ieee-1850/ieee-1850-issues/hm/0422.html
- http://www.eda-stds.org/ieee-1850/ieee-1850-issues/hm/0427.html
Resolution
It should be possible to describe the following types of restrictions:
- Some prefix of the path matches the SERE r tightly - can be expressed by
assume r! Therefore does not require a special keyword.
- restrict! r - The path models tightly the SERE - defined for a finite path,
and undefined for infinite paths.
- restrict r - The path ends too soon. Can be expressed as assume {r;EOP} or assume{r;false}.
Additional Notes
- It will require an omega operator and omega semantics to define "models tightly"
(and therefore option 2) for infinite paths.
- We need to define EOP.
- The issues that were covered by the proposal bellow:
83, 90, 105, 107
LRM Changes