Subject: [sv-ac] Thoughts on enhancements.
From: Adam Krolnik (krolnik@lsil.com)
Date: Wed Jul 30 2003 - 09:14:36 PDT
Hello all;
In reviewing the capabilities of the 3.1 spec and the enhancments, I'd like to make
some observations possibly leading to requests for enhancement.
1. Allowing assertions in interfaces is great because you can write assertions
about how the signals of an interface are expected to work. However
interfaces may not contain a clock signal (or reset) as these typically
are passed separately to the modules connected to interfaces.
Thus there is a problem of specifying a clock for properties of an interface.
Solutions previous to SVA have used a `define to reference a global clock for the
system. However going forward I'd like to have a better method as this one is
limiting all assertions to the use of only one clock. Many systems are contain
multiple clock domains and in order to reuse design elements properly, they can't
use a global clock.
Note, allowing assertions as part of a struct (or a module without a clock signal)
present the same problem - there is no local clock signal in the scope.
2. Assertions written in an interface (I believe) will be local to the scope
where the interface is instantiated - which is usually the parent of the modules
communicating. Thus any errors detected by the assertions will reference the parent's
scope when reporting. It would be best to have assertions represent the scope that
is driving the interface in the incorrect way. Note, it would not be good to
have the assertion in the scopes of all modules connecting to the interface - you
would get the same error message multiple times.
If one could place assertions in the mod_port definition, then it should be possible
to specify that these assertions should be located with the module specifying that
mod_port for an interface. With this, a user can write an assertions specific to
the driver of that particular information and obtain an error message referencing the
drivers scope in the failure message.
So I would like to see an enhancement to allow mod_port definitions to contain
assertions, properties and sequences so that these elements can be instantiated
specific to the module using the mod_port.
Note, I would also like to ensure that a tool is not restricted from using assertions
in a mod_port definition when dealing with a module using a different mod_port. I'm
thinking about tools (formal) that operate on a single module and would want to make
use of any assumptions, assertions, etc. to constrain the module interface.
3. Early on in SV-AC, we decided to only use assert and cover. We decided that assume
was not necessary. I asked why not include more directives from PSL (assume, cover,
assert, assume_guarantee.)
4. We had discussions about including assertions in functions but did not complete
the discussions. Would this be a good time to have these discussions? I would like to
see assertions inside functions since many people use functions to define logic.
5. If we are thinking of extending modules to allow sequences or properties
to be passed in, and we are looking at ways to wait/sample/expect assertion (names)
it would be good to also send this information in or out of a module.
Modules currently can't include events in their ports. It may be interesting to
be able to pass in ('ended aproperty') and even pass it out.
6. Is there other PSL functionality that could/should be part of the SVA properties
and sequences? Should SVA be expanded to the rest of PSL?
In summary, I would recommend these enhancements to be added to the list:
1. Handle clocks not local to a particular scope (interface, struct, module, etc.)
2. Assertions/properties/sequences within a mod_port declaration.
3. Use more PSL verification directives. (all?)
4. Allow assertions in functions.
5. Extend module ports to include sequence, property and event passing.
6. Expand properties/sequences to additional PSL constructs.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Wed Jul 30 2003 - 09:15:27 PDT