SVA Повторение непоследовательных Операция Отборочные события

Question

я следующее свойство:

property p; 
    @(posedge clk) a |=> b[=2] ##1 c; 
endproperty 

Это говорит нам, что если a утверждается, начните со следующего clk, b следует утверждать, не последовательно два раза с последующим по c утверждается в любое время после последнего b.

Мой вопрос в том, что если c утверждается между первым b и вторым b. Должно ли утверждение терпеть неудачу немедленно или продолжаться? В некоторых справочниках говорится, что это должно потерпеть неудачу, но я в этом сомневаюсь. Каково ожидаемое поведение?

Answer 1

[= или непоследовательный оператор повторения аналогичен Гото повторению, но выражение не должно быть истинным в тактовом цикле, прежде чем c верно.

Скажем, a утверждается. Условие импликации : удовлетворено и далее оценивается утверждение.

После b не проверяется два раза, независимо от того, чтоc есть. После того, как b является , установлено, что для двух непереходных тактовых краев, после этогоc проверяется после 1-тактного цикла (из-за ##1).

Если c является утверждал и -де-утверждал когда b является проверяется на 2 раза, то, что переключение является не считается. Что из c считается после 2 утверждения b.

После шнапс должен дать четкое представление:

Passing оснастки:

Сбой оснастки:

Здесь, несмотря на то, был глюк в c , утверждение не прошло.

Для получения более подробной информации обратитесь к A Practical Guide for SystemVerilog Assertions pdf. Doulos tutorial также является хорошим.

Answer 2

Короче говоря, да, это пройдет. Независимо от того, где c утверждается, после наблюдения двух «b», он будет ждать c == 1. Итак, если c был 1 с самого начала и никогда не доходит до нуля, он тоже пройдет.

Еще один момент, чтобы сделать это, когда это утверждение действительно потерпит неудачу. Он пройдет, когда будет утверждён c, но если нет, он будет продолжать работать до конца теста! Вы увидите сбой только в конце моделирования.