SVA: Verify stable signal in different clock domain

Question

My problems is perfectly described in the following paper "Asynchronous Behaviors Meet Their Match with SystemVerilog Assertions":

Consider the scenario in Figure 8 where the strobe signal is generated in the src_clk domain and must be stable for at least 3 cycles in the dst_clk domain. An assertion must check that the strobe signal remains stable but also that it has the adequate setup and hold time to be sampled in the dst_clk domain.

Figure 8

The author then suggest the following assertion to overcome this problem:

assert property (
    @(posedge src_clk) $rose(strobe) |-> (
        strobe[*1:$] ##1 1 )
    ) intersect (
        ##1 @(posedge dst_clk) strobe[*3]
        ##1 @(posedge src_clk) 1
    )
 );

My problem is that both Cadence incisive 15.20 and Synopsys VCS 2014.10 complains about the use of multiple clocks inside an intersect:

Incisive 15.20: Invalid operator and/or operands in multi-clock context.

Synopsys VCS 2014.10: Single-clocked sequence expected in right operand of 'intersect' operator, multi-clocked sequence found.

https://www.edaplayground.com/x/wGE

It does however work when I compile using Aldec Riviera Pro 2017.02, so I'm guessing this is just a tool limitation.

Are there any other alternative ways of achieving this?

Ayalo Ayalo · Accepted Answer · 2020-06-30T07:56:02

I find it helpful to use glue logic to avoid complex properties.

In this case I'd count dst_clk clocks and do this:

unsigned reg [7:0] dst_clk_conter_width;
parameter counter_width = 256;

always @(posedge dst_clk) 
  dst_clk_counter <= dst_clk_counter +1;

property prop;
  @(posedge src_clk or posedge dst_clk)
  $rose(strobe) |-> 
    (1,strobe_rise_dst_clk_num = dst_clk_counter) 
    ##[1:$] strobe
    ##1 strobe && (dst_clk_counter  = (strobe_rise_dst_clk_num + 3) % counter_width)
endproperty

Explanation:

first line captures current counter value, second line makes sure strobe doesn't drop and last line checks that we passed 3 dst clocks already

SVA: Verify stable signal in different clock domain

1 Answers