SVA使用实例，包括RTL ,TB，bin

SVA（SystemVerilog Assertions）是一种用于验证硬件设计的语言，可以在RTL（Register Transfer Level）代码和Testbench（TB）中使用。下面是一个完整的SVA验证流程，包括RTL代码、TB代码和二进制文件（bin）。

1. RTL代码

假设我们有一个简单的计数器模块，它有四个输入信号：时钟信号`clk`、复位信号`rst_n`、计数使能信号`en`和计数方向信号`dir`，以及一个输出信号`cnt`，表示计数器的当前值。我们要验证的功能是，当计数器达到最大值时，它会自动清零并重新开始计数。下面是该模块的RTL代码：

module counter(
   input logic clk,
   input logic rst_n,
   input logic en,
   input logic dir,
   output logic [7:0] cnt
);

   logic [7:0] tmp_cnt;
   
   always_ff @(posedge clk or negedge rst_n) begin
      if (!rst_n) begin
         tmp_cnt <= 8'h0;
      end else begin
         if (en) begin
            if (dir) begin
               tmp_cnt <= tmp_cnt + 1;
            end else begin
               tmp_cnt <= tmp_cnt - 1;
            end
         end
      end
   end
   
   assign cnt = tmp_cnt;
   
endmodule

2. TB代码

下面是一个简单的Testbench，用于验证计数器模块的功能。在测试中，我们将计数器的最大值设置为255，然后将计数器递增直到达到最大值。当计数器达到最大值时，我们期望它会自动清零并重新开始计数。下面是该TB代码：

module tb_counter;

   logic clk;
   logic rst_n;
   logic en;
   logic dir;
   logic [7:0] cnt;
   
   counter dut(
      .clk(clk),
      .rst_n(rst_n),
      .en(en),
      .dir(dir),
      .cnt(cnt)
   );
   
   initial begin
      clk = 1'b0;
      rst_n = 1'b0;
      en = 1'b0;
      dir = 1'b0;
      
      #5 rst_n = 1'b1;
      #10 en = 1'b1;
      #50 dir = 1'b1;
      #200 $finish;
   end
   
   always #5 clk = ~clk;
   
endmodule

3. bin文件

在TB中，我们需要使用SVA来验证计数器的功能。下面是一个简单的SVA代码，用于验证计数器是否能够正确地清零并重新开始计数。

module sva_counter;

   logic clk;
   logic rst_n;
   logic en;
   logic dir;
   logic [7:0] cnt;
   
   counter dut(
      .clk(clk),
      .rst_n(rst_n),
      .en(en),
      .dir(dir),
      .cnt(cnt)
   );
   
   initial begin
      $dumpfile("tb.vcd");
      $dumpvars(0, tb_counter);
      $monitor("time=%t cnt=%h", $time, cnt);
   end
   
   // Assertion to check if counter resets to 0 when it reaches 255
   property p_reset;
      @(posedge clk)
      disable iff (!rst_n)
      (cnt == 8'hFF) |-> (cnt == 8'h0);
   endproperty
   
   // Check all properties
   assert property (p_reset);
   
   // Simulate the design
   initial begin
      clk = 1'b0;
      rst_n = 1'b0;
      en = 1'b0;
      dir = 1'b0;
      
      #5 rst_n = 1'b1;
      #10 en = 1'b1;
      #50 dir = 1'b1;
      #200 $finish;
   end
   
   always #5 clk = ~clk;
   
endmodule

4. 验证流程

我们使用以下命令来编译和运行验证流程：

iverilog -o tb_counter.vvp counter.v tb_counter.v sva_counter.v
vvp tb_counter.vvp -lxt2
gtkwave tb.vcd

第一个命令将RTL代码、TB代码和SVA代码编译成一个可执行文件`tb_counter.vvp`。第二个命令运行验证流程，并将输出保存到`tb.vcd`文件中。最后一个命令使用`gtkwave`软件打开`tb.vcd`文件，以便我们可以查看验证结果。

在验证过程中，我们可以看到计数器的值递增直到达到最大值255，然后自动清零并重新开始计数。同时，SVA代码中的断言`p_reset`也被验证为正确。这意味着计数器能够正确地清零并重新开始计数，符合我们的设计要求。