This assertion is based on clock semantic and use sampled value of their expression. These assertions can expand over multiple cycle.
always@ (posedge clk)
a1: assert property (a ##2 b);
a2: assert property (@(posedge clk) a ##2b);
In Vivado® simulator, the concurrent assertion of 2nd form that is used outside the procedural block is supported.
- In Tcl console, invoke
close_sim
command to close the simulation running previously. - In Tcl console, invoke
reset_simulation
command to clean the simulation directory. - In Tcl console, invoke
launch_simulation
command to run the simulation. - In Tcl console, invoke the following
command:
current_scope /axi_vip_0__exdes_adv_mst_active_pt_mem__slv_passive/DUT/ex_design/axi_vip_passthrough/inst/IF/PC
- Double-click the scope PC to open the source code.
- Observe that line number 1144 onwards all the property declarations and assertions have been used.