Если последовательность возникает, то внутри нее возникают подпоследовательности в утверждениях System-Verilog

Question

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

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

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

, но это не похоже на работу для моего примера.

Я прочитал, что:

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

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

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

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

Answer 1

Вы считаете правильным, что последовательный оператор |-> запускается после того, как 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.