Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

readme: Update documentation of assertion macros #237

Merged
merged 3 commits into from
Oct 4, 2024
Merged

readme: Update documentation of assertion macros #237

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6b81605
readme: Update documentation of assertion macros
michael-platzer Oct 4, 2024
d088998
readme: Fix formatting for consistency
michael-platzer Oct 4, 2024
5d777e3
readme: Update statement on relationship with lowrisc assert macros
michael-platzer Oct 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 27 additions & 23 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -165,38 +165,42 @@ easier to use them. They are identical with the macros used by [lowrisc](https:/
and just re-implemented here for the sake of easier use in PULP projects (the same include guard is used so they should not clash).

#### Simple Assertion and Cover Macros
| Macro | Arguments | Description |
| ----------------------------------------------------------- | -------------------------------------------------------------------------- | ----------- |
| `` `ASSERT_I`` | `__name`, `__prop` | Immediate assertion |
| `` `ASSERT_INIT`` | `__name`, `__prop` | Assertion in initial block. Can be used for things like parameter checking |
| `` `ASSERT_FINAL`` | `__name`, `__prop` | Assertion in final block |
| `` `ASSERT`` | `__name`, `__prop`, (`__clk`, `__rst`) | Assert a concurrent property directly |
| `` `ASSERT_NEVER`` | `__name`, `__prop`, (`__clk`, `__rst`) | Assert a concurrent property NEVER happens |
| `` `ASSERT_KNOWN`` | `__name`, `__sig`, (`__clk`, `__rst`) | Concurrent clocked assertion with custom error message |
| `` `COVER`` | `__name`, `__prop`, (`__clk`, `__rst`) | Cover a concurrent property |
| Macro | Arguments | Description |
| ------------------ | ------------------------------------------------ | -------------------------------------------------------------------------- |
| `` `ASSERT_I`` | `__name`, `__prop`, (`__desc`) | Immediate assertion |
| `` `ASSERT_INIT`` | `__name`, `__prop`, (`__desc`) | Assertion in initial block. Can be used for things like parameter checking |
| `` `ASSERT_FINAL`` | `__name`, `__prop`, (`__desc`) | Assertion in final block |
| `` `ASSERT`` | `__name`, `__prop`, (`__clk`, `__rst`, `__desc`) | Assert a concurrent property directly |
| `` `ASSERT_NEVER`` | `__name`, `__prop`, (`__clk`, `__rst`, `__desc`) | Assert a concurrent property NEVER happens |
| `` `ASSERT_KNOWN`` | `__name`, `__sig`, (`__clk`, `__rst`, `__desc`) | Concurrent clocked assertion with custom error message |
| `` `COVER`` | `__name`, `__prop`, (`__clk`, `__rst`) | Cover a concurrent property |
- *The name of the clock and reset signals for implicit variants is `clk_i` and `rst_ni`, respectively.*
- *`__desc` is an optional string argument describing the failure causing the assertion to be violated that is embedded into the error report and defaults to `""`.*

#### Complex Assertion Macros
| Macro | Arguments | Description |
| -------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------- | ----------- |
| `` `ASSERT_PULSE`` | `__name`, `__sig`, (`__clk`, `__rst`) | Assert that signal is an active-high pulse with pulse length of 1 clock cycle |
| `` `ASSERT_IF`` | `__name`, `__prop`, `__enable`, (`__clk`, `__rst`) | Assert that a property is true only when an enable signal is set |
| `` `ASSERT_KNOWN_IF`` | `__name`, `__sig`, `__enable`, (`__clk`, `__rst`) | Assert that signal has a known value (each bit is either '0' or '1') after reset if enable is set |
| Macro | Arguments | Description |
| --------------------- | ------------------------------------------------------------ | ------------------------------------------------------------------------------------------------- |
| `` `ASSERT_PULSE`` | `__name`, `__sig`, (`__clk`, `__rst`, `__desc`) | Assert that signal is an active-high pulse with pulse length of 1 clock cycle |
| `` `ASSERT_IF`` | `__name`, `__prop`, `__enable`, (`__clk`, `__rst`, `__desc`) | Assert that a property is true only when an enable signal is set |
| `` `ASSERT_KNOWN_IF`` | `__name`, `__sig`, `__enable`, (`__clk`, `__rst`, `__desc`) | Assert that signal has a known value (each bit is either '0' or '1') after reset if enable is set |
- *The name of the clock and reset signals for implicit variants is `clk_i` and `rst_ni`, respectively.*
- *`__desc` is an optional string argument describing the failure causing the assertion to be violated that is embedded into the error report and defaults to `""`.*

#### Assumption Macros

| Macro | Arguments | Description |
| ------------------------------------------------------- | ---------------------------- | ----------- |
| `` `ASSUME`` | `__name`, `__prop`, (`__clk`, `__rst`) | Assume a concurrent property |
| `` `ASSUME_I`` | `__name`, `__prop` | Assume an immediate property |
| Macro | Arguments | Description |
| -------------- | ------------------------------------------------ | ---------------------------- |
| `` `ASSUME`` | `__name`, `__prop`, (`__clk`, `__rst`, `__desc`) | Assume a concurrent property |
| `` `ASSUME_I`` | `__name`, `__prop`, (, `__desc`) | Assume an immediate property |
michael-platzer marked this conversation as resolved.
Show resolved Hide resolved
- *The name of the clock and reset signals for implicit variants is `clk_i` and `rst_ni`, respectively.*
- *`__desc` is an optional string argument describing the failure causing the assertion to be violated that is embedded into the error report and defaults to `""`.*

#### Formal Verification Macros

| Macro | Arguments | Description |
| ----------------------------------------------------------- | ------------------------------------------------------------ | ----------- |
| `` `ASSUME_FPV`` | `__name`, `__prop`, (`__clk`, `__rst`) | Assume a concurrent property during formal verification only |
| `` `ASSUME_I_FPV`` | `__name`, `__prop` | Assume a concurrent property during formal verification only |
| `` `COVER_FPV`` | `__name`, `__prop`, (`__clk`, `__rst`) | Cover a concurrent property during formal verification |
| Macro | Arguments | Description |
| ------------------ | ------------------------------------------------ | ------------------------------------------------------------ |
| `` `ASSUME_FPV`` | `__name`, `__prop`, (`__clk`, `__rst`, `__desc`) | Assume a concurrent property during formal verification only |
| `` `ASSUME_I_FPV`` | `__name`, `__prop`, (, `__desc`) | Assume a concurrent property during formal verification only |
michael-platzer marked this conversation as resolved.
Show resolved Hide resolved
| `` `COVER_FPV`` | `__name`, `__prop`, (`__clk`, `__rst`) | Cover a concurrent property during formal verification |
- *The name of the clock and reset signals for implicit variants is `clk_i` and `rst_ni`, respectively.*
- *`__desc` is an optional string argument describing the failure causing the assertion to be violated that is embedded into the error report and defaults to `""`.*
Loading