Verilog 17 : Assertions in – OVL, PSL, and FIFO Verification

Chapter 1: Introduction to Assertions

1.1 What are Assertions?

• Definition: Assertions are statements in HDL that check if a design behaves as expected during simulation.

• They do not change the design behavior, but monitor it.

• Think of them as automatic examiners: they raise an alert if something goes wrong.

Example Analogy:

• Imagine a traffic light controller.

• Assertion: “The red and green lights should never be ON at the same time.”

• If violated, simulation stops or logs a warning.

---

1.2 Assertion Languages

• SystemVerilog Assertions (SVA) – built-in assertions in SystemVerilog

• Open Verification Library (OVL) – a library of reusable assertion modules

• Property Specification Language (PSL) – industry-standard assertion language

---

1.3 Advantages of Using Assertions

1. Early Detection of Bugs: Catches design violations during simulation.

2. Self-Checking Testbenches: Reduces manual verification effort.

3. Reusable Verification Components: Assertions can be reused across projects.

4. Improved Reliability: Monitors design invariants automatically.

---

1.4 Implementing Assertion Monitors

1. Add assertion statements in RTL or separate monitor modules.

2. Assertions can trigger warnings, errors, or simulation stop.

3. Often used in FIFO, bus protocols, and control logic verification.

---

1.5 What You Need

• Simulator supporting assertions (VCS, Modelsim, NCSim)

• RTL code of design under test (DUT)

• Testbench generating stimulus

---

Chapter 2: Verification of FIFO Using Assertions

2.1 FIFO Model

• FIFO (First-In-First-Out) stores data temporarily.

• Properties to check using assertions:

  • FIFO should not overflow

  • FIFO should not underflow

  • Data comes out in the same order as input

Basic FIFO Signals:

• clk – clock

• rst – reset

• write_enable, read_enable

• data_in, data_out

• full, empty

---

2.2 RAM Model

• FIFO is implemented using RAM array.

• Write pointer increments on write, read pointer increments on read.

• Assertions can check pointer limits to detect overflow/underflow.

---

2.3 Testbench Code

• Generate write and read patterns.

• Include reset and clock generation.

• Assertions monitor FIFO during simulation.

module fifo_tb;
  reg clk, rst;
  reg wr_en, rd_en;
  reg [7:0] data_in;
  wire [7:0] data_out;
  wire full, empty;

  // Instantiate FIFO DUT
  fifo my_fifo(clk, rst, wr_en, rd_en, data_in, data_out, full, empty);

  initial begin
    clk = 0; rst = 1; wr_en = 0; rd_en = 0; data_in = 0;
    #5 rst = 0;
    // Write some data
    #10 wr_en = 1; data_in = 8'hA5;
    #10 wr_en = 1; data_in = 8'h5A;
    #10 wr_en = 0;
    // Read data
    #10 rd_en = 1;
    #20 $finish;
  end

  always #5 clk = ~clk; // Clock generation
endmodule

---

Chapter 3: Assertion with OVL (Open Verification Library)

3.1 What is OVL?

• OVL is a library of pre-built assertions.

• Common assertions:

  • ovl_always – asserts a condition always holds

  • ovl_never – asserts a condition never occurs

  • ovl_cover – collects coverage metrics

Advantages:

• Reduces manual coding

• Provides tested, reusable assertion modules

• Works with multiple simulators

---

3.2 Assertion in RTL

`include "ovl_pkg.sv"

module fifo_with_ovl(
  input clk,
  input rst,
  input wr_en,
  input rd_en,
  output full,
  output empty
);

  // FIFO implementation
  // ...

  // OVL assertion: FIFO should not overflow
  ovl_never #(.msg("FIFO Overflow!")) fifo_overflow_chk (
    .clk(clk),
    .reset_n(~rst),
    .test_expr(~full | ~wr_en)
  );

endmodule

---

3.3 Simulator Output

[OVL] Time 20: FIFO Overflow! Assertion violated.
Simulation stopped.

• Provides immediate feedback if FIFO violates constraints.

---

3.4 OVL Assertion List

• ovl_always – condition always true

• ovl_never – condition never occurs

• ovl_cover – used for coverage

• ovl_edge – detect rising/falling edges

• ovl_event – detect sequence of events

---

Chapter 4: Assertion with PSL (Property Specification Language)

4.1 What is PSL?

• PSL is an industry-standard assertion language.

• Used to specify temporal properties of designs.

• Can be embedded directly in RTL or in separate PSL files.

PSL Example:

// Check FIFO never overflows
property no_overflow;
  always (wr_en -> !full);
endproperty

assert property (no_overflow);

---

4.2 Assertion in RTL (PSL)

module fifo_with_psl(
  input clk,
  input rst,
  input wr_en,
  input rd_en,
  output full,
  output empty
);

  // FIFO implementation
  // ...

  // PSL assertion: FIFO underflow never occurs
  assert always (rd_en -> !empty);

endmodule

---

4.3 Simulator Output

[PSL] Time 25: Assertion failed: FIFO underflow occurred
Simulation terminated.

• PSL provides powerful temporal property checking.

• Detects complex sequences and timing violations.

---

4.4 Post-Processing

• Assertion failures can be logged to files.

• Coverage reports can be generated using PSL/OVL tools.

• Useful for verification sign-off in ASIC/FPGA projects.

---

Chapter 5: Step-by-Step Guide for Beginners

1. Understand the design: Identify critical signals (full, empty, read/write).

2. Choose assertion language: OVL for simplicity, PSL for temporal properties.

3. Write assertions in RTL or separate modules.

4. Create a testbench: Generate stimulus for your FIFO or module.

5. Run simulation: Check assertion outputs and logs.

6. Post-process: Analyze coverage and failures, refine testbench.

---

Chapter 6: Tips for Exam-Perfect Learning

• Memorize common assertion types (always, never, cover).

• Understand FIFO behavior thoroughly.

• Practice writing both OVL and PSL assertions.

• Simulate and inspect waveforms for assertion failures.

• Link assertions to testbench stimulus to detect corner cases.

---

7. Summary

• Assertions are automatic monitors in HDL.

• OVL provides pre-built assertion modules.

• PSL allows temporal property specification.

• Verification of FIFO using assertions ensures correct data flow.

• Good practice: Assertions + Testbench + Coverage = robust design verification.