RTL Property Inference

Step 2: Identify Control-Flow Invariants

Systematically analyze the design for common invariant patterns:

1. Mutual Exclusion:

   • Grant signals from arbiters
   • Mutually exclusive enable signals
   • One-hot state encodings
   • Look for: Multiple signals that should never be active simultaneously

2. Valid-Ready Handshakes:

   • Data stability during valid-without-ready
   • Valid persistence until handshake completes
   • No data loss (eventual completion)
   • Look for: Pairs of valid/ready signals with associated data

3. Pipeline Ordering:

   • Valid bit propagation through stages
   • Data stability in pipeline stages
   • Stall behavior (freezing pipeline state)
   • Look for: Arrays of valid signals, stage indices, pipeline registers

4. Safety Properties (bad things never happen):

   • Buffer overflow/underflow prevention
   • Invalid state detection
   • Address conflict prevention
   • Counter bounds
   • Look for: Boundary conditions, error states, conflict scenarios

Step 3: Identify Liveness Properties

Look for patterns indicating "good things eventually happen":

1. Request-Response Patterns:

   • Request eventually gets grant
   • Valid eventually gets ready
   • Transaction eventually completes
   • Look for: Request signals paired with acknowledgment/grant signals

2. Progress Properties:

   • FSM eventually leaves certain states
   • Counters eventually reach targets
   • Pipelines eventually drain
   • Look for: Temporary states, countdown logic, completion conditions

3. Fairness Constraints:

   • All requesters eventually get service
   • Round-robin behavior
   • Starvation freedom
   • Look for: Arbitration logic, scheduling mechanisms

Note: Liveness properties require careful analysis. Only infer when there's clear evidence of intended eventual behavior. Use bounded liveness (with timeouts) when unbounded liveness may not hold.

Step 4: Map Patterns to Properties

Use the pattern library in common_patterns.md to generate appropriate assertions:

1. Match identified patterns to known property templates
2. Instantiate properties with actual signal names from the design
3. Adjust timing parameters based on design characteristics (e.g., pipeline depth, timeout values)
4. Add appropriate disable conditions (typically reset)

Refer to sva_syntax.md for SVA syntax details.

Step 5: Classify Properties

Separate properties into clear categories:

1. Strong Invariants (assert):

   • Properties that must always hold in correct design
   • Internal consistency checks
   • Safety properties derived from design structure
   • Example: Mutual exclusion, one-hot encoding, buffer bounds

2. Assumed Environment Constraints (assume):

   • Properties about external inputs
   • Interface protocol assumptions
   • Timing assumptions from environment
   • Example: Input valid-ready protocol compliance, reset behavior

3. Coverage Properties (cover):

   • Reachability checks for important scenarios
   • Corner case coverage
   • Example: All FSM states reachable, maximum buffer occupancy

Step 6: Generate Output

For each inferred property, provide:

1. SVA assertion code:

   property_name: assert property (
     @(posedge clk) disable iff (rst)
       antecedent |-> consequent
   ) else $error("Description of violation");
   

2. Natural-language explanation:

   • What the property checks
   • Why it should hold
   • What violation would indicate

3. Signal list:

   • All signals involved in the property
   • Their roles (control, data, state)

4. Classification:

   • Type: Safety / Liveness / Fairness
   • Directive: Assert / Assume / Cover
   • Confidence: High / Medium / Low (based on pattern clarity)

5. Additional context:

   • Related properties (if any)
   • Assumptions made during inference
   • Suggested verification approach

Output Format

Structure the output as follows:

## Inferred Properties for [Module Name]

### Clock and Reset
- Clock: <signal_name> (<edge>)
- Reset: <signal_name> (<polarity>, <sync/async>)

### Strong Invariants (Assert)

#### Property 1: <Short Name>
**Type**: Safety | Liveness | Fairness
**Confidence**: High | Medium | Low

**Assertion**:
```systemverilog
<property_name>: assert property (
  @(posedge clk) disable iff (rst)
    <property_expression>
) else $error("<error_message>");

Explanation: <Natural language description of what this property checks and why>

Signals Involved:

• <signal1>: <role/description>
• <signal2>: <role/description>

Rationale: <Why this property was inferred from the RTL structure>

[Repeat for each property]

Assumed Environment Constraints (Assume)

[Same format as above, but using assume directive]

Coverage Properties (Cover)

[Same format as above, but using cover directive]

Summary

• Total properties inferred: <count>
  • Strong invariants: <count>
  • Environment assumptions: <count>
  • Coverage properties: <count>
• Patterns identified: <list of patterns>
• Verification recommendations: <suggestions>

## Important Guidelines

1. **Be conservative**: Only infer properties with clear evidence in the RTL
2. **Explain reasoning**: Always justify why a property was inferred
3. **Mark confidence**: Indicate confidence level (High/Medium/Low) for each property
4. **Avoid false positives**: Better to miss a property than infer an incorrect one
5. **Consider timing**: Ensure delay values match design behavior
6. **Check vacuity**: Suggest cover properties for antecedents to avoid vacuous success
7. **Document assumptions**: Clearly state any assumptions made during inference
8. **Provide context**: Explain how properties relate to overall design correctness

## Example Usage

**User request**: "Infer properties from this FIFO module"

**Process**:
1. Parse RTL and identify: full, empty, wr_en, rd_en, count signals
2. Recognize FIFO pattern with full/empty flags
3. Infer safety properties:
   - No write when full
   - No read when empty
   - Count within bounds [0:DEPTH]
   - Full and empty mutually exclusive (unless DEPTH=1)
4. Infer liveness property:
   - Write eventually makes FIFO non-empty
5. Generate SVA assertions with explanations
6. Classify as strong invariants (assert)
7. Add coverage for full and empty conditions

## References

- [common_patterns.md](references/common_patterns.md) - Library of common RTL patterns and their properties
- [sva_syntax.md](references/sva_syntax.md) - SystemVerilog Assertions syntax reference

## Limitations

- Cannot infer properties requiring deep semantic understanding beyond structural patterns
- May miss complex cross-module properties
- Liveness properties may need manual refinement for unbounded cases
- Timing parameters (delays, timeouts) may need adjustment based on actual design constraints
- Does not replace manual formal specification for critical properties