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
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115