If property is asserted in the always block, then, in which region read and write signals be sampled?? Kindly help!!
module myModule(input bit clk,read,write,reset);
//assert property(p);
//asserting here samples the signals read and write in the preponed region
always@(posedge clk)
assert property(p);
//If property is asserted in the always block, then, in which region read and write signals be sampled??
//Kindly help
endmodule
ap_ab1: assert property(@ (posedge clk) a |=> b );
ap_ab2: assert property(@ (posedge clk2) a |=> b );
always_ff @(posedge clk) begin
ap_ab1a: assert property(@ (posedge clk) a |=> b );
ap_ab2a: assert property(@ (posedge clk2) a |=> b );
end
// These two are identical, with variables sampled in the Preponed region.
// It's the same clocking event
ap_ab1: assert property(@ (posedge clk) a |=> b );
always_ff @(posedge clk) begin
// ap_ab1a: assert property(@ (posedge clk) a |=> b );
// FIrst the posedge clk occurs, then
// At the next posedge clk2, variables a, b sampled in the Propned region of posedge clk2
always_ff @(posedge clk) begin
ap_ab2a: assert property(@ (posedge clk2) a |=> b );