I’m struggling to figure out how to check a signal value doesn’t change mid-cycle via SVA.
Could I use $stable for this? - I thought $stable could only be used to check signal stability across multiple clock cycles, but not on the same clock cycle
To give a bit more perspective, let’s say I have a clock (clk), a signal (signal_a), which must not change across an entire clock cycle, and signal_a is driven on the neg-edge.
I tried using 2 properties, one with $rose, another one with $fell
The above is not working. Does this fall within the multi clock SVA category?
I have attached a screenshot which depicts a clock signal and a signal which doesn’t remain stable across the entire clock cycle, which is the situation I’m trying to have a check for.
I unstaood your question to mean that if (b_stable) then sig “a”
must not toggle in that cycle.
THIS SOLUTION IS INCORRECT
BECAUSE ANY FIRED TASK CAN SET THE
change TO 1
module top; // BAD SOLUTION
`include "uvm_macros.svh" import uvm_pkg::*;
bit clk, a, b_stable, changed;
int p1, f1;
initial forever #3 clk = !clk;
always @(posedge clk) begin
fork : FORK // DO NOT USE!!
int count;
begin changed=0; end
begin @(a) changed=1; end
join_none
end
ap_stable_a: assert property(
@(posedge clk ) // disable iff (disable_condition)
b_stable |-> ##1 changed==0) p1++; else f1++;
initial begin
bit v;
$dumpfile("dump.vcd"); $dumpvars;
repeat (20) begin
@(posedge clk);
if (!randomize(v, b_stable) with {
v dist {1'b1 := 2, 1'b0 := 1};
b_stable dist {1'b1 := 4, 1'b0 := 2};
}) `uvm_error("MYERR", "This is a randomize error");
if(v) #1 a=!a;
end
$finish;
end
endmodule
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
I just need to check that a signal driven on the negedge, does not change value during the entire clock cycle. The waveform screenshot I attached shows the data signal going low on the neg-edge of the clock, and coming back high on the pos-edge. I want the assertion to fire at that point.
I thought this was straightforward with direct assertion syntax, but so far I’ve not managed to write one successfully.
I’ve been able to successfully get the assertion to fire with glue logic.
// Data is driven on the neg-edge, and I want to check the data line
// does not change across a given clock cycle
logic neg_value, pos_value;
initial begin
forever begin
@ (negedge n_enable); //Active low enable
// The data are driven on the negedge, so the first value of the
// pos_value will need to be updated on the first negedge
@ (negedge clk);
pos_value <= data_line;
end
end
//Latching values on pos/neg edges to then compare the assertion
always @(negedge clk or negedge n_rst) begin: neg_update
if(!n_rst)
neg_value <= 0;
else if(!n_enable) begin
neg_value <= data_line;
end
end
always @(posedge clk or negedge n_rst) begin: pos_update
if(!n_rst)
pos_value <= 0;
else if(!n_enable) begin
pos_value <= data_line;
SAME_VALUE_CHECK_P: assert property (pos_value == neg_value);
end
end
The code above does what I want I think (I’ve seen the assertion fire when expected only). Can the above not be simplified into a multi-clock assertion such us:
I don’t understand why the assertion above doesn’t work. Is it required for multi-clock SVA checks for the clocks to have different frequency?
I’ve also tried swapping
module top;
//`include "uvm_macros.svh"
// import uvm_pkg::*;
bit clk;
bit[2:0] data, p1, f1, p2, f2;
initial forever #3 clk = !clk;
// Am assuming that the data has a setup time,
// meaning that data cannot change in the exact time as negedge clk.
// I am also assuming that data is drivien in a nonblocking assignment
// i.e., @(negedge clk) data<= an_int_value;
task automatic t();
int v; bit fail, pass;
fork
begin
@(posedge clk) v=data;
wait(data != v); fail=1;
end
begin @(negedge clk) pass=1; end
join_any
am_data: assert(fail==0) p1++; else f1++;
endtask //automatic
always @(negedge clk) fork t(); join_none
property signal_change_check;
bit[2:0] v;
@(posedge clk )
(1, v= data) |=> @(negedge clk) v == data;
endproperty
ap_signal_change_check: assert property(signal_change_check) p2++; else f2++;
initial begin
bit[2:0] v; bit err;
$dumpfile("dump.vcd"); $dumpvars;
repeat (20) begin
@(negedge clk);
if (!randomize(v, err));// `uvm_error("MYERR", "This is a randomize error");
if(err) begin
#1 data<=v;
@(posedge clk) #1 data<= v+1'b1;
end
else #1 data<=v;
end
$finish;
end
endmodule
However, the property was not working as expected as it was failing even when the signal on the negedge was the same as in the posedge.
I want to check the signal doesn’t change value mid-cycle, because the signal can be driven on the neg or pos-edge depending on configuration, and had a case in which the signal was wrongly toggling mid-cycle.
(1, neg_edge_value = data_line) |-> @(posedge clk) neg_edge_value == data_line;
I am not clear as to when the signal changes.
How is the fork-solution working for you?
Can you expand on that solution? That will suggest an SVA approach.
Can you explain what you’re trying to achieve by switching |=> to |->?
I tried it anyways, but the assertion fails identically as when I use |=>.
The LRM says in section 16.13.2 (Multiclocked properties):
The meaning of multiclocked nonoverlapping implication is similar to that of singly clocked nonoverlapping
implication. For example, if s0 and s1 are sequences with no clocking event, then in @(posedge clk0) s0 |=> @(posedge clk1) s1
|=> synchronizes between posedge clk0 and posedge clk1. Starting at the point at which the implication
is being evaluated, for each match of s0 clocked by clk0, time is advanced from the end point of the match
to the nearest strictly future occurrence of posedge clk1, and from that point there must exist a match of
s1 clocked by clk1.
The following example shows a combination of differently clocked properties using both implication and
Boolean property operators: @(posedge clk0) s0 |=> (@(posedge clk1) s1) and (@(posedge clk2) s2)
The multiclocked overlapping implication |-> has the following meaning: at the end of the antecedent the
nearest tick of the consequent clock is awaited. If the consequent clock happens at the end of the antecedent,
the consequent is started checking immediately. Otherwise, the meaning of the multiclocked overlapping implication is the same as the meaning of the multiclock nonoverlapping implication.
For this case, where the first event is on the neg-edge and the second on the pos-edge both overlapping and non-overlapping implication operators are correctly behaving in the same way.
So far I’ve only been successful at getting the check to work using concurrent assertions and some glue logic around sampling the values at the neg and pos edges.
This still feels like it can be check via SVA in a more simple manner though.
You’re correct on |-> and |=>
I use |-> because I know that posedge and negedge of the same clock do not occur in the same time slot.
the following solution assumes the following:
(negedge clk ) (1, neg_edge_value = data_line) |->
@(posedge clk) neg_edge_value == data_line;
a) data may change between posedge and negedge
b) data sampled at the next posedge is same as data sampled at negedge.
c) any data glitch between negedge and posedge is NOT detected if data is unchanged after the glitch.
If uou want to detect a glitch, see my fork-join solution above.
