Questa OneSpin StaticFormal Questa Verify Property: Leading the Way in Digital Design Verification

 
Thank you for all the questions during the webinar! You can find the answers to the live questions below. If more support is needed for any of the issues you are facing, please open a support case at https://support.sw.siemens.com/

Q&A

Q: How to prevent inconclusive results through the tool?
A: There are several methods to prevent inconclusive results such as:

1. Increase the run time using the -timeout option.
2. Black-boxing parts of your design hierarchy that are not of interest using the netlist blackbox directive.
3. Cut-point any logic that may not be formal-friendly such as large counters or memories using the netlist cutpoint directive.
4. Set constant pins on test logic, don't care configurations, modes, and clock enables to reduce design size and help compile and run time using the netlist constant directive.

For more information about all directives and commands, please refer to the command reference manual. 

Q: Is there a way to generate a testbench from Questa Verify Property?
A: Yes, you can create a set of testbenches that reproduce the firing in the active formal verify database using the formal generate testbenches TCL command. 

Q: What is the difference between Assert and Assume constructs?
A: An assert construct is a property that is expected to always be true throughout the formal analysis. However, an assume construct describes a legal input to the design to make it easier for the analysis. 

Q: How to enable the contributors group in the waveform window?
A: You can go to the Properties pull-down menu after highlighting the Properties tab and choose Preferences. You will find a drop-down menu beside Contributors, hit it and choose Show Opened to always be opened by default when opening the waveform window. 

Q: What does a sanity waveform mean?
A: A sanity check is a check that a stimulus sequence exists that activates the checking logic for the property and results in events that show the application of the property. Whereas the waveform for the stimulus sequence is called a sanity waveform. 

Q: How could we enable coverage in the tool?
A: Questa Verify Property represents formal code coverage, using the six code coverage types as Questa SIM. There are specific command options to run formal coverage. Use the -include_code_cov option with the formal compile command to instrument code coverage and cover bins during the formal compilation, then use the -cov_mode with the formal verify command to collect formal coverage, and finally, use the formal generate coverage TCL command to create the formal coverage report as it is not generated by default.

Q: Does Questa Verify Property support immediate and concurrent assertions? 
A: Yes, Questa Verify Property does support the immediate assertions except with procedural loops. Also, supports concurrent assertions that have no activation condition. 

Q: Why should we use formal verification over constrained-random verification?
A: Formal verification and simulation are both essential methods in the verification of digital designs. Use the formal verification in the very early phase of your design process to check exhaustively your design and remove any bugs as necessary from the beginning without the need for building a testbench. However, it may not cover every possible scenario or dynamic interaction due to computational limitations. Simulation, on the other hand, offers extensive coverage, allowing for the validation of dynamic behaviors. By combining the strengths of both formal verification and simulation, verification engineers can achieve higher confidence in the correctness of their digital designs. 

Q: How to use the multi-grid option if supported in the tool? 
A: You can use the -jobs option to specify the number of engine processes. The default value is 16 if you are using the new QOSF license.
This multi-core analysis splits the formal problem into separate processes that run in parallel, which can reduce analysis time significantly. Unless otherwise specified, these engine processes run on the same machine. Use the configure grid submit directive to specify other machines to run on a grid. 

Q: How could I use the tool to verify standard protocols? 
A: The tool is shipped with a Questa Formal Library, also known as QFL. This library has a set of pre-defined qfl_memmap_interface modules for standard buses like AMBA AXI and APB. The qverify_memmap utility creates a binding module that includes an instance of the appropriate interface module and connects it to the memmap ports of a set of qfl_memmap_reg checkers. 

Q: Do I need to have a Questa Visualizer license to run the tool? 
A: No, the Questa Verify Property license feature is enough to invoke Visualizer GUI and run the tool with all the explained features.  

Q: What are the abstraction techniques mentioned in the webinar? 
A: Abstraction is the process of removing DUT elements from the formal analysis without touching the source code. The tool automatically identifies and removes most of the non-formal friendly elements from the analysis. However, you may want to remove the rest yourself with some abstraction techniques. These abstraction techniques are:

1. Setting constants to signals
2. Black-boxing modules
3. Cut-pointing signals
4. Counter abstraction
5. Memory abstraction

Please refer to Verification Academy for more information. 

Q: What is the difference between formal compile -G and formal compile -g?
A: formal compile -G overrides the final value of the VHDL generic or Verilog parameter specified by name that received explicit values in generic maps, instantiations, or from defparam. Whereas, formal compile -g assigns a value to only those specified VHDL generics and Verilog parameters that have not received explicit values in generic maps, instantiations, or via defparams. 

Q: Can you confirm, that Questa Verify is an extra feature that requires a separate license ($$$$)? 
A: Yes, Questa Verify Property is an advanced feature that typically requires a separate license. You should have the "Questa Verify Property Ap SW - SfPrc" license feature.  

Q: What are the major differences among other tools such as Lint or CDC tools?
(OR)
Q: How is Questa Verify different than other tools(i.e. Questa Check, Questa Formal, Questa Inspect, etc.)?
A: Each tool in Questa tools is designated for a different verification area. Questa Verify Property mainly focuses on exhaustively proving or disproving design properties in the context of functional verification, giving you more confidence that your design behaves as expected. 

Q: .log vs .rpt ... what is the difference? It sounds like .rpt is a summary of the .log. 
A: The formal_verify.rpt file contains more detailed information than the formal_verify.log file. It includes Clock Relationships, the Initialization Sequence used, Port Constraints, the number of registers and memories that are uninitialized at the end of the initialization sequence, and the Formal Netlist Statistics. It also provides the results, specifying which properties are Fired, Proven, or Covered, and ends with Process Statistics and a Summary Table similar to the formal_verify.log file but with more details. 

Q: How do you check that your assert properties are correct? By injecting faulty DUT behavior to see if they fire? E.g. by cutpoints? 
A: To ensure your assert properties are correct, one effective method is to introduce a bug into the design, either by altering the RTL or using the tool options like cutpoints, to see if the property fires. Mutation coverage can also help determine which logic the property covers.
It's essential to consider various factors, such as whether the injected bug is in a spot the property would catch if the property aligns with the specification, and if the assumptions are over-constraining the design. Running signoff code coverage of the property can also help identify which parts of the design are covered when the property is proven, and adjustments can be made if the coverage is less than expected.

Q: Are there any larger length resources that go through the entire process of project setup to the end goal for Questa Verify? 
A: Some useful resources to check out for more information or examples would be: 

1. The user manual at Questa PropCheck User Guide (siemens.com) 
2. The command reference manual at Questa OneSpin StaticFormal Command Reference (siemens.com) 
3. The tutorials which are shipped with the tool
4. The On-Demand Training available at Functional Verification - Learning Paths - Questa Formal Verification (siemens.com) 
5. Verification Academy where you can register for free using the following link Verification Academy: Tools and training for functional verification | Siemens Verification Academy. You can find various demos on Questa Verify Property and other formal tools at Browse all Demos in Siemens Verification Academy | Siemens Verification Academy

There is also a Support Center which is a Siemens interface for handling support cases, downloading tools, finding knowledge-based articles, or even support kits to assist you in gaining more knowledge for a certain area. You will find on the Support Center various resources for Questa Verify Property. You can find the link for Support Center at Support Center (siemens.com).