Subject: Re: PSL-SystemVerilog unification (review of SVA proposal)
From: Bernard Deadman (bdeadman@sdvinc.com)
Date: Mon Feb 10 2003 - 13:54:43 PST
At 09:37 AM 2/7/2003 -0600, Harry Foster wrote:
>However, it is now
>time to build consensus and unify (in terms of syntax and semantics) any PSL
>and SVA overlap for a future 1.1 version of a PSL LRM, which will reflect
>the unification effort.
Harry,
Thanks - you seem to have set us an interesting puzzle, that few seem to
want to address. When you wrote "...and unify any ... overlap", were you
hoping we could find some??? [[Is this the old schoolboy joke, "what's the
difference between a rock and a bowl of jelly"? The problem is I don't
remember if there was a punchline....]]
Instinctively I think the two languages are probably doing roughly the same
thing, in the majority of circumstances, therefore there ought to be a
chance of achieving consensus on the semantics, but do you (or anyone else
for that matter) have a suggestion for a method of constructively comparing
formal semantics with partially defined informal semantics? Surely one of
the reasons PSL (and other contender languages like CBV & ForSpec) have
formal semantics is to clearly define all the corner cases, rather than
rely on dubious single case diagrams and ambiguous English
descriptions? As an example, what does one assume when SVA contains
fragments like
boolean_expr '=*' range
for which there is apparently neither an example nor an 'English' explanation?
Equally, how will we be able to measure that we have achieved alignment?
The semantics problem looks hard, but I'm much more worried by the widely
divergent syntax, that seems to be beyond your request to "identify any
syntax concerns". My forecast is any engineer who has to write day in and
day out in BOTH PSL and SVA will get hopelessly confused and make a *LOT*
of stupid mistakes with things like the use of () versus {} and the
syntactically similar but semantically quite different [*] terms.
Unless I missed something, the syntax of SVA seems so far removed from that
of PSL, that I strongly doubt a couple of changes will achieve alignment.
It seems to me the only viable alternatives are more radical, and I can see
at least three options:
1) I don't imagine the PSL committee is willing to halt the standardization
of 1.0 to accept unproven OVA/SVA syntax without an incredibly strong
technical reason, which nobody seems able to make therefore it's
conceivable that OVA/SVA syntax could be forced on the PSL committee
because of a political, rather than technical, decision by Accellera. In
this case:
i) PSL 1.1 (note: not PSL 1.0 because that needs to be in the
marketplace today) has to adopt SVA syntax
ii) any properties that have been written in the 1-2 years before 1.1
is released and gets vendor support will be effectively junked
iii) someone has to write formal semantics for SVA a year from now
iv) SVA will have to be extended up to the existing, proven capability
of PSL for formal checking
iv) vendors will have to figure out how to get SVA to work in a formal
model checking engine
2) the goal of alignment is abandoned and OVA/SVA and PSL co-exist, thereby
inhibiting the interchange of IP which seems stupid to me - they're
sponsored by the same body for the same applications for heavens sake!
3) Accellera acknowledges the PSL regular expression syntax is correct,
accurate, fully defined, with a wider scope than the SVA proposal and ready
now and they make a decision to change the incomplete SVA to incorporate at
least SERE's plus composition of SERE's, in place of (roughly) the
sequence_expr plus and/or/intersect now before usage gets
entrenched. Subject to my intuitive understanding of the informal SVA
semantics I believe this is possible, and that the higher levels in SVA can
be largely retained with relatively little modification.
I suspect this is not what anyone wants to hear, but my most constructive
suggestion is Accellera should adopt 3) as the only logical conclusion,
because I believe it will be possible to grow this form of SVA in the
future to absorb most of the syntactic sugaring inherent in PSL, and that
this will be far easier than struggling to bring SVA to the level PSL has
already achieved.
I'm sure most members of the PSL committee would be reluctant to see the
LRM undermined by adoption of SVA, therefore I would rather abandon
unification (ie take option 2) rather than suffer the significant
compromises inherent in 1).
I would like repeat that in my opinion, anything other than firm,
immediate, courageous action to substitute the core of SVA with PSL will
leave the two languages hopelessly forked for the foreseeable future.
Regards
Bernard
====================================================================
SDV Inc. 9111 Jollyville Rd, Suite 102, Austin, TX 78759 USA
Phone: (512) 231-9806 xt 101 FAX: (512) 231-9807 Mobile: (512)
431-5126
Email: bdeadman@sdvinc.com Website: www.sdvinc.com
This archive was generated by hypermail 2b28 : Mon Feb 10 2003 - 14:11:07 PST