In reply to MICRO_91:
In reply to ben@SystemVerilog.us:
I appreciate the honest feedback however, the student in me would like to know your views on the following :
The design would update the register in either NBA or in Active ( via loopback from NBA to Active ).
Knowing section 16.11 of the LRM , how is it that it’s considered a bad style ?
It’s not as if I am using a tool’s restriction/implementation to achieve the solution.
You are writing assertions that compare updated values of variables (updated in the NBA) to sampled values of variables. To do that, you depend on how simulation uses regions to simulate concurrency. So now, you are getting into the heart of the tool.
SVA specifically uses the sampling of signals before any update to keep things CLEAN.
Instead of comparing updated values of variables to sampled values of variables,the better approach is to compare sampled values to past values.
Could you elaborate on this ?
In SystemVerilog formal verification, there are no time regions or concepts like “Prepone” and “Active”, “NBA” as you might find in simulation. These concepts are specific to simulation and are used to control the timing and scheduling of events within the simulation environment. Time regions, such as “Prepone” and “Active”, NBA" are used to model the timing behavior of a hardware design.
In formal verification, the focus is on proving the correctness of the design without relying on simulation time. Formal tools use mathematical algorithms and symbolic reasoning to exhaustively analyze the design’s behavior and properties, without considering the concept of simulation time or event scheduling. Formal verification tools explore all possible input combinations and paths within the design to ensure that it adheres to specified properties or assertions.
Therefore, while simulation heavily relies on the concept of time and event scheduling, formal verification operates independently of simulation time and does not use time regions or similar concepts. Instead, it works with logical and mathematical models to prove or disprove the correctness of a hardware design based on formal specifications and assertions.
**Example:**
bit[3:0] state, nxt_st;
always @(posedge clk) nxt_st <= state;
function bit[3:0] updated_nxt_st();
return nxt_st ; // returns DUT's updated NBA value of the same time step
endfunction
ap_not4formal: assert property(@(posedge clk)
updated_nxt_st() == state) |-> b; // registered state==sampled state |-> b
// works in simulation because of SV processing of regions
// In FV, since it knows nothing about Regions, the above assertion is interpreted as
ap_not4formal_interpretation: assert property(@(posedge clk)
nxt_st == state |-> b); // which is incorrect; this models a wire and not a register
Since I could use the same basic logic to enhance the code to a different pattern detection , I am not sure on how the requirements are not being met .
Your approach is NOT how SVA is intended to be used. SVA is based on sampled values and does not depend on how the tool processes SV. Now, by putting into your assertions the updated values of values along with the sampled values of variables, you are adding another layer of complexity in understanding the properties.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog