Multiple часы Assertion в SystemVerilog

Question

Вот Дизайн Код:

module mul_clock (input clkA, clkB, in, output out); 
    bit temp; 
    reg x[2:0]; 

    always @ (posedge clkA) 
    temp <= temp^in; 

    always @ (posedge clkB) 
    x <= {x[1:0], temp}; 

    assign out = x[2]^x[1]; 
endmodule 

Как написать утверждение для "Out", как это дизайн мульти-часы.

Я пробовал один, но все еще получаю некоторые ошибки. Пожалуйста, помогите мне, чтобы изменить это утверждение или написать еще одно:

property p1; 
    bit t; 
    bit x[2:0]; 

    @(posedge clkA) 
    (1'b1, t ^= in) |=> @(posedge clkB) (1'b1, x[0] = t) |=> @(posedge clkB) (out == x[2]^x[1], x[1] = x[0]) |=> @(posedge clkB) (out == x[2]^x[1], x[2] = x[1]); 
endproperty 

Примечание: С всегда блокировать и один тактовый утверждение, мы можем проверить из порта. Но я хочу сделать это с помощью утверждения multiclock без всякого блока, если это возможно.

Answer 1

Отказ от ответственности: Я не проверял это.

Вы пробовали:

#1 @(posedge clkA) (1'b1, t ^= in) |-> 
#2 @(posedge clkB) (1'b1, x[0] = t) |=> 
#3 @(posedge clkB) (out == x[2]^x[1], x[1] = x[0]) |=> 
#4 @(posedge clkB) (out == x[2]^x[1], x[2] = x[1]); 

То есть, с перекрытием импликации в часы передачи. По моему опыту, неперекрывающаяся импликация заставит утверждение пробовать не на следующем clkB, а пропустить один clkB, а затем образец на clkB.

Кроме того, я не совсем понимаю, почему вы используете последствия полностью через свое утверждение. Строка №2 не является обязательным условием для строки №3, и то же самое можно сказать и для строки №3 и строки №4. То, как я прочитал это утверждение, должно начинаться с каждого clkA, а затем последовательность будет всегда. В этом случае было бы более правильным, хотя предыдущий код мог бы работать.

@(posedge clkA) 
    (1'b1, t ^= in) |-> 
@(posedge clkB) 
    (1'b1, x[0] = t) ##1 
    (1'b1, x[1] = x[0]) ##1 
    (out == x[2]^x[1], x[2] = x[1]); 

И наконец, что произойдет, если clkA намного быстрее clkB? Несколько утверждений начнутся параллельно и не согласятся на фактическое значение t в первом предложении clkB. Я должен признать, что я неясен в области определения значений, локальных для свойства, но проверьте, не вызывает ли это вас неприятности. Возможным решением может быть объявление переменной t вне области свойств. Таким образом, t будет обновляться до нового значения в каждом posedge clkA, и вы будете иметь n утверждения, проверяющие одно и то же (что не является проблемой).

Редактировать: Я удалил out == x[2]^x[1] чек из строки № 3, потому что x является локальным для собственности. Таким образом, вы не можете проверить значение, сделанное другим экземпляром этого утверждения.

Дополнение: Если вышеуказанное не работает или если для запуска параллельных утверждений, проверяющих одно и то же, кажется, что следующий код может работать.

Edit2: Поместите свойство x внутри и измените две последние строки в свойстве, чтобы обновить x, чтобы исправить значения.

bit t; 
always_ff@(posedge clkA) 
    t ^= in; 

property p1; 
bit[2:0] x; 
@(posedge clkB) 
    (1'b1, x[0] = t) |=> 
    (1'b1, x[1] = x[0]) ##0 (1'b1, x[0] = t) ##1 
    (1'b1, x[2] = x[1]) ##0 (1'b1, x[1] = x[0]) ##0 out == x[2]^x[1]; 
endproperty 

Дополнительный совет в конце: триггеров, созданных должны иметь сбросы. То есть, как x, так и temp должны быть сброшены локально в свои отдельные тактовые домены. Сброс может быть синхронным или асинхронным по вашему выбору. Это также должно быть добавлено в вашу собственность. Также: всегда используйте always_ff или always_comb, никогда не используйте всегда.

асинхронный сброс:

always_ff @ (posedge clkA or posedge arstClkA) 
if(arstClkA) 
    temp <= 0; 
else 
    temp <= temp^in;