RE: Informal proposal for Issue Group D - named constructs: issues

Tej, some initial thoughts on this.
 
For proposal 2, SVA does now have (in next LRM rev) types, so this proposal
is out. Proposal 3 I dislike "replacing" the Boolean/Sequence (see next
stmt).
 
I would rather suggest that we should keep the *kind* of Boolean/Sequence
and add an additional *type*. In the spirit of Proposal 1 I think it would
be best to have types that are independent from the HDL but rather can be
mapped easily. For your mentioned ambiguity I would suggest that may be
having either either all type or all untyped args to minimize such issues
may be wise, of course defining the mapping from PSL "types" to the HDL
flavor types would also be needed.

Thx.
-Bassam.
 

--
Dr. Bassam Tabbara
Architect, R&D
Novas Software, Inc.
(408) 467-7893
 
  _____  
From: owner-ieee-1850-extensions@eda.org
[mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of Singh, Tej
Sent: Monday, December 27, 2004 10:48 AM
To: ieee-1850-extensions@eda.org
Subject: Informal proposal for Issue Group D - named constructs: issues
Hi All,
 
Please refer to Group D in the Issues List at
http://www.eda.org/ieee-1850/Issues/Issues.html
There are three possible options to extend PSL declaration formal types
which are listed below. 
Before I submit a formal proposal, I will like to discuss the three
proposals to get the opinion of
the commitee as to which one should I work on.
 
Proposal 1
----------------
 
The proposal extends the  types allowed in LRM 1.1 with the following
 
bit
bitvector
numeric
 
Refer to section 5.1.1, 5.1.3 and 5.1.4 for HDL flavour types that can map
onto these PSL types.
 
There are two issues with this proposal
 
1. Due to many-to-one mapping from HDL type to PSL type, this proposal
causes ambiguity issues
in VHDL. For e.g.
 
sequence s(bit b1, b2) is {b1 = b2};
 
The sequence expression is ambiguous as 'b1 = b2' can resolve to std_ulogic
or bit.
 
2. The PSL declaration can no more be semantically resolved just by looking
at the 
declaration alone. For e.g. consider this VHDL example
 
signal sig_bit1: bit;
signal sig_bit2 : bit
signal sig_logic : std_logic;
 
sequence s(bit b1, b2) is {sig_bit1 = b1 and b2};
assert always s(sig_bit2, sig_logic);
 
The expression of sequence 's' is valid but becomes invalid when it gets
instantiated because the operand of 'and' is two different type.
 
If we adopt this approach, the LRM will have to specifically mention that
the resultant expression after replacing formal with actual 
should be a valid expression in the flavour for issue #1.Issue #2 is
inherent to this proposal and tools will have to make sure that the
expression is resolved correctly
 
Proposal 2
---------------
 
The proposal extends the  types allowed in LRM 1.1 with the following
 
anytype
 
Any HDL flavour  variable type can map to the formal of this type.
 
For e.g.
 
sequence s(anytype b1, b2) is (b1 = b2};
 
This is more like a SVA approach where the formals are not typed.
 
Issues with this propsal are
 
1. Makes the language very loose. The declaration no more contains the
information about the parameter types that it can take.
 
2. Same as issue #2 of Proposal 1.
 
Proposal 3
---------------
 
This proposal replaces the 'boolean' type in LRM 1.1 with the following
 
Any HDL Variable Type.
 
For e.g.  
 
VHDL example
sequence s (std_logic b, std_logic_vector bv, my_record m, sequence s_param)
is .......
 
SystemVerilog Example
sequence s (bit b, int i, my_class mc, sequence s_param) = ...............
 
The const becomes a type quailifier rather than a type. It can be applied to
any HDL type but not to PSL types (sequence and parameter).
 
This takes care of the issues in Proposal 1 and 2. It makes the PSL
declaration as parameterizable as the
function calls in the language flavor.
 
I do not foresee any issues with this proposal.
 
Regards
Tej