Subject: RE: assertion discussions of fvtc languages
From: Erich Marschner (erichm@cadence.com)
Date: Fri Apr 12 2002 - 06:37:04 PDT
John,
| 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.
I believe that the email from me that you have quoted indicates clearly that I tried to present to the Assertions committee both my understanding of Sugar AND my understanding of CBV, without overt bias. If, in those discussions, my understanding of Sugar was more accurate than my understanding of CBV, it is because the complete Sugar 2.0 definition had been published and presented already (on March 20th), whereas we were all still waiting for the complete CBV specification to be published. In particular, although the 'past' operator was presented in your roadmap presentation on February 20th, it was not mentioned at all in the slides of your presentation on March 20th, which was supposed to be the final language presentation before the ballot. (And saving past values in variables is not unique to CBV - Sugar and HDLs in general do this quite well.)
Since even now I probably don't understand CBV well enough to represent it correctly, I will refrain from mentioning it further in other venues.
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: John Havlicek [mailto:havlicek@adttx.sps.mot.com]
| Sent: Thursday, April 11, 2002 5:09 PM
| To: vfv@eda.org; assertion@eda.org
| Cc: john.havlicek@mot.com; kurt.shultz@mot.com
| Subject: assertion discussions of fvtc languages
|
|
| 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 : Fri Apr 12 2002 - 06:38:27 PDT