Как покрыть свойство fifo rd/wt?

Я пытаюсь написать точку прикрытия fiford rd write.

module M;

  bit stop;  bit clk; initial while (!stop) #5 clk = ~clk;

  bit A, B, rst;

  initial rst = 0;

  initial begin
    A = 0;
    #20 A = 1;
    #10 A = 0;
    // #10 B = 1;
    #10 B = 0;
    #50 stop = 1;
  end


  // sequence fifo_rd_wt_s(reg sig);
  //  ((|A === 1) |-> s_eventually (|B === 1));
  // endsequence: fifo_rd_wt_s

  property fifo_rd_wt_p(reg sig_clk, reg sig_rst);
    @(posedge sig_clk) disable iff(sig_rst)
    ((|A === 1) |-> s_eventually (|B === 1));
  endproperty: fifo_rd_wt_p


  cover_fifo_read_write: cover property(fifo_rd_wt_p(clk, rst)) $error($sformatf("%0t hit fifo read write", $time)); 
      // else $error($sformatf("%0t did not hit", $time));



   final
     $display("Finished!");

endmodule: M

В журнале выполнения я вижу, что он запускается каждый цикл, но это не то, что я хочу. Я хочу, чтобы он срабатывал каждый раз, когда видит A, за которым следует B.

Не уверен, что мне не хватает.

Я нашел нечто подобное здесь

Код присутствует в коде.


system-verilog system-verilog-assertions
person justrajdeep    schedule 19.10.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я думаю, что ваша проблема связана с последствиями. Я использовал ваш пример и заменил на strong((|A === 1) ##[1:$] (|B === 1)); он работал нормально.

Покрытие с импликацией может иметь неожиданное поведение (в вашем случае это было покрытие антецедента), всегда безопаснее использовать покрытие с последовательностями.

person Viktorinox    schedule 22.10.2018