Formal Verification SVA assume signal to NOT toggle at negedge

In reply to erictaur:
If FV can handle multi locking, you can write something like:


property p; 
 bit v; 
  @(posedge clk) (1, v=sig) ##0 @(negedge clk) sig==v; 
endproperty 
ap_p: assert property(p);
 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books:
  3. Papers:
    Understanding the SVA Engine,
    Verification Horizons
    Reflections on Users’ Experiences with SVA, part 1 and part 2
    Reflections on Users’ Experiences with SVA

SUPPORT LOGIC AND THE ALWAYS PROPERTY
http://systemverilog.us/vf/support_logic_always.pdf
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/