Help me write an assume assertion of my handshake protocol

SystemVerilog
1

I want to express my original handshake logic in assume assertion.

Handshake protocol is as follows:

  • req/ack handshaking
  • If req is asserted, MOD_B asserts ack in 0(immediately) to 12 clocks.
  • If req is deasserted, MOD_B deasserts ack in 0(immediately) clock.
  • There exist a case where req is deasserted arbitrary even when ack has not been asserted.
  • ack is never asserted when no req is asserted.

connection

| -- req --> |
 MOD_A| <--ack --  | MOD_B

waveform example

  • case1 (basic case)
req _____/~~~~~~~~~~~~~~~~\______
 ack ___________/~~~~~~~~~~~\_____
          |<--->| ... 0 - 12 clocks interval
  • case2 (req deasserted before assertion of ack)
req _____/~~~~~~~~~~~~~~~~\______
 ack _____________________________

(MOD_B is preparing to assert ack but before doing asserting operation, req is deasserted).

Ack operation can be written in verilog as follows:

assign ack = (latency==0) ? req :
              (latency==1) ? req && req_T1 :
              (latency==2) ? req && req_T1 && req_T2; 
               .... 
  always @(posedge CLK) begin
   if(! Z_RST) begin
     ack_T1 <= 1'b0;
     ack_T2 <= 1'b0;
     ..
   end
   else begin
     ack_T1 <= req;
     ack_T2 <= ack_T1; 
     ...
   end
  end

Incorrect assertion

property AssumeReqAck_AssertEdge;
@(posedge CLK)
  $rose(req) ##0 (req)[*0:12] |-> ack;
endproperty
property AssumeReqAck_CancelAssert;
  @(posedge CLK)
  $fell(req) |-> ack==0;
endproperty

Thank you, in advance, for your help.
Regards

2

Hi,

I’d write something like this:

  1. If req is asserted, MOD_B asserts ack in 0(immediately) to 12 clocks.
    $rose(req) |-> (req && !ack)[*0:11] ##1 (req && ack)
    This is if req is maintained during the first cycle when ack is active.
    If it’s not the case replace (req && ack) by (!req && ack). non overlapping until.

  2. If req is deasserted, MOD_B deasserts ack in 0(immediately) clock.
    $fell(req) |-> !ack

  3. ack is never asserted when no req is asserted.
    !req |-> !ack

Note that to addres the following point:
There exist a case where req is deasserted arbitrary even when ack has not been asserted.
You have to modify the first prop and replace (req && !ack)[*0:11] by (!ack)[*0:11]

But it looks like in this case the transfer is aborted, which doesn’t look like a normal transfer to me. So I would stick with the first prop which strengthen the verification…
By the way if this happens, will you receive an ack later anyway??? If it is the case you’ll see the third property failing.
Again it doesn’t look like a “proper handshake”.

3

In reply to Andreas38:

Andreas’s approach is very good - split your assertion/spec to several small ones. The 3rd one can also be written as:

  1. ack is never asserted when no req is asserted.
    ack |-> req;

Also if your tool supports, explore using LTL operators such as “until, until_with” etc. Many a times they capture the requirement in less text/code and are more intuitive.

Regards
Ajeetha, CVC

4

Thank you for the advice and correction.

I understand the way splitting the requirement into smaller parts of assertions to express a complete protocol is good approach.
I will check whether “until_with” statement is available with my tool tomorrow.

By the way if this happens, will you receive an ack later anyway??? If it is the case you’ll
see the third property failing.
No, once req is deasserted, no ack asserted for the req. In other words, ack is LEGALLY discarded by MOD_B.

Again it doesn’t look like a “proper handshake”.
The word “handshake” might not be good for me.
Although I agree with you this kind of loosely coupled interaction is rare, but it is actually used in my design. In my context, “req” is used to show MOD_B the timing of “you MAY work your operation”, rather than the conventional way of signal definition: “you MUST work your operation”. Basic concept of my design is best effort, so it is okey if req is not acknowledged.

In passing, how I can check my assertion is correct or not?
If there are good way, please let me know. As for me, when I do not have a confidence, I rely on simulation to generate incorrect cases …

Thank you very much for the advice.
Regards

5

In reply to tsb_matumoto:

Hi,

Ok I see your point regarding the req discarding.
But on a general level, any “MAY” that you have in the specification will dramatically fragilise the verification since you can’t verify these points with assertions…
And in general again, you can find some determinsitic conditions to turn the MAY into a SHALL.

I’m pretty sure that the discarding process is deterministic and depends on a set of register/inputs values. I’d try to identify the condition triggering a discard. Let’s call this condition cond1 (which is most likely a Boolean expr. but can also be a sequence).

And then you can write this:
$rose(req) |->
(
(!cond1 && req && !ack)[*0:11] ##1 (!cond1 && req && ack)
) or
(
(1’b1)[*0:11] ##1 cond1
)

This will bring closure in your protocol verification.

6

Dear Andreas38;

Thank you for the great idea. By taking internal deterministic conditions into account, I can write a property with more confidence. And I agree “SHALL” based protocol is better for verification and ,from a verification engineer’s standpoint, I will ask design engineer to use SHALL based definition in the next project.

Back to the first reply from you, you have coded as:

property AssumeReqAck_AssertEdge;
      @(posedge CLK)
	$rose(req) |-> (!ack)[*0:11] ##1 (req && ack)
   endproperty

But I think this is not correct because when $rose(req) happens, (req && ack) is not always true. Is my understanding correct?

Thank you for your cooperation.
Regards

7

In reply to tsb_matumoto:

Hello,

Hum I’m not sure I understand your question…
I’m pretty sure the proeprty is correct regarding your waveforms and descriptions.
What do you mean by “when $rose(req) happens, (req && ack) is not always true”?
If it’s again related to the possibility to abort transfers, my answer is in the previous message. Add the abort condition to the property.
But what I don’t quite get is that when $rose(req), you don’t know anything about the end of the property. You have to wait for 12 potential cycles.

8

In reply to Andreas38:

Hi,
I’d write something like this:

  1. If req is asserted, MOD_B asserts ack in 0(immediately) to 12 clocks.
    $rose(req) |-> (req && !ack)[*0:11] ##1 (req && ack)
    This is if req is maintained during the first cycle when ack is active.
    If it’s not the case replace (req && ack) by (!req && ack). non overlapping until.
  2. If req is deasserted, MOD_B deasserts ack in 0(immediately) clock.
    $fell(req) |-> !ack
  3. ack is never asserted when no req is asserted.
    !req |-> !ack
    Note that to addres the following point:
    There exist a case where req is deasserted arbitrary even when ack has not been asserted.
    You have to modify the first prop and replace (req && !ack)[*0:11] by (!ack)[*0:11]
    But it looks like in this case the transfer is aborted, which doesn’t look like a normal transfer to me. So I would stick with the first prop which strengthen the verification…
    By the way if this happens, will you receive an ack later anyway??? If it is the case you’ll see the third property failing.
    Again it doesn’t look like a “proper handshake”.

How would the same assertion look like if ack does not get asserted @posedge of clk, but goes high in the positive duty cycle?

Thanks