In reply to wiki458:
Hi Ben,
“Sampling in preponed region, execution in observed region, action block in reactive region”
Are these scheduling principles obeyed by assertion based formal verification tools as well, or do they have a different mechanism for sampling and evaluation?
Formal verification does not use simulation and works differently. From my SVA 3rd Edition:
7.1.4 More about model checking
In model checking, properties (written in a property language, like SVA) are used to capture the design intent. A formal verifier reads in an RTL design and builds a state transition graph for the system in a manner similar to an FSM. A first and foremost requirement for Model Checking is that designs need to be synthesizable and cycle-based. A natural limitation of such an approach would be that designs that contain
elements such as phase-locked loops (PLLs), behavioral memories, etc. cannot be converted into logic equations, thus they can’t be proven using the formal engines. Typically, a model checker treats non-synthesizable blocks as black-boxes, making the outputs of those blocks free ranging variables (meaning that they can have any random value), unless built-in models are available for those black boxes
The Verifier then reads in the properties and directives. Typically these properties represent the design specification as temporal sequences (such as request to grant protocols, illegal transitions), and they specify whether these properties hold forever or during a finite time. A Model Checker then checks whether the design implementation obeys these properties by searching the entire state space of the design, and produces counterexamples if the design fails to obey the properties.
By definition, FV is a complete proof, and hence is the ultimate verification methodology – if applicable. However, FV suffers heavily from the state space explosion problem for larger designs because it needs to search a very large number of states. An acceptable methodology is to limit the analysis to blocks of manageable size by partitions (i.e., smaller blocks) or by imposing constraints via the restrict operator to limit the scenarios for convergence on a proof (see 4.5.1.3). The assume construct should also be used to specify legal input states; this would avoid a failure due to some sequence of inputs that would not happen in the real world.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- 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