I coded assertion like this but the simulator is showing this error
** Error: …/ref/i2c_assertions.sv(82): Illegal SVA expression in Verilog expression.
Can anyone point out what’s the mistake?
//START condition
//Detects the time where SCL went LOW
sequence scl_fall(Tscl_fall);
($fell(I2C_INTERFACE.scl),Tscl_fall=$time);
endsequence
//Detects where the time where SDA went LOW
sequence sda_fall(Tsda_fall);
($fell(I2C_INTERFACE.sda),Tsda_fall=$time);
endsequence
//Checking for START condition
sequence s1;
time t1,t2;
(((scl_fall(t1))>(sda_fall(t2))),$display("START condition dtected at %0t",sda_fall(t2)));
endsequence
property p1;
@(negedge I2C_INTERFACE.scl) s1 ;
endproperty
I explain the issue you have in my SVA Handbook; basically, typed formal arguments declared as local variables can be exported to the calling unit, such as the property or sequence, if they are prefixed with the reserved word local and are declared of direction inout or output. Variables declared in the assertion variable declaration region (i.e., those not in the port list) cannot be exported. Here is a link to my book that explains the rules in handling the exportation of local variable
Below is the sample code and simple testbench for it.
//1. Data transfer from the external interface into the driver.
//2. Data transfer from the driver to the memory through another interface.
//3. Verification that data stored into the memory at that address location is identical to what was originally transferred from the originator of the data
module var_example;
bit clk, ext1_req, ext1_ack, ext1_rd_wrf;
bit ext2_req, ext2_ack, ext2_rd_wrf;
byte ext1_data, ext2_data, drv_data;
byte mem[0:1024];
bit[0:9] ext1_addr, ext2_addr;
initial forever #10 clk=!clk;
default clocking cb_clk @ (posedge clk);
endclocking
sequence q_ext1_to_driver(local output byte v_data,
local output bit[0:9] v_addr);
first_match (($rose(ext1_req) && !ext1_rd_wrf, v_data=ext1_data,
v_addr=ext1_addr) ##[1:3] ext1_ack);
endsequence : q_ext1_to_driver
sequence q_ext2_to_mem(local input byte v_data, local input bit[0:9] v_addr);
ext2_req ##0 !ext2_rd_wrf ##0 ext2_data==v_data ##0 ext2_addr==v_addr ##
1 ext2_ack ##[1:3] mem[v_addr]==v_data;
endsequence
property p_ext1_to_mem;
byte v_data;
bit[0:9] v_addr;
q_ext1_to_driver(v_data, v_addr) |->
##[1:3] q_ext2_to_mem(v_data, v_addr);
endproperty : p_ext1_to_mem
ap_ext1_to_mem: assert property(p_ext1_to_mem);
always begin
if(!randomize(ext1_data, ext1_addr)) $display("randomization failure");
@ (posedge clk);
ext1_req <= 1'b1;
ext1_rd_wrf <= 1'b0;
mem[ext1_addr] <= ext1_data; // preload of data for test only
@ (posedge clk);
ext1_req <= 1'b0;
ext1_rd_wrf <= 1'b1;
ext1_ack <= 1'b1;
@ (posedge clk);
ext2_req <= 1'b1;
ext2_rd_wrf <= 1'b0;
ext2_data <= ext1_data;
ext2_addr <= ext1_addr;
ext1_ack <= 1'b0;
@ (posedge clk);
ext2_req <= 1'b0;
ext2_rd_wrf <= 1'b1;
ext2_ack <= 1'b1;
@ (posedge clk);
ext2_ack <= 1'b0;
repeat (5) @ (posedge clk);
end
endmodule : var_example
Consider using the within sequence operator. The sequence containment within specifies a sequence occurring within another sequence.
Note: (seq1 within seq2) is equivalent to:
((1[*0:] ##1 seq1 ##1 1[*0:]) intersect seq2 )
You also seem to overuse the sequence declaration, and I see no use for your task.
I don’t know if this assertion will work for you, but I suggest something like.
// When SCL is HIGH and before it goes LOW,
// SDA should go LOW.(Here SDA and SCL start from being HIGH initially)
ap_scl: assert property(
@ (posedge some_clock) $rose(scl)|-> !sda[->1] within $fell(scl)[->1]);
// @ (posedge some_clock) $rose(scl)|-> !sda[->1] within ($fell(scl) && sda)[->1]);
// A pootential other option.
// As far as "(1'b1,posedge_delay)|->(slave_addr_tran==1'b1)"
// I have no idea as to what you are talking about.
// If there is a relationship between $fell(sda) and slave_addr_tran,
// write another assertion
1.Here my clock itself is scl.So,I cant check the START condition if I use @(posedge scl) as my clocking event.So, I used @(negedge sda).
2.After START was detected,at the next immediate posedge of SCL,checking of cfg.slave_addr_tran ==1’b1 should be done.So, I thought of using a task which will produce delay of one posedge of scl.
I thought of using a task which will produce delay of one posedge of scl.
BTW, firing a task from a sequence_match_item just fires it, like a function call. There is no time consumption in the assertion.
It is discouraged to use tasks; I haven’t chhecked, but I believe it might be illegal. If legal, it does nothing for the assertion (no time consumption processed by the assertion as a result of the task call). You can use functions that consume no time.
Ben SystemVerilog.us
But ben, how to use non-clocked delays for checking the sequences? (Delays less than one clock cycle).
SVA is event-based with variables samples in the Preponed region of the event.
Events are usually clocking event, but could be user-defined events (declared with the event type).
Assertions are really intended to verify and cover properties based on the relationships of variables (e.g, req |=> ack)
For delays, you could use supporting logic yo create events.
Write multiple small assertions instead of 1 compex one.
Ben
It is quite complicated here.Because,
START condition has to be checked first when scl is HIGH.Then scl should go LOW and after some time it should go HIGH and at this posedge of SCL I need to sample a variable.
The problem occurs due clocking event.Because for START condition ,the clocking event is negedge of sda and for sampling the variable(cfg.slave_addr_tran) the clocking event is posedge scl.
SVA can use multiclocks,
@(posedge clk1) a |-> @(posedge clk2) b
Solve your particular verification with plain SystemVerilog code
e.g.,
always @(posedge clk) begin
...
end
On this forum, I generally provide guidance and quick help. However, for detailed complex problems, I really do not have the time, and besides, it is not my responsibility anyway.
Best wishes.
Ben