Hi All,
There is a BlackBox with one input bus and one output bus. There are VALID signals for each of the buses. The block is clocked by CLK.
How can I check / assert that the sequence of data in the output bus is the same as in the input bus? Latency between input and output data may vary (actually latency between VALID signals may vary).
I know how to write this check in Verilog, but I wonder how to write it using SVA.
Thank you!
your requirements are ambiguous. Are you talking about a fifo?
If I assume that the data from left gets in at valid_left, and data from out with a valid, then I came up with the following:
// There is a BlackBox with one input bus and one output bus.
// There are VALID signals for each of the buses. The block is clocked by CLK.
// How can I check / assert that the sequence of data in the output bus is the
// same as in the input bus? Latency between input and output data may vary
// (actually latency between VALID signals may vary).
module test2;
parameter UPPER = 9;
bit clk, valid_l, valid_r; // valid left, valid right
bit[15:0] data_l, data_r; // data left, data right
// How long is the sequence?
// What is the start of the sequence
property p_dldr;
bit[15:0] v_d;
@(posedge clk) (valid_l, v_d=data_l) |-> ##[1:UPPER] data_r==v_d;
endproperty
a_: assert property ( p_dldr );
initial forever #5 clk=!clk;
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Yes, behavior of this block is similar to FIFO.
(valid_l, v_d=data_l)
May this command be presented as ([condition],[expression])? Where can I read a full description of the command?
I don’t see how ‘valid_r’ is participated in the checks… Can the above be re-written in the following way:
@(posedge clk) (valid_l, v_d=data_l) |-> ##[1:UPPER] valid_r ##0 data_r==v_d;
Thank you!
P.S. what’s the name of the ([condition],[expression]) function? If I want to read its full description, what’s function name should I search for in the books?
In reply to dmitryl:
You’re correct, I missed the valid_r.
@(posedge clk) (valid_l, v_d=data_l) |->
##[1:UPPER] valid_r ##0 data_r==v_d; // Corrected
A sequence can be one of the following:
sequence_expr ::= // See 1800::16.7
…
( sequence_expr {, sequence_match_item } ) [ sequence_abbrev ]
sequence_match_item ::=
operator_assignment
| inc_or_dec_expression
| subroutine_call
sequence_abbrev ::= consecutive_repetition
consecutive_repetition ::=
[* const_or_range_expression ]
| [*]
| [+]
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
Could the following
property p_dldr;
bit[15:0] v_d;
@(posedge clk) (valid_l, v_d=data_l) |-> ##[1:UPPER] valid_r ##0 data_r==v_d;
endproperty
be re-written as:
sequence vld_seq;
@(posedge clk)
valid_l ##0 v_d=data_l;
endsequence
property p_dldr;
bit[15:0] v_d;
@(posedge clk) vld_seq |-> ##[1:UPPER] valid_r ##0 data_r==v_d;
endproperty
?
In reply to dmitryl:
It is illegal. Note:
valid_l ##0 v_d=data_l;
is illegal because property local variable must be written in sequence_match_item
The following is your only choice.
property p_dldr;
bit[15:0] v_d;
@(posedge clk) (valid_l, v_d=data_l) |-> ##[1:UPPER] valid_r ##0 data_r==v_d;
endproperty
Putting the local variable in the sequence does not make that variable visible to the property.
The local variable can be declared in the property and passed as an argument to the sequence.
But, it really is too much bother, and makes the code less readable.
Ben SystemVerilog.sv
In reply to ben@SystemVerilog.us:
Is there a way to re-write the
(valid_l, v_d=data_l)
sequence in another way (other than (… , …))?
In reply to dmitryl:
Two concepts, local variable in property and local variable in sequence:
local variable in a property
Within a property, if you want to modify a property local variable or a module variable then you HAVE TO use a sequence_match_item, as explained in my previous answer. You cannot, otherwise, modify any variable otherwise. To modify a module variable, then you would have to use a function call.
module m;
bit clk, a, b, c;
int data;
function void set_data(int x);
data=x;
endfunction
ap_module: assert property(@(posedge clk)
(a, set_data(1234) |-> b ##[1:$] c ##0 data==1234);
// Note: data is not local to the property
property p_d;
int v_d;
(a, v_d=data) |-> b ##[1:$] c ##0 data==v_d);
endproperty
ap_d: assert property(@(posedge clk) p_d );
// Note: v_d is local to the assertion and every successful attempt and thread carries its own copy of it.
What exactly are your issues in using a sequence_match_item? the ()?
I don’t get it.
local variable in a sequence
Rule: A local variable formal argument acts as a local variable of the sequence or property. It can be exported out only if direction inout or output (in sequence declarations only, and not in property declaration). An untyped formal argument cannot have a direction or a type; it can be treated as a local formal argument of direction input or output depending on how it is used within the sequence or property. An untyped formal argument can also be treated as a non-local formal argument if it is not assigned a value in the body of the sequence or property in which it is used. For example (Ch/2type_m.sv)
bit clk, a, b, c;
default clocking cb_clk @ (posedge clk); endclocking
sequence q_local_formal_arguments2( local input int i=0,
untyped j, k,
local output bit t);
(i>10, j=i) ##1 (1, j=data, t=1'b1) ##1 k;
endsequence
property p_test_untype;
int x, z; // local variable
bit r; // local variable
(a, x=10) ##1 q_local_formal_arguments2( .i(x), .j(z), .k(a), .t(r)) ##1 x==z ##0 r;
endproperty : p_test_untype
ap_test_untype: assert property(p_test_untype);
Ben SystemVerilog.us