Assert property

Coverage
,
1

For a one bit counter the following assert property code is correct one r not?

property counter_1bit;
@(posedge clk)
$fell(reset)|-> $fell(count);
endproperty: counter_1bit

onebit_counter: assert property(counter_1bit);

2

In reply to suresh M:

Depends on your specification - such as:

  1. Is reset active Low or High
  2. Counter is synchronously reset or async?

Srini
www.verifworks.com

3

In reply to Srini @ CVCblr.com:
For a one bit counter the following assert property code is correct one r not?
spec:

  1. reset is active low
  2. synchronous counter.

property counter_1bit;
@(posedge clk)
$fell(reset)|-> $fell(count);
endproperty: counter_1bit

onebit_counter: assert property(counter_1bit);

4

In reply to suresh M:

Hi,

Are you checking only for reset condition? Or else are you looking for counter functionality also? Could you please specify for which scenario you are looking?

5

In reply to Anudeep J:

I’m looking for one bit counter functionality.
checking for reset condition , will the above code works or not?

6

In reply to suresh M:

It will work for reset condition. BUt it will not work for counter functionality

7

In reply to Anudeep J:

You can go with below code for checking counter functionality

property counter_1bit;
bit cnt;
disable iff(!reset)
@(posedge clk)
(1, cnt = out)|=> (out == cnt + 1'b1);
endproperty: counter_1bit

onebit_counter: assert property(counter_1bit);
8

In reply to Anudeep J:
what is the need of 1 in the below code, I don’t understand that the sequence (1,cnt=out)
(1, cnt = out)|=> (out == cnt + 1’b1);

9

In reply to suresh M:

1 is to make that sequence intentionally true but our ultimate goal is to assign present out value to cnt.

10

In reply to Anudeep J:
Shall we write code like this ?if not this, please guide me

property counter_1bit;
@(posedge clk)
($fell(reset)&&$fell(count))|=> (count=count+1’b1);
endproperty: counter_1bit

onebit_counter: assert property(counter_1bit);

11

In reply to suresh M:

Hi,

You are saying that its an active low reset, then why are you checking counter functionality when it is fell(my query). PLease clarify me

12

In reply to Anudeep J:

I’m saying that reset action also includes in counter functionality, can’t we write like this

($fell(reset)&&$fell(count))|=> (count=count+1’b1);

that is $fell(reset)-----> which is checking active low reset?
should we write only like this

disable iff(reset)
is this statement can use only for asynchronous ?

13

In reply to suresh M:

No we cannot write because, if you check for ($fell(reset)&&$fell(count)) condition, you are checking reset and then you are checking counter value in the next cycle immediately. It implies, you are checking counter functionality when it is in reset mode. Counter gives 0 as output when it is reset and counter works after reset got rose. For synchronous, you should check for reset and counter functionality seperately(as per my knowledge). I hope you got what I was trying to explain.

14

In reply to Anudeep J:

then shall we write like this

property check_reset;
@(posedge clk)
$fell(reset)|->$fell(count);
endproperty: check_reset

property check_counter_fn;
@(posedge clk)
$rose(reset)|-> count=count+1’b1;
endproperty: check_reset

onebit_counter_reset: assert property(check_reset);
onebit_counter_fn: assert property(check_counter_fn);