In reply to moogyd:
Looks like a good solution. The always_comb if (clk_div4) triggers on a change in clk_div4 going to a 1'b1, and the deferred assertion reporting is done in the Reactive Region with the #0, or in the Postponed Region with the final. In your case, either version of the deferred assertion looks OK, unless you have tricky combinational logic for the generation of clk_div2, which I doubt.
Quote:
1800'2012: The processing of the action block differs between
observed and final deferred assertions as follows:
— For an observed deferred assertion, the subroutine shall be scheduled in the Reactive region. Actual argument expressions that are passed by reference use or assign the current values of the underlying variables in the Reactive region.
— For a final deferred assertion, the subroutine shall be scheduled in the Postponed region. Actual argument expressions that are passed by reference use the current values of the underlying variables in the Postponed region.
Ben Cohen
http://www.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 978-1539769712
* 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
--------------------------------------------------------------------------