Hi,
Can some help me write an assertion to check waking 1s pattern for a signal? Ex: for a 4-bit signal, the behavior is as follows: 1000, 0100, 0010, 0001.
I tried in this manner. Please let me know if it is correct:
property p1 @(posedge clk);
$countones(a ^ $past(a,1)) == 2;
$onehot(a) == 1;
Let me know if it correct or there is a better way to do this.
Thanks!
In reply to curious_verifier:
What is my design is in error I I get the sequence for that walking ONE to be
0100 0001 0010 … ?
Have you tried it?
$countones(a ^ $past(a,1)) == 2;
current a== 0100
past(a)(in err) 0001
past_a ^ a 0101 $countones(of this) == 2, An ERROR
since this is not a walking one.
You can use support logic or a function call
BEn
Thanks Ben. I used function and tried it out.
Here is the revised logic:
module test;
logic [3:0] data;
bit clk;
static logic[3:0] temp = 4'b1000;
function bit check1(logic [3:0] x);
$display("the temp is: %b and x is: %b",temp,x);
if (temp == x) begin
temp = {temp[0], temp[3:1]};
return 1;
end
return 0;
endfunction
property check1_data;
@(posedge clk) '1 |-> check1(data);
endproperty
assert property(check1_data) begin
$display("%b passed", data);
end
else begin
$display("%b failed", data);
end
initial begin
clk = 1'b0;
forever #5 clk = ~clk;
end
initial begin;
#4;
data = 4'b1000;
#10;
data = 4'b0100;
#10;
data = 4'b0010;
#10;
data = 4'b0001;
#4;
$finish;
end
endmodule
Assertion is passing with this. But wanted to check with you if this is good approach.
Thanks!
In reply to curious_verifier:
Your assertion does not check for the walking requirement. You also need to clarify your requirements. Is the a continuous walking one with a wrap-around? Is there a starting or enable signal. What happens after the 1 reaches the LDB (bit 0)
Hi Dave,
Yes it is wrapping requirement, Also, the enable condition or the starting point is: 1000. Assertion should check with respect to previous clock.
In reply to curious_verifier:
Bottom line, the right concept, but I prefer a more traditional style.
You use a static function as an expression that saves the old value.
I would not do this. Usually, functions are called in a
sequence_match_item to update a local variable. They can also be used to compute the new expected value
// Essence of your code:
function bit check1(logic [3:0] x);
$display("the temp is: %b and x is: %b",temp,x);
if (temp == x)
begin
temp = {temp[0], temp[3:1]};
return 1;
end
return 0;
endfunction
assert property(@(posedge clk) '1 |-> check1(data)); //
My modifications:
module test;
logic [3:0] data;
bit clk;
static logic[3:0] temp = 4'b1000;
function automatic bit[3:0] expected_data(logic [3:0] past_d);
bit[3:0] v;
// compute the current d based on the past_d
v = {past_d[0], past_d[3:1]};
return v;
endfunction
property expected_data_data;
@(posedge clk) $countones(data)==1 ##0 data==expected_data($past(data));
endproperty
assert property(expected_data_data) $display("%b passed", data);
else $display("%b failed", data);
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to curious_verifier:
module test;
logic [3:0] data;
bit clk;
logic[3:0] temp = 4'b100;
let ROTR(in) = in >> 1 | in << $bits(in) - 1;
always #5 clk = ! clk;
initial begin;
data = temp;
repeat (10) @(posedge clk) begin
data <= ROTR(data);
$displayb(data);
end
// #100 // for failures
$finish;
end
property walking1(in);
@(posedge clk) $onehot(in) && in[$left(in)][->1] // starting point begins
|=> always $onehot(in) && in == ROTR($past(in));
endproperty
initial assert property (walking1(data)) $info("pass");
endmodule
In reply to dave_59:
Interesting approach. You’re good at manipulating data bits of a register.
I tend to take a programming (code) approach.
Either way, thanks for bringing a different point of view.
Ben
An alternative solution :
always #5 clk = !clk ;
bit [3:0] state ; // Assuming DUT updates state on each clock in NBA region
bit [3:0] q_state[$] = { 4'b1000 , 4'b0100 , 4'b0010 , 4'b0001 }; // Possible Valid states
function bit[3:0] return_state() ;
return state ; // returns DUT's updated NBA value of the same time step
endfunction
bit [1:0] st = 2'b11; // On first Increment we want 0
function bit[1:0] return_bit();
st++;
return st;
endfunction
property prop;
bit [3:0] current_st ;
bit [1:0] index ;
@(posedge clk) (1, current_st = return_state(), index = return_bit() ) ##0 current_st inside { q_state } ##0 ( current_st == q_state[ index ] ) ;
endproperty
assert property( prop ) $display("T:%2t PASS" , $time);
else $display("T:%2t FAILS" , $time);
initial #100 $finish();
In reply to MICRO_91:
Ben
In reply to ben@SystemVerilog.us:
Ben ,
I appreciate the honest feedback however, the student in me would like to know your views on the following :
1.BAD STYLE because it relies on SV regions
The design would update the register in either NBA or in Active ( via loopback from NBA to Active ).
Knowing section 16.11 of the LRM , how is it that it’s considered a bad style ?
It’s not as if I am using a tool’s restriction/implementation to achieve the solution.
2.Not applicable to formal
Could you elaborate on this ?
3.Difficult to follow and to apply to requirements
Since I could use the same basic logic to enhance the code to a different pattern detection , I am not sure on how the requirements are not being met .
Thank you Ben and Dave!
In reply to MICRO_91:
In reply to ben@SystemVerilog.us:
I appreciate the honest feedback however, the student in me would like to know your views on the following :
The design would update the register in either NBA or in Active ( via loopback from NBA to Active ).
Knowing section 16.11 of the LRM , how is it that it’s considered a bad style ?
It’s not as if I am using a tool’s restriction/implementation to achieve the solution.
You are writing assertions that compare updated values of variables (updated in the NBA) to sampled values of variables. To do that, you depend on how simulation uses regions to simulate concurrency. So now, you are getting into the heart of the tool.
SVA specifically uses the sampling of signals before any update to keep things CLEAN.
Instead of comparing updated values of variables to sampled values of variables,the better approach is to compare sampled values to past values.
Could you elaborate on this ?
In SystemVerilog formal verification, there are no time regions or concepts like “Prepone” and “Active”, “NBA” as you might find in simulation. These concepts are specific to simulation and are used to control the timing and scheduling of events within the simulation environment. Time regions, such as “Prepone” and “Active”, NBA" are used to model the timing behavior of a hardware design.
In formal verification, the focus is on proving the correctness of the design without relying on simulation time. Formal tools use mathematical algorithms and symbolic reasoning to exhaustively analyze the design’s behavior and properties, without considering the concept of simulation time or event scheduling. Formal verification tools explore all possible input combinations and paths within the design to ensure that it adheres to specified properties or assertions.
Therefore, while simulation heavily relies on the concept of time and event scheduling, formal verification operates independently of simulation time and does not use time regions or similar concepts. Instead, it works with logical and mathematical models to prove or disprove the correctness of a hardware design based on formal specifications and assertions.
**Example:**
bit[3:0] state, nxt_st;
always @(posedge clk) nxt_st <= state;
function bit[3:0] updated_nxt_st();
return nxt_st ; // returns DUT's updated NBA value of the same time step
endfunction
ap_not4formal: assert property(@(posedge clk)
updated_nxt_st() == state) |-> b; // registered state==sampled state |-> b
// works in simulation because of SV processing of regions
// In FV, since it knows nothing about Regions, the above assertion is interpreted as
ap_not4formal_interpretation: assert property(@(posedge clk)
nxt_st == state |-> b); // which is incorrect; this models a wire and not a register
Since I could use the same basic logic to enhance the code to a different pattern detection , I am not sure on how the requirements are not being met .
Your approach is NOT how SVA is intended to be used. SVA is based on sampled values and does not depend on how the tool processes SV. Now, by putting into your assertions the updated values of values along with the sampled values of variables, you are adding another layer of complexity in understanding the properties.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
how about this one:
module tb;
bit [3:0] va = 4‘b0010;
property walk;
@(posedge clk);
bit[3:0] temp;
$countones(va) ##1 (1, temp = {va[0], va[3:1]}) ##0 (temp == va);
endproperty
In reply to qkuang:
This is what you need
$onehot(va) ##0 // one hot
(1, temp = {va[0], va[3:1]}) // compute the next value
##1 (temp == va); // compare the expected new value to the current value
Ben