Subject: assertion discussions of fvtc languages
From: John Havlicek (havlicek@adttx.sps.mot.com)
Date: Thu Apr 11 2002 - 14:08:47 PDT
Dear Formal Verification and Assertion Technical Committees:
It has recently come to my attention that there has been a fair
amount of discussion in the Assertion Committee over the past 3
weeks about the languages being considered in the Formal Verification
Committee. The majority of this discussion has revolved about
features in IBM's Sugar2.0 proposal. There has been some discussion
of CBV. To the best of my knowledge, little of this discussion
has involved IBM or Motorola representatives familiar with the
proposed formal verification languages.
In this and several subsequent mails, I want to make some clarifying
comments on the discussion of CBV that has appeared on the Assertion
Committee reflector. I also want to balance the discussion by
providing examples of CBV where only Sugar2.0 was discussed before.
My comments on the first message from the Assertion reflector appear
below.
Best regards,
John Havlicek
===============================================================================
| -----Original Message-----
| From: Erich Marschner
| Sent: Thursday, March 21, 2002 5:48 PM
| To: 'fitz@co-design.com'
| Subject: RE: Minutes of Assertion meeting 3/21/02
|
|
| Tom,
|
| Some comments on the notes:
|
| | Erich pointed out 4 syntax issues that may be affected by
| | compatability with
| | the VFV language:
|
| | What denotes a sequence?
| | What separates elements in a sequence?
|
| Sugar uses braces and semicolons - e.g., {a; b; c}
| CBV uses brackets and semicolons - e.g., [a; b; c]
|
| | What is the repeat operator?
|
| Sugar uses brackets, in many different flavors:
| a[*] 0 or more successive cycles
| a[+] 1 or more successive cycles
| a[*n] n successive cycles
| a[*n..m] at least n successive cycles, and up to m
| successive cycles
| a[=n] n not-necessarily-contiguous cycles
| etc.
| CBV uses braces (but syntax not fully defined yet):
| a{*} 0 or more successive cycles
| a{n} n successive cycles
| a{+} 1 or more successive cycles
| a{?} 0 or 1 cycle
| a{n to m} at least n successive cycles, and up to
| m successive cycles
"Cycles" is not accurate here with respect to CBV unless
"a" is a boolean expression. "Contiguous, but non-overlapping,
repetitions" would be a more accurate phrase when "a" is a general
regexp.
|
| | What is the clocking method?
|
| This is a bit more involved. Sugar allows "sequence @clk",
| where clk is any Verilog expression (presumably including
| "(posedge clk)"). CBV seems to be more involved.
Clocking in CBV regular expressions is defined using three
regexp timing operators. For "e" a boolean expression, the
operators are
S@(e) // sample--set sampling event to e, but do not align
|@(e) // align--align to nearest weakly-future event of e, but
// do not change the current sampling event
$@(e) // sync--equivalent to "|@(e)S@(e)"
Boolean expressions include expression such as
"a_posedge(clk)"
"(a_posedge(clk) & ~idle)"
These operators afford great flexibility in defining the sampling
under which regexps and sub-regexps are matched. These operators
behave analogously to the operators
sample @(e)
align @(e)
sync @(e)
in the statement layer of CBV.
Here is an example of a CBV regexp with timing operators:
$@(e)[u;v;S@(f)[w;x];y]
where "e", "f", "u", "v", "w", "x", "y" are all boolean expressions.
This regexp is equivalent to the following regexp without timing
operators:
[
[~e{*};e], // $@(e) causes alignment to e and sets sampling event to e
u;
[~e{*};e], // ";" under sampling at e causes alignment to e
v;
[~e{*};e], // ";" under sampling at e causes alignment to e
w; // S@(f) does not align, but changes sampling event to f
[~f{*};f], // ";" under sampling at f causes alignment to f
x;
[~e{*};e], // ";" under sampling at e causes alignment to e
y
]
Note that ";" is the non-overlapping concatenation operator,
while "," is the overlapping concatenation operator.
|
| The bottom line is that, except for clocks, the main
| syntactic difference is that one uses braces for sequence,
| brackets for repeat count, and the other uses the opposite.
| Also, one uses '..' for a range, the other uses 'to'. So it
| should be easy to adopt/adapt.
This archive was generated by hypermail 2b28 : Thu Apr 11 2002 - 14:11:47 PDT