SVA for AHB Verification

SystemVerilog Assertions are critical for verifying protocol compliance. Below are the "Must-Have" assertions for any AHB Master or Slave.

Master Stability Assertion

Rule: If HREADY is low, the Master must hold Address/Control signals stable (unless passing IDLE->NONSEQ transition, wait, simplest rule first).

property p_stable_master;
    @(posedge hclk) disable iff (!hresetn)
    (!hready) |-> 
    ($stable(haddr) && $stable(htrans) && $stable(hwrite) && 
     $stable(hsize) && $stable(hburst));
endproperty

a_stable_master: assert property(p_stable_master)
    else $error("AHB Violation: Master signals changed while HREADY was low!");

Reset Check

Rule: During Reset, HTRANS must be IDLE.

property p_reset_idle;
    @(posedge hclk) 
    (!hresetn) |-> (htrans == 2'b00); // IDLE
endproperty

a_reset_idle: assert property(p_reset_idle)
    else $error("VIOLATION: HTRANS is not IDLE during Reset");

Write Data Stability

Rule: HWDATA must remain stable during the Data Phase wait states.

// If we are in a Write Data Phase and HREADY is low...
property p_stable_data;
    @(posedge hclk) disable iff (!hresetn)
    // Detailed logic requires tracking phases, but simplified:
    (state == DATA_PHASE && hwrite && !hready) |-> $stable(hwdata);
endproperty

Common Interview Questions

Q: How do you check the 1KB boundary rule?
You write a property that, on HTRANS==NONSEQ (start of burst), calculates the end_address based on HSIZE and HBURST. Then simply check:
(start_addr[31:10] == end_addr[31:10]).