Clear, Correct, and Traceable: SPI SVA Best Practices

Ensuring Correctness and Observability in SPI Signal Assertions

In SPI verification, a fundamental requirement is that all active signals—SCLK, MOSI, and MISO—must be fully defined whenever chip-select is asserted. Any unknown or high-impedance state (X or Z) can compromise data integrity and lead to subtle bugs.

SystemVerilog Assertions (SVA) offer a natural mechanism to codify this requirement. When applied thoughtfully, they enforce correctness and enhance diagnostic clarity. Clear, modular assertions make failures immediately understandable, particularly in larger testbenches, which aligns well with style-aware analysis tools.

Issue 1: Functional Correctness

A common misstep is to combine multiple signals in a single $isunknown call with a logical AND:

// INCORRECT
$isunknown(spiclk && mosi && miso)

The problem: logical AND short-circuits evaluation, potentially masking unknown states.

• Example: spiclk = X, mosi = 0, miso = 1
• spiclk && mosi && miso = 0 → $isunknown(...)=0
• The property passes, inadvertently ignoring the unknown state on spiclk.

Correct approach: assess each signal independently:

property spi_signals_known;
  @(posedge mstclk) disable iff (!spirstn)
    !cs |=> !$isunknown(spiclk) && !$isunknown(mosi) && !$isunknown(miso);
endproperty : spi_signals_known

Each signal is checked individually, ensuring any unknown triggers a violation. Logical AND now combines Boolean results, avoiding short-circuiting issues. This style is functionally correct, readable, and amenable to linting tools like SVALint.

Issue 2: Observability and Debug-Friendliness

Even with functionally correct assertions, a single combined property can obscure the precise source of failure.

• Multiple signals becoming unknown simultaneously does not indicate which signal caused the problem.
• Diagnosing via waveform inspection can be laborious in extensive test environments.

Improved, debug-friendly approach: split the check into independent assertions per signal:

property spiclk_known;
  @(posedge mstclk) disable iff (!spirstn)
    !cs |=> !$isunknown(spiclk);
endproperty : spiclk_known

property mosi_known;
  @(posedge mstclk) disable iff (!spirstn)
    !cs |=> !$isunknown(mosi);
endproperty : mosi_known

property miso_known;
  @(posedge mstclk) disable iff (!spirstn)
    !cs |=> !$isunknown(miso);
endproperty : miso_known

Each assertion fails independently, immediately highlighting the offending signal. This approach improves coverage and simplifies debugging. Clear, modular assertions like these are naturally aligned with SVALint’s style checks.

Conclusion

1. Functional correctness: test each signal with $isunknown individually; avoid aggregation that can mask unknowns.
2. Debug-friendliness: independent assertions clarify exactly which signal fails, streamlining investigation.
3. Style-conscious verification: modular, readable assertions enhance maintainability and align with automated style checks.

By addressing both correctness and clarity, SPI verification becomes robust, maintainable, and immediately actionable, while subtly reflecting good coding style.