Skip to content

Conversation

kroening
Copy link
Collaborator

This adds support for SystemVerilog named properties.

Concurrent assertion items (assert/assume/cover) that are module items with
a block label go into the module name space, not into a separate "property"
name space.

Assertion items without block item now get a label based on the kind of the
assertion item (assert/assume/cover).
@kroening kroening force-pushed the named_property1 branch 2 times, most recently from a613ace to f7c6ec7 Compare June 24, 2024 22:38
@kroening kroening marked this pull request as ready for review June 24, 2024 22:39
This adds support for SystemVerilog named properties.
CORE
named_property1.sv
--bound 0
^\[main\.assert\.1\] always main\.x == 10: PROVED up to bound 0$
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wouldn't it make sense for x_is_ten to be used here in some way?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd like that -- it would require splitting up the type checking phase such that the initial phase doesn't expand symbols marked as "macro". Will do eventually.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@kroening kroening merged commit e746526 into main Jun 30, 2024
@kroening kroening deleted the named_property1 branch June 30, 2024 07:39
Romy15200 pushed a commit to Romy15200/nws that referenced this pull request Aug 19, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants