[systemverilog] assert, property

systemverilog에서는 검증을 위해 프로그래밍적 요소가 많이 추가 되었는데, 대표적인것이 assert와 property 입니다.

 

assert는 우리가 프로그래밍 할 때 사용하는 assert와 동일 합니다.

 

assert(data_1 == data_2) // data_1과 data_2가 같지 않다면 에러를 발생시킨다

위의 코드를 실제로 돌리면 어떻게 나오는지 코드를 아래와 같이 작성했습니다.

initial begin
   assert(data == data_t) else $fatal("Stop");
   fork
        data_gen(data);
        data_gen_t(data_t);
    join 
end
always #(`Clock_period/2)  clk = !clk;

task automatic data_gen_t(ref logic [2:0] t_data);
    @(posedge clk);   t_data    =   3'd1;
    @(posedge clk);   t_data    =   3'd2;
    @(posedge clk);   t_data    =   3'd4;
    @(posedge clk);   t_data    =   3'd4;
    @(posedge clk);
endtask

task automatic data_gen(ref logic [2:0] wdata);
    @(posedge clk); wdata    =   3'd1;
    @(posedge clk); wdata    =   3'd2;
    @(posedge clk); wdata    =   3'd3;
    @(posedge clk); wdata    =   3'd4;
    @(posedge clk);
endtask

이렇게 할 경우 3번째에서 같지 않기 때문에 아래와 같은 결과가 나옵니다

 

추가적으로 property는 timing을 assert문에 넣는 것이 가능합니다

 

예를 들어 '2clk 이내에 값이 5으로 되어야 한다'라는 timing을 assert property 구문을 통해 적용할 수 있습니다.

 

www.design-reuse.com/articles/10907/using-systemverilog-assertions-in-rtl-code.html

Using SystemVerilog Assertions in RTL Code

이 글을 참조하여 실험을 해봤는데

 

data는 매 clock 1씩 증가하는 counter 입니다.

property data_1_5;
    @(posedge clk) data==1 |-> ##[1:2] data==5;
endproperty
data_1_5_test : assert property(data_1_5) else $warning("error gen");

initial begin
    clk = 1'b0;
    rst_b = 1;
    #100 rst_b = 0;
    #10  rst_b = 1;
    #100 rst_b = 0;
    #10  rst_b = 1;
end
always #(`Clock_period/2)  clk = !clk;
always @(posedge clk or negedge rst_b) begin
    if(!rst_b) begin
        data <= 3'd0;
    end else if(data != 3'd7) begin
        data <= data + 3'd1;
    end
end

 

이렇게 짰을 경우 data가 1인 시점부터 1~2clock 이내에 data가 5로 바뀌어야 한다는 조건 이지만,

 

해당 조건은 발생하지 않기 때문에 assert 조건에 걸리게되어 아래와 같이 출력문을 보여줍니다

여기서 error가 2번 발생하는 이유는 rst_b 신호에 의해 data가 0으로 초기화되는 것이 2번 발생하기 때문입니다.

 

---

A|->B, A|=>B 의 차이점은 

 

A|->B 는 A 발생한 시점 부터 event를 추적하며, A|=>B는 A 발생한 시점 다음부터 event를 추적합니다.

 

예를 들어 위의 code 에서 아래와 같이 바꾸어도 warning은 출력이 되지 않습니다

 

property data_1_5_A;
     @(posedge clk) data==1 |-> ##[1:4] data==5;
endproperty

 property data_1_5_B;
     @(posedge clk) data==1 |=> ##[1:3] data==5;
 endproperty