APB3 Slave Formal Verification

Overview

This project demonstrates formal verification of an APB3 Slave design using SystemVerilog Assertions (SVA). The APB3 slave is verified by assuming correct APB3 master behavior and proving that the slave complies with the APB3 protocol and its functional requirements under all valid scenarios.

The goal is to ensure protocol correctness, robustness, and corner-case coverage without relying on simulation-based stimulus.

---

Verification Approach

• The APB3 Slave is treated as the Design Under Test (DUT)
• The APB3 Master behavior is constrained using assumptions
• Formal tools explore all legal master transactions
• Assertions are used to prove correctness of the slave behavior

This approach guarantees exhaustive verification for all valid APB3 scenarios.

---

Assumed APB3 Master Behavior

The master is constrained using assumptions to follow the APB3 protocol:

• PSEL asserted before PENABLE
• PENABLE asserted only in access phase
• Address and control signals stable during access
• PREADY sampled only when PENABLE is high
• No protocol-violating signal sequences

These assumptions define the legal environment for the APB3 slave.

---

Verified Properties

The following aspects of the APB3 slave are formally verified:

Protocol Compliance

• Correct handling of setup and access phases
• Proper use of PREADY
• Stable read data during valid transfers
• Correct response timing for reads and writes

Functional Correctness

• Read data corresponds to the addressed register/memory
• Write operations update the correct locations
• No unintended state changes

Error Handling

• Proper assertion of PSLVERR for invalid accesses
• No spurious error responses during valid transfers

Reset Behavior

• Slave enters a known safe state after reset
• No protocol activity before reset deassertion

---

Assertions and Coverage

• Assertions (SVA) used to prove:

  • Protocol rules
  • Functional properties

• Formal coverage used to ensure:

  • Read and write paths are exercised
  • Wait-state scenarios are explored
  • Error and non-error cases are reachable

---

Advantages of Formal Verification

• Exhaustive checking of all legal APB3 master transactions
• Early detection of corner-case bugs
• No dependency on testbench stimulus
• Strong confidence in protocol correctness

---

Tools & Technology

• Language: SystemVerilog
• Assertions: SystemVerilog Assertions (SVA)
• Method: Formal Property Verification
• Applicable Tools: JasperGold / VC Formal (tool-independent properties)

---

Status

• APB3 slave protocol formally verified
• Master behavior fully constrained using assumptions
• No protocol violations under all legal scenarios

---