In reply to rkg_:
I would write two assertions
- An assertion based on the inc, dec, that impacts the lock.
- An assertion on how inc, dec are generated based on fll_unlock_check_timer.
In other words, you need to check the creation of the outputs, making sure that they are according to spec. That spec may be other factors besides the timer. The timer is an implementation. In general, for black-box the implementation is irrelevant.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
… - SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
- Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com - Papers:
- Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy - SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy