Assertions (SVA)

Gün 5: Arayüzler, Assertion ve Coverage | Immediate ve Concurrent assertion'lar, property, sequence

Bu derste SystemVerilog Assertions (SVA) ile tasarımın doğru davranıp davranmadığını otomatik olarak nasıl denetleyeceğimizi öğreneceğiz. immediate ve concurrent assertion farkını, sequence ve property yapılarını ve cover kullanımını ele alacağız.

Assertion Nedir, Neden Kullanılır?

Assertion, tasarımın uyması gereken bir kuralı biçimsel olarak ifade eden ve simülasyon sırasında sürekli denetleyen bir ifadedir. Kural ihlal edildiği anda assertion başarısız olur ve mesaj basar. Faydaları:

• Hatayı kaynağında yakalar: Hata, etkisi çıkışa yansımadan, oluştuğu saatte raporlanır.
• Belgeleme görevi görür: Protokol kuralları kodun içinde okunabilir biçimde yazılı durur.
• Kapsam ölçer: cover ile belirli senaryoların gerçekten test edildiğini doğrularsınız.

Immediate ve Concurrent Assertion Farkı

• Immediate assertion: Prosedürel bir blok içinde (always, initial) yürütülür ve o anda, bir yazılım if ifadesi gibi anlık değerlendirilir. Zamansal davranış denetlemez.
• Concurrent assertion: Bir saat olayına göre çalışır (@(posedge clk)), birden fazla saat çevrimine yayılan zamansal ilişkileri kontrol eder. property ve sequence ile kurulur.

Property, Sequence ve Operatörler

• sequence: Zaman içindeki sinyal desenlerini tarif eder. ##[1:3] "1 ila 3 çevrim sonra", [*4] "4 ardışık çevrim boyunca" anlamına gelir.
• property: Bir koşulun sonucunu tanımlar. |-> (overlapping) tetikleme ile sonucu aynı çevrimde, |=> (non-overlapping) ise sonraki çevrimde bekler.
• disable iff (!rst_n): Reset aktifken assertion'ı devre dışı bırakır; reset sırasındaki sahte ihlalleri önler.
• $fell/$rose: Bir sinyalin düşen/yükselen kenarını yakalar.

Kaynak Kod

// =============================================================================
// GUN 5 - Konu 4: SystemVerilog Assertions (SVA) - Immediate ve Concurrent
// =============================================================================

