QUESTION: Which methodology is good from below and please give pros and cons of both:
SV Assertions in separate file and include it in RTL source using `include directive (please give one complete example if possible)
SV Assertions in separate file and use bind directive
ANSWER:
The use of the bind directive with assertions in modules or checkers is the preferred approach for the following reasons:
Separates the assertions from the design
Ease of modifying assertions without affecting design or time-stamp of designs, as a change in time-stamp may cause un-needed resynthesis of the design.
Minimizes the burden on a synthesis tool to optimize out supporting code used for the assertions and not in the RTL design.
The use of the `include of straight inline SVA code is dangerous as it can cause some errors in the synthesis process; That code has to be optimized out by the synthesis tool, and any incorrect assignment to supporting SVA code (e.g., to real RTL) can be catastrophic.
The use of the `include of a checker module again brings the time stamp problem and is not a clear separation between RTL and verification.
A problem I see with bind is if you have a larger test framework with a big hierarchy of modules. You then need to maintain a list of all the SVA modules to bind to in the various testbenches, and it seems easy to miss something. For example, let’s say you add a submodule to the counter module with its own SVA bindfile. You then need to update all the testbenches that use counter somewhere in the hierarchy with a new bind directive. With `include, you guarantee that you don’t miss any assertions.
Furthermore, you have another layer of maintenance whenever you add/remove ports or parameters to the module you bind to. With ports this can be done automatically with the .* notation, but this is not available for parameters, so if you add a WIDTH parameter to counter, you need to update the binds in all testbenches with #(.WIDTH(WIDTH)). With `include, added parameters will automatically be available in the assertions file, and it is guaranteed that there are no mismatches between the parameter in the module and the bind file.
If you surround include* with something like *ifdef SIMULATION, it seems to me that you cover all the items in your list of benefits for using bind. Any comments on this?
I agree with many of your assessments as to why bind is difficult here. Ben’s bind solution requires a bit of overhead for designs that are being developed, and often changing.
There’s similar problems with parameterization and bind. Say an assertion only exists under a generate if within the RTL:
generate
if( SOME_PARAM )
begin : gen_context
//assertions here
end
endgenerate
I’d also argue that Ben’s #1 point is a disadvantage - not an advantage of using bind. Having the designer code the assertion right within the code is the correct context. You see intent right along side with the code. That’s a good thing for including the assertions in the design. It also means that there’s nothing else for a design integrator to do in order to get the assertions. If you instantiate the design in RTL, you get the assertions too.
Another note - we don’t include the assertions - they're directly in the RTL. I'm of the opinion that include abuse is a bit prevalent in the verification space. Excessive wildcarded imports too.
We also have many assertions coded within SystemVerilog Interface RTL. I don’t think the “bind” solution would work with here, would it? This works great in RTL, as again, the designer instantiates an interface to use in RTL - and gets along side of it protocol checkers for free - without any effort required.
Ben’s #2 point is valid - timestamping and triggering make dependencies. But to me, this is a secondary or even tertiary concern. #3 point is related, but really a don’t care for our team, and I’m doubtful as to how much cost this really is.
We do surround our assertions with a similar ifdef SIMULATION (or translate_off/on pragmas) to leave that code out of the synthesis.
As a RTL designer, now heavily using SystemVerilog code within our synthesizable design, I do struggle a bit with what/how much “simulation/verification only” code to include in the set of files that Synthesis “sees”. It’s certainly something new to think about.
Ben’s #1 point (Separate the assertions from the design) is a disadvantage - not an advantage of using bind. Having the designer code the assertion right within the code is the correct context.
Assertions separate or within RTL designs: This is generally a policy issue directed by management. Large corporations are generally very “process, disciplined” oriented; you practically need permission signatures for everything. Correctly so, management is very worried about respins, particularly when done for stupid errors.
I can see why one may believe that’s a good thing for including the assertions in the design. It also means that there’s nothing else for a design integrator to do in order to get the assertions. If you instantiate the design in RTL, you get the assertions too. However, here are the many issues with that:
[list=a]
Timestamp of design: (already addressed in above discussion)
Need of pragmas: Not all assertions can be written strictly with raw SVA. Many require supporting code, and others are written with raw SystemVerilog with tasks (see my papers #1#2 in my signature). A quick example of an SVA assertion requiring supporting logic is one where every REQ must have its own ACK, and any pending REQ is not satisfied with a single ACK. Putting this supporting code with the RTL requires pragmas (like synth_off synth_on). This is another potential source of errors.
Verification of assertions: Complex assertions need to be verified individually. Putting them within the design now makes it more difficult to check the assertions separately.
Code review complexity: There are several aspects to code reviews, one of which is style, organization, load on achieving the desired speed and power, addressing multiclocking issues. Another aspect is the correctness of the code for the design. This is where assertions come in. But here again, there are 2 classes of assertions: one to verify that the design meets the external requirements that came in from the initial system specs. Another class of assertion deals with coverage and design specific exclusive to the RTL design, often imposed by the designer. All that extra SVA and supporting code within the RTL is very combersome.
[*]
assertions coded within SystemVerilog Interface RTL. I don’t think the “bind” solution would work with here, would it?
I generally agree with this premise provided the interface is not part of the RTL port list for the reasons mentioned above.
[/list]
While I agree that having assertions directly in the design is nice, using `include seems like a good option because it pretty much covers all the benefits of the bindfiles, without the following drawbacks:
Maintenance burden on bind statements in all testbenches. Risk of missing assertion files.
Maintenance burden of parameter associations in all testbenches. Risk of mismatch between bindfile parameters and RTL parameters.
Inability to add assertions in SV interfaces. (?)
Extra coding overhead with parameter/port list in bindfiles and bind statements in testbenches
You could also make a custom macro that has an ifdef SIMULATION and/or synth_off pragmas around the include statement.
Timestamp of design
If you use `include, the assertion files will not be part of the synthesis makefiles, so adding an assertion will not affect the build system.
Need of pragmas
The bindfiles can import/refer to packages and their subroutines. For risks with synth_off, the solution with the custom assertion file include macro seems safe to me.
Verification of assertions
This is no problem with include. You can simply make a testbench that has all the signals used by the assertions, then include the assertion file in your testbench.
Code review complexity
If you use `include, the assertion code in the RTL will only be a single line of code. I don’t see this as a burden for reviews.
In reply to perchrc:
I see the benefits of the include*. I just don't believe that it is a good idea to hard-line SVA into the RTL; it should be in a separate file. Note that unlike the *include, the binding of the same checker (or module) to different entities (module, or interface [if checker] ) allows the use of different actual arguments.
One could argue that this is not really serious since the bound element ties to entities that have port-list, so the names of the variables and parameters used in the SVA file are the same as the formal argument of the RTL, thus there is no need for all that argument association when the `include is used. Anyway, just passing on something to consider.
On Inability to add assertions in SV interfaces. (?), SystemVerilog provides the checker construct that can be bound to an interface.
Ben Cohen SystemVerilog.us
I generally agree with this premise provided the interface is not part of the RTL port list for the reasons mentioned above.
Interface are part of the Synthesizable RTL portlist in our designs. Along with multi-dimensional arrays as first class citizens, Interfaces are probably the #1 advancement of the language moving us to the next higher level of digital design. There’s no reason to limit Interface use to just verification.
As mentioned, I agree with the problem of timestamps, just perhaps not the degree. I just feel that proposed solutions are not worth the cost of code clarity, self documentation, and ease of integration. I think including assertions into the RTL is a very good thing. Convincing RTL designers to think about, and code up more verification items is a good thing.
Perhaps, as usual this is a case of a not entirely black and white solution. The assertions I code up as an RTL designer, are rather straightforward: state machine decode errors, bus-interface protocol problems, etc. Nothing complex. But it really helps me during the design to state my assumptions and implications as code with assertions - right alongside my RTL.
Moving up - our verification teams are more experts at SVA, and do utilize many of the other constructs mentioned here.
