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: data'nin hicbir biti x/z olmamali
      // (data !== 8'hxx yazmak yalnizca TUM bitler x ise yakalar; $isunknown her biti denetler)
      assert_valid_data: assert (!$isunknown(data))
        else $warning("[%0t] Data belirsiz (x/z)!", $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, $isunknown(data) ile data'nın herhangi bir bitinin x/z olmadığını anlık kontrol eder ve ihlalde $warning üretir. (data !== 8'hxx yazımı yalnızca sekiz bitin tamamı x olduğunda yakalardı; tek biti belirsiz bir veri gözden kaçardı.) 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.
• Assertion'lar da örneklemeyi Preponed bölgede yapar: Concurrent assertion'lar sinyalleri saat kenarından hemen önceki değerleriyle (clocking block'un #1step girişi gibi) okur. Bu yüzden always @(posedge clk) içinde <= ile güncellenen bir sinyal, assertion tarafından bir sonraki kenarda görülür. req |=> gnt ifadesinin "bir çevrim sonra" demesi tam da DUT'un bu NBA gecikmesine karşılık gelir.
• Hata mesajlarında $sampled ve $past: Action block içinde $sampled(sig) örneklenen değeri, $past(sig, n) ise n çevrim önceki değeri verir; hata ayıklamada "ihlal anında ne vardı?" sorusunu yanıtlar.
• Bu örnekte assert_no_error_valid ihlali beklenir: Hata testinde data=0xFF ile valid=1 aynı anda sürülür; bir çevrim sonra error=1 olur ve valid hâlâ 1'dir. Bu bilinçli bir "tasarım hatası" sahnesidir; $error mesajını görmek assertion'ın çalıştığının kanıtıdır.

SVA Operatörleri Hızlı Referans

Benzetme: Assertion, tasarımın yanına oturttuğunuz yorulmaz bir denetçidir. Her saat kenarında defterine bakar: "req geldi, bir çevrim sonra gnt geldi mi?" Gelmezse anında düdük çalar. Siz dalga formunda saatlerce aramazsınız; denetçi ihlalin hangi çevrimde olduğunu söyler. cover ise denetçinin "bu senaryo gerçekten yaşandı" diye attığı tiktir.

assert, assume, cover, expect

Sık Yapılan Hatalar

• |-> ile |=>'yi karıştırmak: req |-> gnt aynı çevrimde gnt ister; DUT bir çevrim gecikmeli üretiyorsa doğru tasarım hatalı raporlanır.
• disable iff unutmak: Reset sırasında çıkışlar geçersizdir; assertion sahte ihlal üretir. Reset davranışını test eden property hariç, hepsinde kullanın.
• Sonsuz üst sınırlı sequence'leri kontrolsüz bırakmak: req |-> ##[1:$] gnt ifadesi gnt hiç gelmezse asla başarısız olmaz (simülasyon biter, assertion "bekliyor" kalır). Üst sınırı makul bir sayıyla (##[1:100]) sınırlayın.
• x kontrolünü !== 8'hxx ile yapmak: Yalnızca tüm bitler x ise yakalar. $isunknown() kullanın.
• Immediate assertion'ı initial dışında saat olmadan yazmak: Kombinasyonel bir always_comb içinde immediate assertion, sinyal geçişleri sırasında (glitch) sahte tetiklenebilir. Zamanlı kontroller için concurrent assertion seçin.
• cover yazmamak: Hiç ihlal edilmeyen bir assertion, senaryonun hiç oluşmadığı anlamına da gelebilir. Her kritik property için bir cover ekleyin.

Kendinizi Deneyin

1. p_req_gnt'yi req |-> gnt yapın (örtüşen). Hangi testlerde ihlal aldınız? DUT'un 1 çevrimlik gecikmesiyle ilişkilendirin.
2. p_valid_ready'den disable iff (!rst_n) ifadesini silin ve reset sırasında sahte ihlal görünüp görünmediğini kontrol edin (ipucu: valid reset sırasında 0 olduğu için belki görünmez; valid=1 iken reset uygulayıp tekrar deneyin).
3. property p_data_stable; @(posedge clk) disable iff (!rst_n) valid && !ready |=> $stable(data); endproperty ekleyin: "ready gelmeden data değişmemeli". Stimulus'ta data'yı erken değiştirerek ihlali tetikleyin.
4. cover property (@(posedge clk) req ##1 gnt ##1 !gnt) ekleyin ve kaç kez gerçekleştiğini sayın. [->n] operatörünü kullanarak "üçüncü gnt" anını yakalayan bir cover yazın.