module assertions;
  logic clk = 0;
  always #5 clk = ~clk;

  logic       rst_n;
  logic       req;
  logic       gnt;
  logic       valid;
  logic       ready;
  logic [7:0] data;
  logic       error;

  // Basit DUT davranisi
  always @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      gnt   <= 0;
      ready <= 0;
      error <= 0;
    end else begin
      gnt   <= req;            // 1 cycle gecikme ile grant
      ready <= valid;          // 1 cycle gecikme ile ready
      error <= (data == 8'hFF); // 0xFF durumunda hata
    end
  end

  // =========================================================================
  // IMMEDIATE ASSERTIONS: Prosedurel blok icinde, aninda kontrol
  // =========================================================================
  
  always @(posedge clk) begin
    if (rst_n) begin
      // Basit immediate assertion
      assert_valid_data: assert (data !== 8'hxx)
        else $warning("[%0t] Data belirsiz (x)!", $time);

      // Error ve valid ayni anda aktif olmamali
      assert_no_error_valid: assert (!(error && valid))
        else $error("[%0t] Error ve valid ayni anda aktif!", $time);
    end
  end

  // =========================================================================
  // SEQUENCE TANIMLARI: Zamansal davranislar icin yapi taslari
  // =========================================================================
  sequence s_handshake;
    valid ##[1:3] ready;
  endsequence

  sequence s_burst;
    valid [*4];  // 4 ardisik cycle boyunca valid
  endsequence

  // =========================================================================
  // CONCURRENT ASSERTIONS: Zamansal iliskileri kontrol eder
  // =========================================================================

  // Property: req -> sonraki cycle gnt gelmeli
  property p_req_gnt;
    @(posedge clk) disable iff (!rst_n)
    req |=> gnt;
  endproperty

  // Property: valid kalktiginda 1-3 cycle icinde ready gelmeli
  property p_valid_ready;
    @(posedge clk) disable iff (!rst_n)
    valid |-> ##[1:3] ready;
  endproperty

  // Property: Reset durumunda tum cikislar sifir olmali
  property p_reset_check;
    @(posedge clk)
    !rst_n |-> !gnt && !ready && !error;
  endproperty

  // Property: Req dustugunde sonraki cycle gnt de dusmeli
  property p_req_deassert;
    @(posedge clk) disable iff (!rst_n)
    $fell(req) |=> $fell(gnt);
  endproperty

  // --- SEQUENCE KULLANAN YENI PROPERTY'LER ---

  // s_handshake kullanan property: Handshake gerceklestiginde hata (error) olmamali
  property p_handshake_no_error;
    @(posedge clk) disable iff (!rst_n)
    s_handshake |-> !error;
  endproperty

  // s_burst kullanan property: 4 valid'lik burst isleminden sonra gnt gelmeli
  property p_burst_leads_to_gnt;
    @(posedge clk) disable iff (!rst_n)
    s_burst |-> ##[1:5] gnt;
  endproperty

  // =========================================================================
  // ASSERTION'LARI ETKINLESTIRME (ASSERT & COVER)
  // =========================================================================

  assert property (p_req_gnt)
    else $error("[%0t] REQ->GNT ihlali!", $time);

  assert property (p_valid_ready)
    else $error("[%0t] VALID->READY ihlali!", $time);

  assert property (p_reset_check)
    else $error("[%0t] Reset kontrol ihlali!", $time);

  assert property (p_handshake_no_error)
    else $error("[%0t] Handshake sequence sirasinda hata olustu!", $time);

  assert property (p_burst_leads_to_gnt)
    else $error("[%0t] Burst tamamlandi ancak grant gelmedi!", $time);

  // Cover: Bu durumun gerceklestigini dogrula
  cover property (p_req_gnt)
    $display("[%0t] COVER: req->gnt gozlemlendi", $time);

  // Sequence'larin gerceklesip gerceklesmedigini dogrudan takip etme
  cover property (@(posedge clk) s_handshake)
    $display("[%0t] COVER: Handshake sequence (s_handshake) tamamlandi", $time);

  cover property (@(posedge clk) s_burst)
    $display("[%0t] COVER: Burst sequence (s_burst) tamamlandi", $time);


  // =========================================================================
  // TEST UYARICILARI (STIMULUS)
  // =========================================================================
  initial begin
    $display("=== SystemVerilog Assertions (SVA) ===\n");

    rst_n = 0; req = 0; valid = 0; data = 0;
    #20;
    rst_n = 1;
    #10;

    // Normal req/gnt
    $display("--- Normal REQ/GNT ---");
    @(posedge clk); req = 1;
    @(posedge clk); @(posedge clk);
    req = 0;
    #20;

    // Valid/Ready handshake
    $display("--- VALID/READY Handshake ---");
    @(posedge clk); valid = 1; data = 8'hAB;
    @(posedge clk); @(posedge clk);
    valid = 0;
    #30;

    // Hata durumu
    $display("--- Hata Testi (data=0xFF) ---");
    @(posedge clk); valid = 1; data = 8'hFF;
    @(posedge clk); valid = 0; data = 0;
    #30;

    // YENI: Burst durumu
    $display("--- Burst Testi (4 ardisik valid) ---");
    @(posedge clk); 
    req = 1; // p_burst_leads_to_gnt property'sini saglamak icin req tetikleniyor
    valid = 1; data = 8'h11;
    @(posedge clk); valid = 1; data = 8'h22; req = 0;
    @(posedge clk); valid = 1; data = 8'h33;
    @(posedge clk); valid = 1; data = 8'h44;
    @(posedge clk); valid = 0;
    #40;

    $display("\n=== SVA Sonu ===");
    $finish;
  end
endmodule

Kodun Açıklaması

• DUT davranışı: İlk always @(posedge clk or negedge rst_n) bloğu basit bir tasarımı modeller: gnt <= req (1 çevrim gecikmeli grant), ready <= valid (1 çevrim gecikmeli ready) ve error <= (data == 8'hFF) (0xFF'te hata).
• Immediate assertion'lar: assert_valid_data, data'nın belirsiz (x) olmadığını anlık kontrol eder ve ihlalde $warning üretir. assert_no_error_valid, error ile valid'in aynı anda aktif olmadığını denetler, ihlalde $error verir.
• sequence s_handshake: valid ##[1:3] ready — valid'ten 1-3 çevrim sonra ready gelmesini tarif eder. sequence s_burst: valid [*4] — valid'in 4 ardışık çevrim sürdüğü deseni tanımlar.
• Concurrent property'ler:
  • p_req_gnt: req |=> gnt — req'ten bir sonraki çevrimde gnt gelmeli.
  • p_valid_ready: valid |-> ##[1:3] ready — valid'ten sonra 1-3 çevrim içinde ready gelmeli.
  • p_reset_check: !rst_n |-> !gnt && !ready && !error — reset sırasında tüm çıkışlar sıfır olmalı (burada bilinçli olarak disable iff yoktur).
  • p_req_deassert: $fell(req) |=> $fell(gnt) — req düştüğünde sonraki çevrimde gnt de düşmeli.
  • p_handshake_no_error: s_handshake |-> !error — el sıkışma tamamlandığında hata olmamalı.
  • p_burst_leads_to_gnt: s_burst |-> ##[1:5] gnt — 4'lük burst sonrası 1-5 çevrim içinde gnt gelmeli.
• Etkinleştirme: Her property assert property (...) else $error(...) ile denetlenir. Ayrıca cover property (...) ifadeleri (p_req_gnt, s_handshake, s_burst) ilgili senaryonun gerçekten oluştuğunu raporlar.
• Stimulus (initial bloğu): Reset uygulanır; sırasıyla normal req/gnt, valid/ready el sıkışma, data=0xFF hata senaryosu ve 4 ardışık valid'lik burst testleri yürütülür. Burst testinde req bilinçli tetiklenir, çünkü p_burst_leads_to_gnt gnt üretimini gerektirir.

Önemli Noktalar

• |-> ve |=> ayrımı: |-> sonucu aynı çevrimde, |=> ise bir sonraki çevrimde bekler. Yanlış seçim, doğru tasarımı bile başarısız assertion ile raporlatır.
• disable iff ile reset koruması: Reset sırasında çıkışlar geçersizdir; disable iff (!rst_n) olmadan reset her assertion'ı sahte şekilde tetikleyebilir. Dikkat: p_reset_check bilerek bu korumayı kullanmaz, çünkü amacı tam da reset davranışını doğrulamaktır.
• cover ile boş test tuzağından kaçının: Bir assertion'ın hiç ihlal edilmemesi, senaryonun test edildiği anlamına gelmez. cover property senaryonun gerçekten gerçekleştiğini kanıtlar.
• Sequence'ler yeniden kullanılır: s_handshake ve s_burst birden çok property içinde tekrar kullanılır; bu, bakımı kolaylaştırır.
• Immediate vs concurrent yerleşimi: Immediate assertion'lar prosedürel blok içinde anlık; concurrent assertion'lar modül düzeyinde saat tabanlı çalışır. İhtiyaca göre doğru türü seçin.