SVA недвижимости для простого сигнала

Question

осциллограмм: -

Я сделал собственность как:

property p1; 
    a |=> (b == 1)[=2] ##1 (c == 1)[=2] 
endproperty 

Но это свойство не работает хорошо для этой волны, это ISN «Работает на 3 или более« б »до« c »и не работает для« c »после первого« b ».

Мне нужно свойство, которое может пройти только после сигнала «a» всего 2 «b» и после «2 c» с любым количеством промежутков между ними.

благодарит за помощь.

Answer 1

Вы не указываете, что b не должно быть 1, если во время импульсов на c, и вы не указываете, что c не должен быть 1 во время импульсов на b.

Итак, как о чем-то вроде этого:

property p1; 
    a |=> ((c == 0) throughout (b == 1)[->2]) ##1 ((b == 0) throughout (c == 1)[->2]); 
endproperty 

Оператор [->N] является точных непоследовательных оператора повторения или Гото оператора повторения. С повторением goto выражение должно сохраняться в последнем цикле матча; другими словами, совпадение достигается, как только указанное количество повторений происходит.