Subject: RE: Sequential Regular Expressions as Assertions
From: Tom Fitzpatrick (fitz@co-design.com)
Date: Wed Mar 20 2002 - 14:56:50 PST
Hi Harry,
Thanks for clearing up the VFV Requirements thing. It seems to me that we've
got a workable plan, and if we can identify the syntax issues early enough,
we'll be able to resolve them and still meet the SystemVerilog 3.0 schedule.
Sounds like a win-win.
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: Wednesday, March 20, 2002 5:05 PM
To: fitz@co-design.com; Harry Foster; assertion@server.eda.org
Subject: RE: Sequential Regular Expressions as Assertions
> 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.
This is a little misleading. It was not a requirement that the formal
property language be compatible with Verilog, Verilog-2000, SystemC, VHDL,
etc. The requirements R2a, R3a, R4a, R4b, and R4c stated that the final
language must demonstrate how an expression would be used within the
language. For example, requirement:
R2a: The language must define how Verilog expressions may be used in its
statements.
The donated language need only demonstrate the Boolean layer for one
language. In fact, if you look at Sugar (for example), the temporal layer
is clearly separated from the Boolean layer. Hence, any valid HDL Boolean
expression ultimately would work (with appropriate parenthesis). IBM, for
example, has demonstrated that their language works with Boolean expressions
from Verilog, VHDL and EDL (IBM formal modeling language). CBV has
demonstrate the Boolean layer for Verilog and sketched out VHDL as well
(although, unlike IBM, I understand that they haven't finished a yacc parser
for VHDL yet--but they plan to do this too).
The committee decided (and we had this discussion during one of our
meetings) that, to start, it was not necessary for a donated language to
demonstrate the Boolean layer for all existing HDL's (only needed to
demonstrate it with Verilog). Ultimately, a Boolean layer bindings needs to
be worked out for all HDL's including SystemC.
Keep in mind that the SystemVerilog DAS proposal, for the first time, is
trying to introduce a simple Temporal component to the Verilog language
through the sequential regular expressions (i.e., reasoning about or
analyzing sequences of events over time). I think it would be wrong to
ignore the expertise and experience from the formal committee members....
As I've stated--I'm very much in favor of the sequential regular expressions
as part of the SystemVerilog standard. I think the assertion committee
should try to maintain compatibility in the basic syntax for our subset of
regular expressions. I don't think that this is an impossible task (in fact
if you study the Sugar and CBV proposal's for intervals we are not that far
off...) and I think we should be able to tweak the syntax once the final
formal language is selected in mid-April.
-Harry
This archive was generated by hypermail 2b28 : Wed Mar 20 2002 - 14:56:09 PST