Если последовательность встречается, то в утверждениях System-Verilog в ней встречается подпоследовательность.

Я хочу сказать: «если последовательность A встречается, то последовательность B встречается в этой последовательности». Как я могу это сделать?

Я бы подумал, что могу использовать утверждение:

assert property (@(posedge clk) (A |-> (B within A));

но в моем примере это не работает.

Я читал это:

Говорят, что линейная последовательность соответствует на протяжении конечного интервала последовательных тактов часов при условии, что первое логическое выражение оценивается как истинное в первом такте часов, второе логическое выражение оценивается как истинное при втором такте часов и так далее, вплоть до последнее логическое выражение, принимающее истинное значение на последнем такте часов.

но я подозреваю, что такт часов перешел на другую сторону |-> последнего такта часов, когда я хочу, чтобы он был первым.

Мой конкретный пример - это аккумулятор, который, как я ожидаю, переполнится, если я добавлю достаточно положительных чисел, поэтому мне нужны A = (input == 1)[*MAX_SIZE] и B = (output == 0), поэтому здесь B - это последовательность длины 1, я не знаю, вызывает ли это проблемы.

Я очень новичок в system-verilog, поэтому, возможно, что-то другая часть моего кода работает неправильно, но я нигде не видел, чтобы этот пример был выполнен.


system-verilog system-verilog-assertions
person R.Mckemey    schedule 09.12.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы правы, что консеквент в операторе |-> запускается после того, как A уже совпал. Вы хотите заглянуть в прошлое: «когда-то я видел A, видел ли я B within A?».

Для этого вы можете использовать свойство triggered последовательности:

sequence b_within_a;
  @(posedge clk)
    B within A;
endsequence

assert property (@(posedge clk) A |-> b_within_a.triggered);

Последовательность b_within_a будет соответствовать точно в конце A, конечно, если B также произошло, когда свойство triggered будет оцениваться как 1.

Обратите внимание, что для последовательности b_within_a часы определены специально. Это требование LRM, иначе вам не будет разрешено вызывать triggered по нему.

person Tudor Timi    schedule 09.12.2016
comment
Что, если B within A будет завершен раньше, чем A? Я имею в виду, что B within A = B должен находиться внутри A и, следовательно, он будет завершен, как только B перейдет с 1 на 0, в то время как A все еще активен, но еще не завершен. - person Karan Shah; 10.12.2016
comment
Значит, вы не удовлетворили часть within A, и последовательность еще не будет соответствовать. - person Tudor Timi; 10.12.2016
comment
Да, это правда, потому что согласно LRM B within A означает (1[*0:$] ##1 B ##1 1[*0:$]) intersect A. - person Karan Shah; 11.12.2016
comment
Спасибо вам обоим. Мне нужно было добавить @(posedge clk) в объявление моей последовательности, пока я не получал This sequence method does not have a clock.. Я получил эту идею из другого сообщения @TudorTimi: http://stackoverflow.com/questions/39876386/reset-awareness-when-using-sequence-triggered-in-assertion - person R.Mckemey; 12.12.2016
comment
@ R.Mckemey Это был мой недосмотр. LRM действительно требует, чтобы вы явно определяли часы, если вы хотите использовать свойство последовательности triggered. - person Tudor Timi; 12.12.2016