Assertion for command transfer


module assert;
 bit clk, reset;
 bit out_vld, out_rdy;
 bit in_vld, out_rdy;
 bit [31:0]out_cmd;
 bit [31:0]in_cmd;

always @(posedge of clk iff reset)begin // or task to do the same
if( out_vld && out_rdy) begin
// out_cmd to transfer
end
end

always @(posedge of clk iff reset)begin
if( in_vld && in_rdy) begin
// in_cmd to be received
end
end
// assertion:
//the out_cmd should get successfully transferred within 16 clk
// there is 3 interface which are sending command
// say core, sw, ip

endmodule

In reply to m_r_m:

 
module assert;
 bit clk, reset;
 bit out_vld, out_rdy;
 bit in_vld, out_rdy;
 bit [31:0]out_cmd;
 bit [31:0]in_cmd;
 
always @(posedge of clk iff reset)begin // or task to do the same
if( out_vld && out_rdy) begin
// out_cmd to transfer
end
end
 
always @(posedge of clk iff reset)begin
if( in_vld && in_rdy) begin
// in_cmd to be received
end
end
// assertion:
//the out_cmd should get successfully transferred within 16 clk
// there is 3 interface which are sending command
// say core, sw, ip
// [Ben] is this what you need? Repeat for the other out_cmd values 
let core_cmd=8'H0001;
ap_out_core: assert property(@(posedge clk) 
 out_vld && out_rdy |-> ##[1:16]out_cmd==core_cmd); 
endmodule


In reply to ben@SystemVerilog.us:
thanks for your reply.


// assertion:
//the out_cmd should get successfully transferred within 16 clk
// there is 3 interface which are sending command
// say core, sw, ip
// [Ben] is this what you need? Repeat for the other out_cmd values 
// core will send commands "out_cmd" and same will be rcvd as "in_cmd" (if in_vld && in_rdy)at end point.
// (checker to check the xfer should be w/i 16 clk)
// there will be multiple commands 
// if 1st cmd is at t1 (should be xfered w/i t1+16;)
// similar for all intf