Assumptions practical Approach in Formal Environment?
In reply to janki_ps:
Went to https://chat.openai.com/ and reviewed the answer.
[Ben] in formal verification with systemverilog, how are SVA assumptions used?
[ChatGPT]
In formal verification using SystemVerilog Assertions (SVA), SVA assumptions (SystemVerilog Assertions Assumptions) play a crucial role in guiding the formal verification tool to make specific assumptions during the verification process. These assumptions help the tool to explore the state space efficiently and prove or find counterexamples for your assertions.
Here is how SVA assumptions are typically used:
Defining Assumptions:
Use the assume keyword in SystemVerilog Assertions (SVA) to specify assumptions about the design or the environment.
These assumptions typically represent conditions that you want to assume true for the purpose of the formal verification.
// Example: Assuming a signal ‘reset’ is asserted initially
SVA assumptions: assume property (initial reset |-> ##1 ~reset);
In this example, the assumption is that the reset signal is asserted initially, and then it should be de-asserted after one time unit.
Guiding the Formal Verification Tool:
SVA assumptions guide the formal verification tool to explore the design space by assuming certain conditions.
This helps in narrowing down the potential state space to be explored and makes the verification more targeted and efficient.
// Example: Assume certain conditions for formal verification
SVA assumptions: assume property (my_condition);
Here, my_condition represents a condition that you want to assume true during formal verification.
Handling Complex Scenarios:
In complex designs, there might be scenarios where certain assumptions can simplify the verification process.
For example, you might assume specific initial conditions, specific values of certain signals, or certain sequences of events.
// Example: Assume a specific sequence of events
SVA assumptions: assume property (A |-> ##1 B ##1 C);
In this example, you are assuming a sequence of events: A must happen, followed by B then C.
Iterative Refinement:
During the formal verification process, you might iteratively refine your assumptions based on the results obtained.
If the verification fails, you might revisit and refine your assumptions to cover more cases or to make them more accurate.
// Example: Refine assumptions based on verification results
SVA assumptions: assume property (new_condition);
Here, new_condition represents a refined or additional assumption based on the results obtained from the formal verification.
It’s important to carefully choose and review the assumptions as overly restrictive or incorrect assumptions
can lead to false positives or false negatives in the verification process.
Additionally, the use of assertions (sequence and property constructs) in conjunction with assumptions
helps in creating a comprehensive and effective formal verification environment.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.