Formal Verification of Hardware Designs Unit-II
Lecture –I: - Introduction to System Verilog Assertions
1. Define the following terms connected with formal verification:
Assertion, Assumption, Constraint, Coverage, Fairness property, Formal specification
2. Briefly describe the factors which amplify the power of formal verification.
3. List out the difficult situations where we will look for help from Formal Verification.
4. List out the different formal verification usage models.
5. List out the advantages of Formal Verification.
6. With neat diagram, explain the layers of System Verilog Assertions.
7. What are the features of System Verilog as hardware verification language (HVL) useful in
creating better testbench?
Answer:
• Lexical elements of System Verilog can be broadly classified as: -
• Object oriented programming and randomization (OOPS)
• Assertions
• Layered System Verilog Testbench structure need both OOPS and Assertions
• System Verilog assertions are used to construct the properties which represent design intent in
formal verification.
Lecture –II: - Immediate Assertions
8. Explain the features of immediate assertions.
9. Why concurrent assertions are recommended normally unless usage of immediate
assertions is required for un-clocked sections of design.
10. Why deferred immediate assertions are recommended?
11. List out the features of concurrent assertions.
Lecture –III: - Concurrent Assertions
12. List out the sampled value functions supported in System Verilog Assertions.
13. What are the precautions taken with respect to reset in designing concurrent assertions.
• Assertion reset is asynchronous, with an assertion being shut off immediately any time its
disable condition is met.
14. How to set default clock and reset in system Verilog assertion.
Lecture –IV: - Sequences and Properties in Assertions
15. List out the operators used to combine the sequences.
16. Why it is recommended to use sequences instead of $rose/$fell .
17. Explain implication operator in sequences
Lecture –V: - Building Properties
18. Explain implicit multi-threading in assertions.
19. How to plan a assertions at specification phase
20. How to plan for embedding properties during RTL development.
21. How to plan for a Validation related Properties
22. Explain how to connect properties to design
23. Explain named sequences with an example.
24. Difference between Simulation & FPV
25. Explain FPV.
