Mission Statement

The Accellera Formal Property Language Technical Committee is chartered with the responsibility of defining a property specification language standard compatible with both the Verilog (IEEE-1364) and VHDL (IEEE-1076) language.  This formal language is targeted for both dynamic verification (e.g., simulation) as well as static verification (e.g., model checking). In addition, the Formal Property Language Technical Committee is chartered with:

Committee Members

The committee is comprised of the following members:

Operational Ground Rules

Recordkeeping

 At ever meeting we will select a volunteer to take minutes of each meeting. 

Scheduling Meetings

Definition of Quorum 

A quorum is defined differently for "more significant" and "less significant" issues. For more 
significant issues, 80% of voting members must cast a vote for the decision to be valid, and to achieve this high percentage, such ballots will be done by email. For less significant issues, such as operational decisions made 
during meetings, only 50% of voting members must cast a vote for the decision to be valid. However, any voting member may request that a less significant question be reballoted as a more significant question, under the 80%, email procedure. This was generally agreed to, and later (see below) was approved by ballot. 

How Motions are Made 

Advance notice, by email, of a motion to be made is acceptable - even encouraged, to put the issue on the agenda, so that people concerned with the motion can make a point of attending that meeting - but that there should be at least one meeting where the motion is discussed before any vote is taken. To enforce this, a motion can only be seconded in person, at a meeting, by a voting member. For major issues, we cannot both introduce a motion 
and vote on it in the same meeting, in order to ensure that any member concerned with the issue have an opportunity to participate in its discussion and in the vote. 

Voting Members and Balloting

  1. A "voting member" is anyone who has attended 3 of the last 4 meetings. 
  2. A ballot regarding a "less significant" decision requires a quorum 
    consisting of at least 50% of the voting members (at the time of the vote). 
  3. A ballot regarding a "more significant" decision must be taken by email 
    and requires a quorum consisting of at least 80% of the voting members (at 
    the time of the vote). 
  4. Except for final approval of the standard, each ballot will be decided 
    by simple majority. 
  5. Final approval of the standard will require a quorum of 75% of the 
    voting members, and a 75%positive vote. 

Section 1

Introduction

1.1 Motivation

Due to the lack of a property specification language standard, many formal languages have emerged in the industry.  For early adopters of formal methods, multiple property specification languages has resulted in increases in cost and complexity associated with formal tool evaluation and integration.  More significantly, however, is that the lack of a specification standard provides no incentive for the design community to abandon its natural language (and ambiguous) approach to specification.  To address this problem, the Accellera Formal Property Language Technical committee has been formed define a Property Specification Language (FPL) standard compatible with both the Verilog (IEEE-1364) and VHDL (IEEE-1076) standards.  This document defines the design objectives for the FPL standard.

Keywords

The meaning of these keywords, used throughout this document, are:

·         must - the goal or requirement is a fundamental objective and cannot be compromised.

·         should - the goal or requirement provides useful characteristics and signification benefits, yet it is not a fundamental objective.

·         desirable - the goal or requirement may enhance usability or other specification characteristics; however, if not met, overall objectives will not be compromised.

1.2 Goals

The basic goals of the proposed Property Specification Language (FPL) are:

·         Simplicity - the FPL must be easy to understand and use by engineers familiar with today's HDLs.

·         Conciseness - the FPL semantics must be unambiguous.

·         Expressiveness - the FPL must support temporal logic.

·         Consistency - the FPL must support an assume guarantee reasoning paradigm, which is to say environemntal constraints as well as design properties use the same syntax and semantics.

·         Generality - the FPL should be compatible (when possible) across simulations methods as well as formal methods.

·         Acceptance - the design community should actively embraces the FPL standard.

1.3 FPL Selection

In April 2002, the FPL Committee selected Sugar 2.0 from IBM as its . for standardization.

Section 2

Usage Models

This section is under construction and will define the usage model for the FPL in various verification environments.

Section 3

Requirements

This section is under construction and is intended to define and list the requirements for the FPL standard.  Initially, this section will list the "raw" requirements, which will be refined by the Technical Committee as time progresses.

webmaster

Last update on
Tuesday, June 18, 2002