[Assertion] Assertion to validate clock signals are in the required order

SystemVerilog
, ,
1

Given two clocks, CLKA and CLKB, phase shifted such that the two clocks don’t align and there is no overlap, Write an Assertion to verify CLKA posedge is always followed by CLKB posedge. My problem is how is the assertion written considering the edges don’t align for the two signals and how is the sampling handled in this case ?

CLK waves

2

In reply to Sri52:

This seems like an excellent interview/homework question. What was your answer?

3

Should we create a new ref_clk which has some relation to the two clk signals and use that as our sampling clk

assign ref_clk = clkA | clkB;

or create a new clock which has divide by relation to the slower of the two clocks and use it to sample?

4

In reply to Sri52:

Can you explain what you mean by having two clocks with different frequencies with no overlap?

Also, if there is always one CLKA posedge for every CLKB posedge, how can they be different frequencies?

5

In reply to dave_59:

CLK relationship

My question is incorrect. Considering the clock relationship as in the URL above. Two clocks same freq but phase shifted.

6

In reply to Sri52:

There must be some signal , which will be the source to generate either or both of these.That source can be used as the ref_clk. Can you provide the source clock diagram in the same URL provided above. So that ref_clk can be taken as golden and CLKA & CLKB can be verified through assertion.

Prashant

7

In reply to pk_94:

SO this assertion needs a reference clock to ensure the relationship between the two clocks ?

8

In reply to Sri52:

In reply to pk_94:
SO this assertion needs a reference clock to ensure the relationship between the two clocks ?

If we use ref_clk as suggested here, then we can write following assertion to check that WHEN clkA asserts THEN in next ref_clk cycle clkB asserts and clkA is not high.


assign ref_clk = clkA | clkB;
property clk_a_then_b;
    @(posedge ref_clk)
    $rose(clkA) |-> ##1 ($rose(clkB) && ~clkA);
endproperty

I am not sure if this is the correct solution for your question though.

9

In reply to bharat_vg:

As the assertions are evaluated in the preponed reason. So whenever there is posedge of ref_clk , means that at the same time clkA will rise ,Hence the value just before the rise of clkA is taken to be ZERO (everytime) as it remains high for only half cycle w.r.t ref_clk .So antecedent would never meet.

This assertion would vacuously pass.

10

In reply to Sri52:

Yes there should be some ref_clk according to me.