Утверждение для действительного приходит один раз в транзакции req-ack

Я предполагаю, что под «ошибкой» вы подразумеваете ошибку компиляции. Левая часть оператора throughout может быть только логическим значением, а не последовательностью. Вы думаете об операторе intersect.

intersect потребует, чтобы последовательности слева и справа имели одинаковое количество циклов.

Последовательность слева от intersect должна указывать, что существует один и только один цикл, где valid равно 1. Оператор непоследовательного повторения — хорошее начало, потому что он говорит, что valid может появиться в любом цикле, начиная с момента начала последовательного совпадения. Не сказано, что происходит после этого; он просто говорит, что могут существовать последующие циклы, но не предъявляет никаких требований к этим циклам.

Вам нужно указать, что происходит после цикла, где valid равно 1. Чтобы убедиться, что существует единственный цикл, где valid равно 1, мы должны проверить, что valid равно 0 для последующих циклов. Делается это с помощью следующей последовательности:

!valid [*] ##1 valid ##1 !valid[*]

Это можно было бы написать несколькими способами, но я считаю код выше наиболее читаемым.

В другой части консеквента вы можете смело отбросить термин (req && !ack) и просто сказать:

##[1:$] (!req && !ack)

Он также не делает того, что, как я думаю, вы хотите (убедитесь, что req остается 1, пока не наступит ack). У вас должно быть другое утверждение, которое проверяет, что req должно оставаться 1. Это упростит отладку, потому что вы разделяете проверки для valid и проверки для req и ack.

Собрав все вместе, утверждение должно выглядеть так:

assert property (@(posedge clk_r)
    req & ~ack |->
        (!valid [*] ##1 valid ##1 !valid [*]) within (##[1:$] (!req && !ack));

Примечание: вы должны использовать логические операторы вместо побитовых логических операторов. Вместо & используйте &&, а вместо ~ используйте !.