Могу ли я сгенерировать несколько свойств SystemVerilog в цикле?

У меня есть два упакованных массива сигналов, и мне нужно создать свойство и связанное с ним утверждение для этого свойства, которое доказывает, что два массива идентичны при определенных условиях. Я формально проверяю, и инструмент не может проверить оба полных массива в одном свойстве, поэтому мне нужно разделить его на отдельные элементы. Итак, есть ли способ сгенерировать свойства для каждого элемента массива с помощью цикла? На данный момент мой код очень многословен и сложен в навигации.

Мой код в настоящее время выглядит так:

...
property bb_3_4_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][4] == bb_rtl [3][4] ;
endproperty

property bb_3_5_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][5] == bb_rtl [3][5] ;
endproperty

property bb_3_6_p; 
  @(posedge clk)
     bb_seq  
     |=>     
     bb_exp [3][6] == bb_rtl [3][6] ;
endproperty
...

...
assert_bb_3_4: assert property (bb_3_4_p);
assert_bb_3_5: assert property (bb_3_5_p);
assert_bb_3_6: assert property (bb_3_6_p);
...

Вот как я хотел бы, чтобы мой код выглядел так:

for (int i = 0; i < 8; i++) 
  for (int j = 0; j < 8; j++) 
  begin   
     property bb_[i]_[j]_p;
        @(posedge clk)
           bb_seq  
           |=>     
           bb_exp [i][j] == bb_rtl [i][j] ;
     endproperty
     assert_bb_[i]_[j]: assert property (bb_[i]_[j]_p);
  end

properties verilog system-verilog formal-verification system-verilog-assertions
person WestHamster    schedule 17.10.2012    source источник
comment
Можете ли вы опубликовать код? Это все в процессуальном контексте?   -  person    schedule 17.10.2012
comment
Свойства и утверждения находятся внутри модуля. Я думаю, вам, возможно, придется поместить циклы в всегда блок, в который я не думаю, что вы можете поместить свойства.   -  person WestHamster    schedule 18.10.2012

Ответы (2)


arrow_upward
14
arrow_downward

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

module
...
property prop1(signal1,signal2); 
  @(posedge clk)
     bb_seq  
     |=>     
     signal1 == signal2 ;
endproperty
...
generate
for (genvar i = 0; i < 8; i++) 
  for (genvar j = 0; j < 8; j++) 
    begin : assert_array
    assert property (prop1(bb_exp[i][j],bb_rtl[i][j]));
    end
endgenerate
... 
endmodule

Вы также можете встроить свойство в утверждение:

module
...
generate
for (genvar i = 0; i < 8; i++) 
  for (genvar j = 0; j < 8; j++)
    begin : assert_array
    assert property (@(posedge clk) bb_seq |=> bb_exp[i][j] == bb_rtl[i][j]);
    end
endgenerate
...
endmodule
person Community    schedule 18.10.2012
comment
Это прекрасно работает. Большое тебе спасибо. Следующая проблема, с которой я теперь столкнулся, заключается в том, как пометить эти сгенерированные свойства: утверждения терпят неудачу, но я не могу понять, какое утверждение было нарушено утверждением. - person WestHamster; 19.10.2012
comment
ОБНОВЛЕНИЕ: теперь я могу определить имя/номер утверждения в моем формальном инструменте. Однако, если вы знаете какой-либо полезный совет по именованию утверждений, тогда я весь слушаю. - person WestHamster; 19.10.2012
comment
Если вам нужен больший контроль над отчетами, вы можете добавить в утверждение блок действий. Что-то вроде assert property (...) else $display("Assertion %m failed"); Если вы хотите использовать label : для ссылки на утверждение, я рекомендую добавить begin : имя_массива ... end во внешний цикл генерации, чтобы инструмент не не используйте genblkX[i]. - person ; 19.10.2012

arrow_upward
0
arrow_downward

Вы также можете попробовать то же самое с макросом.

/*Start of macro*/
`define bb_prop(Num1, Num2) \
    property bb_``NUM1``_``NUM2``_p; \
      @(posedge clk) \
      bb_seq |=> bb_exp [``NUM1``` ][``NUM2``] == bb_rtl [``NUM1``` ][``NUM2``]; \
    endproperty \
 bb_prop_``NUM1``_``NUM2``_assert: assert property (bb_``NUM1``_``NUM2``_p) 
/* End of macro*/

`bb_prop(3,4) 
`bb_prop(3,5)
`bb_prop(3,6)
person aravind_sindhey    schedule 23.10.2019