Subject: RE: Sequential Regular Expressions as Assertions
From: Tom Fitzpatrick (fitz@co-design.com)
Date: Wed Mar 20 2002 - 12:52:05 PST
Hi Harry,
It's too bad that this issue got raised this late in the game, but here's
the way I see it. I believe that we on the Assertions committee are all
solidly in favor of including sequential regular expressions in assertions
as part of SystemVerilog3.0. With the announcement, press coverage and
positive response at HDLCon last week, it would really be a shame not to
capitalize on our momentum and I firmly believe that we can and will meet
the SystemVerilog3.0 timeline we all agreed to last week.
Unfortunately, any decision by the VFV committee won't happen until shortly
before we're due to lock down the SystemVerilog spec for ballotting. I find
it a little strange to be worrying about SystemVerilog being compatible with
a VFV language that hasn't been chosen yet, particularly when the VFV
committee explicitly rejected any requirements about being compatible with
SystemVerilog. The requirements approved by the VFV (that you distributed on
11/4/01) state that the FV language must be compatible with Verilog
expressions, but rejected requirements to be compatible with Superlog or
even Verilog-2001. This is an issue that you'll have to take up with them,
if you agree, and I'll leave that up to you.
It seems to me that the VFV committee chose to be more flexible in defining
their language, and that's OK. As you know, with the huge installed-base of
Verilog users out there, SystemVerilog doesn't have as much flexibility.
That being said, it may (and I stress *may*) be possible to modify the
proposed sequential expression syntax for the subset of regular expressions
we've defined in the DAS, but we'll have to wait until we've identified the
issues.
I propose that we continue in the Assertion committee to review the DAS spec
according to the priorities we agreed to last week. We should agree on the
semantics of expression sequences and, if we get that far, the
antecedent/consequent capability as well. After that, on our last meeting on
4/4, we should hopefully have time to explore syntax-only (not semantic)
changes that may make compatiblity with VFV easier. In the cases where CBV
and Sugar differ, we may be able to come up with alternatives, but we may
not.
There is some "clean up" time for the SystemVerilog 3.0 spec during April,
and it may be possible to conclude these hopefully-minor syntax issues as
part of the clean up (if Vassilios agrees). Again, this would only be for
regular expression semantics that are already approved by the Assertion
committee, so we would not be adding any new features, and I believe it
would be an acceptable risk to undertake.
We'll discuss this plan at tomorrow's meeting.
Thanks for your help,
-Tom
-----Original Message-----
From: owner-assertion@server.eda.org
[mailto:owner-assertion@server.eda.org]On Behalf Of Harry Foster
Sent: Monday, March 18, 2002 3:10 PM
To: fitz@co-design.com; assertion@server.eda.org
Subject: Sequential Regular Expressions as Assertions
As many of you know, the Accellera Formal Verification Committee is nearing
the end of its language selection process--scheduled for early April. The
two candidate languages (SUGAR and Extended CBV) both support a syntax for
expressing regular expressions. I would hate to see the SystemVerilog and
Formal Property Language syntax for the basic regular expression differ.
This would only introduce confusion in the industry and minimize
interoperability between the SystemVerilog assertions and the formal
property language.
I would like the assertion committee to serious consider delaying adding the
sequential regular expressions to the 3.0 SystemVerilog draft. We should be
able to add this construct to the 3.1 December draft and align regular
expression syntax between the two committees. The SystemVerilog regular
expressions would be a subset of the formal property language regular
expressions. However, I feel that the syntax should really be the same.
We can discuss this during our upcoming meeting.
-Harry
This archive was generated by hypermail 2b28 : Wed Mar 20 2002 - 12:51:14 PST