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);
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);
In reply to suresh M:
Depends on your specification - such as:
Srini
www.verifworks.com
In reply to Srini @ CVCblr.com:
For a one bit counter the following assert property code is correct one r not?
spec:
property counter_1bit;
@(posedge clk)
$fell(reset)|-> $fell(count);
endproperty: counter_1bit
onebit_counter: assert property(counter_1bit);
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?
In reply to Anudeep J:
I’m looking for one bit counter functionality.
checking for reset condition , will the above code works or not?
In reply to suresh M:
It will work for reset condition. BUt it will not work for counter functionality
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);
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);
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.
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);
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
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 ?
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.
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);