EPA/600/A-92/197
AIR TOXICS: THE RESEARCH CHALLENGE OF THE
1990 CLEAN AIR ACT AMENDMENTS
FRANK T. PRINCIOTTA
AND
DOUGLAS G. McKINNEY
AIR AND ENERGY ENGINEERING RESEARCH LABORATORY
U.S. ENVIRONMENTAL PROTECTION AGENCY
Toxic emissions from stationary air pollution sources have been recognized as a national
health problem for several decades. Unfortunately, a large percentage of these hazardous air
pollutant (HAP) emissions have not been controlled because between 1977 and 1990 the risk-
based Federal regulatory program to reduce them only addressed a few pollutants. Disputes
between industry, the U.S. Environmental Protection Agency (U.S. EPA), and environmental
groups over health effects data, exposure levels, and what constitutes an ample margin of safety
to protect the public health were the primary impediments to progress and limited the number
of National Emission Standards for Hazardous Air Pollutants (NESHAPS) issued to only ten.
The lack of progress toward reducing HAP emissions raised public concern and convinced
Congress to design a new regulatory approach which would avoid the past impediments and
accelerate emission reductions. The purpose of this paper is to describe the major provisions
of Title III of the 1990 Clean Air Act Amendments (CAAA) which formally established this
modified approach and the research which the U.S. EPA has initiated to support state and
Federal regulatory officials implement the extensive new provisions.
MAJOR TITLE HI PROVISIONS
Prior to the passage of the 1990 CAAA, all Federal regulations to reduce HAP emissions
were chemical specific, with emission levels set based on a specific risk level. This strategy was
substantially changed when Congress modified section 112 (now Title III) of the Clean Air Act
to establish a two-phased approach for regulating HAPs. The first phase requires national
technology-based standards for new and existing stationary sources which emit one or more of
the 189 HAPs listed under section 112 (b)(1). Emission levels promulgated for each specific
category or subcategory of sources will be based on the emission reduction capability of the
Maximum Achievable Control Technology (MACT) available. Once all the technology-based
standards are completed (ten years), the second phase of the program will be initiated. This
latter phase will determine if additional standards are necessary for a given source category or
subcategory to protect human health and the environment from residual risks caused by any
remaining emissions. The two-phased approach should accelerate HAP emission reductions
because the initial phase will reduce the majority of the risks without the need for contentious
risk assessments.
In addition to the two-phased regulatory strategy, Title HI includes a variety of special
studies which will generate data to support future national air toxics policies. These studies
require the U.S. EPA to either further characterize air toxic problems or improve the methods
and techniques used to define air toxic risks. Several of the most significant required studies
are described below.
-------
o Area Source Program: The purpose of this program is to reduce 75% of the
cancer incidence resulting from area sources (defined as stationary sources which
emit less than 10 tons of a single HAP or 25 tons of a combination of HAPs) of
hazardous air pollutants in urban areas. The study requires the U.S. EPA to
initiate an urban toxics research program and to produce a Comprehensive
National Strategy which must identify the 30 pollutants that pose the greatest
threat to public health and ensure 90% of the area sources which emit these
pollutants are subject to standards. The strategy developed must be provided to
Congress by November 1995.
o Great Waters: The purpose of this study is to identify and assess the extent of
atmospheric deposition of hazardous air pollutants to the Great Lakes, the
Chesapeake Bay, Lake Champlain, and coastal waters. Within five years, the
Administrator must determine whether further emission standards (beyond those
required under other portions of sec. 112) are needed to prevent serious adverse
effects to any of the Great Lakes or coastal waters.
o Coke Oven Production Technology: Requires DOE and EPA to jointly
undertake a 6 year study to assess coke oven production emission control
technologies and assist in the development and commercialization of technically
practical and economically viable control technologies which have the potential
to significantly reduce emissions of hazardous air pollutants from coke oven
production facilities.
o Electric Utilities: This study requires the Administrator to report to Congress by
November 1993 on hazards to public health due to emissions of hazardous air
pollutants from utilities and to develop standards for utilities if he concludes they
are necessary based on the results of the study. In addition, a special assessment
of mercury emissions from utilities including possible control options is due by
November 1994.
o NAS Risk Assessment: EPA is required to make arrangements with the National
Academy of Sciences to conduct a review of the risk assessment methodology
EPA uses to determine carcinogenic risks associated with exposure to hazardous
air pollutants and to discuss possible improvements in the methodology. A report
is due by May 1993.
Based on the results of these studies, the U.S. EPA may promulgate additional emission
standards to protect specific geographic areas such as the Great Lakes or to include sources such
as utility boilers which are not currently subject to any Title III regulations.
2
-------
RESEARCH STRATEGY
The data needed to support this new two-phased regulatory approach is extensive because
of the large number of pollutants and source categories subject to regulation. The U.S. EPA's
Office of Research and Development (ORD) has recognized the challenge of this new regulatory
strategy and has modified its existing research program to provide the critical data and methods
needed. Development of detailed chemical-specific risk assessments emphasized since the late
1970's has been replaced by a broader research program which focuses on providing the data
needed to regulate specific source categories. The new strategy will initially focus on
developing information to support the phase-one MACT standards and special studies. In future
years, emphasis will shift towards developing advanced risk assessment methods and other data
needed to support residual risk determinations. Based on this fundamental change in research
emphasis, the new goals of the Federal HAP research program are to:
o support the technology-based standards by developing source test methods which
will be used to determine compliance with MACT standards and by evaluating
existing and innovative control technologies and pollution prevention approaches
applicable to source categories subject to MACT standards;
o characterize sources of air toxics and determine exposure levels and risks
associated with those air toxic sources where little or no information is available.
Much of this assessment work is currently aimed at supporting the large number
of special studies in Title 111 (Area sources; Great Waters);
o provide data to support residual risk determinations.
Research in the following six major areas has been redirected to support these broad
goals: source test methods, emissions data and emission reduction approaches, ambient
monitoring, exposure assessment, health studies and assessments, and technology transfer.
These research areas were chosen for emphasis based on near-term data needs identified by the
U.S. EPA's Office of Air Quality Planning and Standards (OAQPS) and an independent
evaluation by ORD scientific staff of the research needed to respond to future HAP problems
such as residual risk. Figure 1 provides a summary of how each research area supports the new
Title III provisions.
3
-------
FIGURE 1 - RELATION OF RESEARCH AREAS TO KEY TITLE HI PROVISIONS
RESEARCH AREAS
Source Test Methods
Emissions Data and
Emission Reduction
Approaches
Ambient Monitoring
Exposure Assessment
Health Studies and
Assessments
KEY TITLE HI PROVISIONS
MACT Standards Special Studies Residual Risk
XXX
X
X
X
X
X
X
X
Technology Transfer X X
RESEARCH DESCRIPTIONS BY AREA
SOURCE TEST METHODS:
Currently there are no established methods for measuring emissions of specific HAPs
from many of the source categories for which the U.S. EPA will develop MACT standards over
the next ten years. ORD is responding to this need by developing measurement methods for the
list of 189 air toxics to support compliance with MACT and any future standards. The program
is designed to have stationary source test methods available for a relatively large number of
pollutants in the shortest time and at the least cost through development of screening methods
and generic methods which identify and quantify a number of different pollutants. However, for
those substances that have unique chemical properties, specific test methods will need to be
developed.
EMISSIONS DATA AND EMISSION REDUCTION APPROACHES;
This research area includes efforts to develop and evaluate data on HAP emissions,
control technologies and pollution prevention approaches. The emissions data research is
focused on developing and improving area source emission estimation methods and providing
emission inventories for 3-5 urban areas to support the Area Source Program. Emissions data
is also being generated to support the periodic assessments of deposition to the Great Lakes and
coastal waters. The emission reduction research includes: 1) developing innovative control
processes and pollution prevention approaches for source categories where existing technologies
4
-------
are either not available or not cost-effective; 2) providing guidance on proper engineering
practices to ensure that existing technologies which will be used as the basis for many MACT
standards perform to their expected design efficiencies in the field; and 3) conducting
engineering studies to demonstrate how existing control and prevention approaches which have
only been used in a limited number of applications can be applied to other sources to reduce
HAP emissions. Initial emphasis will be placed on approaches which could be used to comply
with the phase one technology-based standards.
AMBIENT MONITORING:
The goal of this research is to develop and evaluate, both in the laboratory and under
field conditions, methods for sampling and analysis of ambient air pollutants. There are no
satisfactory ambient methods for more than half of the HAPs listed under Title HI. These
methods are needed to identify and quantify HAPs which pose risks in urban air and to major
lakes and coastal waters and to monitor the progress of the overall air toxics regulatory program.
In addition, the ambient data will be used in the future to support residual risk determinations
by providing information on how the phase-one MACT standards have impacted ambient air
toxic concentrations. Initially efforts are focused on monitoring a wide variety of air toxics in
5-8 urban areas. This monitoring data directly supports the Area Source Program which
requires monitoring in a representative number of urban locations to characterize risks from area
sources.
EXPOSURE ASSESSMENT:
The ORD program is developing data on the atmospheric lifetime and fate of air toxic
chemicals. Such information will also be generated for selected non-toxic substances that react
to form potentially toxic products. The Agency requires data on air toxics to estimate human
and ecological exposures to those compounds and to help devise strategies to eliminate or limit
exposures. Research is also underway to identify and quantify the contributions of specific
sources of air toxics to ambient concentrations. Source signature data will be gathered to
reconcile emissions and ambient concentration data. The exposure assessment work directly
supports the Area Source Program which requires consideration of atmospheric transformation
and other factors which can elevate public health risks from such pollutants. In addition, the
data on exposure will be critical to making residual risk decisions.
HEALTH STUDIES/ASSESSMENTS:
In the health effects area, ORD is evaluating the nature and magnitude of non-cancer
health effects associated with exposure to toxic air pollutants including developing methods to
quantify developmental and reproductive toxicity of chemicals emitted to the air by point and
area sources. Other health research is also planned to assess the neurotoxicity of the 189 HAPs
in animals and humans; to identify which air toxics are liver toxicants; and to improve cancer
risk extrapolation for air toxics through biologically based dose-response modeling. The
assessments portion of this research area will provide non-cancer and cancer health risk
5
-------
assessments on air toxics in support of regulatory activities. The major activities are to develop
chronic Reference Concentrations known as RfCs (defined as an air concentration for a chemical
which is anticipated to pose little or no public health risks) for Title III compounds and to
develop acute non-cancer assessments of the 189 listed air toxics. The health research will
support many of the special studies required under Title III including the area source program
which requires EPA to identify the 30 (or more) air toxics that pose the greatest threat to public
health and will provide the foundation for future residual risk assessments after MACT has been
applied to point sources.
TECHNOLOGY TRANSFER
The technology transfer program will provide technical assistance on a variety of HAP
issues ranging from control technology performance to health risk assessments. The information
will be provided to users through three technical centers currently in full operation. The type
of assistance each center provides is described below.
o The Control Technology Center (CTC) provides technical assistance to state and
local air pollution control agencies on matters relating to air pollution control
technology. A hotline is used to provide quick responses to telephone requests
for assistance. In addition, more in-depth studies are initiated to respond to
specific state or local requests for assistance which can not be answered without
initiating a formal study. Results from these longer-term assistance projects are
issued as technical guidance through publication of technical reports, development
of personal computer software, and workshops on control technology matters.
o Air Risk Information Support Center (Air RISC) - Provides scientific assessment
assistance to states, Regions, and local agencies on air toxics health risk issues.
The types of guidance provided include: rapid response to health risk questions;
2) training in use of risk assessment guidelines; 3) development of cancer and
non-cancer assessments; and review/consultation on state regulatory actions.
o Emission Measurement Technical Information Center (EMTIC) - This center is
designed to promote consistent and accurate application of emission test methods
for development and enforcement of national, state, and local emission prevention
and air pollution control programs. The center has gathered information on
testing needs, held workshops, and sent test methods and quality assurance
information to regional, state, and local agencies.
CONCLUSION
Title HI of the 1990 CAAA has substantially changed the process used to regulate HAPs
and is expected to substantially decrease emissions over the next ten years as MACT standards
are promulgated for hundreds of source categories and subcategories. However, the
effectiveness of the program will depend heavily on the quality of scientific data used to develop
6
-------
and enforce each emission standard issued. The U.S. EPA's Office of Research and
Development has redesigned its air toxics research program to ensure this scientific data is
generated in time to meet mandated regulatory deadlines. The combination of near-term
research to support MACT standards and special studies with longer-term research to support
future residual risk determinations will ensure the challenging new regulatory approach is
implemented with the best scientific information available.
7
-------
Ill nil II III [111 MflC
PB96-150826 Information is our business.
A TEMPORAL LOGIC FOR MULTI-LEVEL REASONING
ABOUT HARDWARE
DEPARTMENT OF COMPUTER SCIENCE
STANFORD, CA
DEC 82
U.S. DEPARTMENT OF COMMERCE
National Technical Information Service
-------
December 1982
Report No. STAN-CS-82-952
A Temporal Logic for Multi-Level
Reasoning about Hardware
%
Ben Moszkowski
Department of Computer Science
Stanford University
Stanford, CA 94305
^IWlZtO
REPRODUCED BY: NTS
U.S. Department of Commerce
National Technical Information Service
Springfield, Virginia 22161
-------
BIBLIOGRAPHIC INFORMATION
PB96-150826
Report Nos: STAN-CS-82-952
Title: Temporal Logic for Multi-Level Reasoning about Hardware.
Date: Dec 82
Authors: B. Moszkowski.
Performing Organization: Stanford Univ., CA. Dept. of Computer Science.
Sponsoring Organization: *National Science Foundation, Washington, DC.*Defense
Advanced Research Projects Agency, Arlington, VA.*Air Force Office of Scientific
Research, Boiling AFB, DC.
Contract Nos: DARPA-N00039-82^C-0250, NSF-MCS79-09495, NSF-MCS81-11586, AFOSR-81-0014
Supplemental Notes: Presented at the IFIP International Conference on Computer
Hardware Description Languages and Their Applications (6th), Pittsburgh, PA., May
1983.
NTIS Field/Group Codes: 62E (Information Theory), 62A (Computer Hardware), 62B
(Computer Software)
Price: PC A03/MF A01
Availability: Available from the National Technical Information Service. Springfield,
VA. 22161
Number of Pages: 26p
Keywords: *Mathematical logic. *Logic design. Learning machines. Artificial
intel hgence. Computer systems programs. Computer systems hardware, ^Temporal logic,
*Multi-level reasoning.
Abstract: The paper describes a logical notation for reasoning about digital circuits.
I he formalism provides a rigorous and natural basis for device specification as well
as for proving properties such as correctness of implementation. Conceptual levels of
circuit operation ranging from detailed quantitative timing and signal propagation up
to functional behavior are integrated in a unified way. A temporal predicate calculus
serves as the formal core of the notation, resulting in a versatile tool that has more
descriptive power than any conventional hardware specification language. The logic has
been applied to specifying and proving numerous properties of circuits ranging from
delay elements up to the Am2901 ALU bit slice. Presentations of a delay model and a.
multiplication circuit illustrate various features of the notation.
-------
A Temporal Logic for Multi-Level Reasoning about Hardware
Ben Moszkowski
Department of Computer Science
Stanford University
Stanford, California 94305
Abstract
This paper describes a logical notation for reasoning about digital circuits. The
formalism provides a rigorous and natural basis for device specification as well as
for proving properties such as correctness of implementation. Conceptual levels of
circuit operation ranging from detailed quantitative timing and signal propagation
up to functional behavior are integrated in a unified way.
A temporal predicate calculus serves as the formal core of the notation, result-
ing in a versatile tool that has more descriptive power than any conventional
hardware specification language. The logic has been applied to specifying and prov-
ing numerous properties of circuits ranging from delay elements up to the Am2901
ALU bit slice. Presentations of a delay model and a multiplication circuit illustrate
various features of the notation.
The work presented here was supported in part by the National Science Foundation
under a Graduate Fellowship, Gravis MCS79-09Jt95 and MCS81-11586, by DARPA
under Contract N00039-82-C-0250, and by the United States Air Force Office of
Scientific Research under Grant AFOSR-81-0014•
This paper is part of the author's Ph.D. dissertation under the supervision of Professor
Zohar Manna and will appear in the IFIP Sixth International Conference on Computer
Hardware Description Languages and Their Applications, Pittsburgh, Pennsylvania,
May, 1983.
1
-------
§1 Introduction
Computer systems continue to grow in complexity and the distinctions between
hardware and software keep on blurring. Out of this has come an increasing
awareness of the need for behavioral models suited for specifying and reasoning
about both digital devices and programs. Contemporary hardware description
languages (for example [1,15,19]) are not sufficient because of various conceptual
limitations:
• Most such tools are intended much more for simulation than for math-
ematically sound reasoning about digital systems. Many compromises
are made so that the descriptions can be executed.
• Difficulties arise in developing circuit specifications that out of necessity
must refer to different levels of behavioral abstraction.
• What formal tools there are for such languages cannot in general deal
with the inherent parallelism and nondeterminism of circuits.
The formalism presented in this paper overcomes these problems and unifies
in a single notation digital circuit behavior that is generally described by means of
the following techniques:
• Register transfer operations
• Flowgraphs and transition tables
• Tables of functions
• Timing diagrams
• Schematics and block diagrams
The notation is based on discrete time intervals and combines aspects of stan-
dard temporal logics (12,17] with features of dynamic logic [7]. Halpern et al.
[6] shows that useful subsets pf the logic are decidable and of relatively reason-
able computational complexity. This indicates that partial automation of reason-
ing may be practical. The formalism's applicability is by no means limited to
the goals of computer-assisted verification and synthesis of circuits. This type of
notation, with appropriate "syntactic sugar," could provide a fundamental and
rigorous basis for communicating, reasoning or teaching about digital concepts and
devices. Simulation-based languages could for example use such a logic as a vehicle
for describing the intended semantics of delays and other features. Thus, semi-
automated correctness checking is really only one part of a much bigger picture.
2
-------
Before outlining the formalism, the paper discusses related work. The temporal
logic is then informally introduced by way of sample properties. Following this, the
formalism serves as a basis for specifying and reasoning about various aspects of a
simple delay element as well as of a hardware multiplication circuit. Quantitative
timing as well as algorithm development are discussed.
§2 Related Work
Gordon's work [4] on register-transfer systems uses a denotational semantics to
provide a concise means for reasoning about clocking, feedback, instruction-set im-
plementation and bus communication. No quantitative timing properties are con-
sidered and the notation has some difficulties in describing operations occurring over
multiple cycles. Wagner [20] presents a semi-automated proof development system
for reasoning about signal transitions and register transfer behavior. Unfortunately
the notation suffers from a lack of formality that is difficult to remedy. Malachi and
Owicki [11] utilize a temporal logic to model self-timed digital systems by giving
a set of axioms. No indication is included on how to generalize the work to the
entire domain of digital circuits. The work of Bochmann [2] describes and verifies
properties of an arbiter, a device for regulating access to shared resources. The
presentation, by means of a temporal logic, reveals some tricky aspects in reasoning
about such components although the concepts used are not as rigorously developed
as they may appear to be and do not easily generalize. As in the previous works,
no quantitative timing issues are examined.
Leinwand and Lamdan [9] use a type of Boolean algebra to model signal tran-
sitions. Applications include systems with feedback and critical timing constraints.
The use of the notation for non-trivial examples is very unintuitive. Patterson [16]
explores the verification of firmware. This work views the problem from the sequen-
tial programming standpoint without describing the underlying digital circuitry and
related issues of concurrency and timing. There is also work by Meinen [13] on
register transfer behavior and McWilliams [10] on worst-case time constraints.
Eveking [3] uses predicate calculus with an explicit time variable to explore
verification in the Conlan language. Although such an approach can in principle
describe circuits, the proliferation of variables representing explicit time points
becomes a major hindrance from a practical as well as theoretical standpoint. Many
high-level temporal concepts become easily obscured amid all the notation.
A number of people have used temporal logics to describe computer communica-
tion protocols [5,8,18]. However, the precise connections between protocols and
3
-------
the underlying hardware and software are still rather unclear as are the relative
advantages of the different techniques employed.
§3 Notational Preliminaries
Before the logic is introduced, it is necessary to say a little about the kinds of
mathematical entities used here for modelling digital signals.
Data Values
Values are limited to natural numbers, X (read "bottom"), and finite-length
vectors constructed using these elements. Both 0 and 1 as well as _L serve as bits,
with 0 standing for low voltage, 1 for high voltage and _L representing voltages that
are out of range. Finite-length vectors can be formed containing natural numbers
and X. The following are sample values:
0, 3, X, (0), (1,2), (), (J-,1,1)
Bit Operations
Four basic operations defined on bits are complement (©), and (©), or (©) and
exclusive-or (®). The symbols ©, © and © are used instead of -1, a and v in order
to distinguish notationally between bit expressions and formulas in the underlying
predicate calculus. Here are corresponding truth tables extended to include X:
©
©
0
1
X
©
0
1
X
©
0
1
X
0
1
0
0
0
0
0
0
1
X
0
0
1
X
1
0
1
0
1
X
1
1
1
1
1
1
0
X
X
X
X
0
X
X
X
X
1
X
X
X
X
X
§4 Informal Overview of Temporal Operators
The temporal logic provides a basis for describing periods of time such as
in timing diagrams. Concepts such as signal response and oscillation are readily
-------
expressible. Examples serve to introduce the various operators used later in this
paper. This presentation has been kept rather informal although the entire logic is
explored in detail in Halpern et al. [6] and Moszkowski [14].
Time is modeled as being discrete and finite. The following figure is a typical
timing diagram:
X
1 •
0 10 20 30 40 50 units
This represents the behavior of the signals X, Y and Z over a period of 50 units
of time. The signal X goes up and down twice, while Y is stable with the value 1.
Initially Z equals 0 for over 20 units, after which it equals _L. Notice that all times
are relative. This approach is used because the properties to be examined depend
solely on distances between points, independent of any absolute times.
The group of signals can be modeled as a finite temporal interval a mapping
variables and times to values. The behavior of intervals is concisely expressible by
temporal formulas presented below. Given such a formula p, the construct a \= p
means p is true for the interval a. The notation t= p signifies that the formula p
is true of all intervals. Please keep in mind that all operators discussed can be
expressed in terms of a small collection of fundamental notions. The properties
shown are deducible from a basic set of logical rules.
4.1 Initial and Terminal Equality
The formula beg(X = Y) is true for an interval a if within a the two signals
X and Y have equal starting values. Similarly, the construct jln{X — Y) is true
for an interval a if X and Y end up equal in a.
Examples for a given interval o:
Concept Formula
X and Y start equal and end complements o t= [beg(X = Y) a fin(X = 07)]
X ends equal to 1 and Y ends equal to 0 a h/m(X = 1 a Y = 0)
5
-------
Properties that are true for all intervals:
*= - fin(X = Y) = = Y))
The signals X and Y do not end equal if and only if they end up not equal.
t= fin((X 0Y) = 1) 3 fin(X = 1 a Y = 1)
If the bit-and of X and Y ends up equaling 1, both X and Y end up equal to 1.
4.2 Temporal Equality
Two signals X and Y are temporally equal in an interval a if they have the
same values at all times. This is written X « Y and differs from the constructs for
initial and terminal equality, which only examine signals' values at the extremes of
the interval.
Examples:
Concept
The signal X is 0 throughout the interval
The bit-and of X and Y everywhere equals 0
X agrees everywhere with the complement of Y
Formula
ctnJwO
<7N(x©y)^o
BY
Properties:
N X as Y = f(X) « f(Y)
If two signals are temporally equal, then any function applied to one of them
temporally equals the same function applied to the other.
l= X ^ 0 =5 X®Y «0
If X temporally equals 0, then the bit-and of it with another signal also equals 0
everywhere.
t= (X,r> ^(0,1}e[X«0aF«1]
The pair (X, Y) temporally equals (0,1} exactly if the signal X temporally equals
0 and Y temporally equals 1.
6
-------
4.3 Temporal Stability
A signal X is stable if it has a constant, defined value. The notation used is
stbX. In the case of a bit signal, this means that the signal is always 0 or always
1, that is
stbX = [I«OvI«l]
Example: (this and further examples will omit the symbols "a n")
Concept Formula
The complement of X is stable stb © X
Properties:
N [I«l] = [stb X a beg(X = 1)]
The signal X always equals 1 if and only if X is stable and initially equals 1.
N= stb X = stb 0 X
A bit signal is stable if and only if its complement is.
[stbX a stbYJ o stb(X © Y)
If two bit signals are stable, then so is their bit-or. The converse is not always true,
N stb(X, Y) = [stbX a stbY)
A pair is stable exactly if the two individual signals are.
4.4 Temporal Length
Quantitative timing properties are handled by a special object len whose value
for any interval a equals the length of a.
Examples:
Concept Formula
The interval is at least m units in length len > m
The signal X is stable and cr measures at least m units stb X a len > m
The predicate empty is true exactly if the interval has length 0. The predicate
skip is true if the interval has length exactly 1. Since time is discrete, this is the
minimum nonzero width.
-------
4.5 Examining Subintervals
For a formula p and interval a, the construct Bp is true if p is true in all
subintervals of time contained within a including a itself. Note that the "a" in 0
simply stands for "all" and is not a variable. The formula <$> p is true if the formula
p itself is true in at least one subinterval of a.
Examples:
Concept Formula
In some subinterval of length > m + n, X is stable <$>([/en > m + n] a stb X)
In all subintervals < m units, X is stable E([/en < m] 3 stb X)
Properties:
N Bp 3 p
If a formula p is true in all subintervals then it is true in the primary interval.
N <& p = -1 0 ~>p
A formula is true in some subinterval if and only if the formula is not everywhere
false.
N B(p A q) = [0p A B?]
The logical-and of two formulas p and q is true in every subinterval if and only if
both formulas are true everywhere.
>= p = <$><§> p
A formula is somewhere true exactly if there is some subinterval in which the formula
is somewhere true.
[Bp a Of] => <8>(p a q)
If p is true in all subintervals and q is true in some subinterval then both are
simultaneously true in at least one.
n [X^Y] = B(X = Y)
Two signals are temporally equal in an interval exactly if they are equal in every
subinterval.
f= stbX 3 B stbX
If X is stable in the overall interval, X is also stable in every subinterval.
8 •
-------
4.6 Initial Subintervals
The operators 0] and are similar to 0 and <8> but only look at initial
subintervals starting at time 0.
Example:
Concept " Formula
X is initially stable for at least the first m units <3>(stbX a len > m)
4.7 Temporal Dependence
It is useful to specify that a signal X remains stable as long as another signal
Y does. X is said to depend on Y, written X depY. This can be expressed using
the temporal formula
XdepY = m(stbY 3 stbX)
Examples:
Concept Formula
X and Y remain stable while Z does {X, Y) dep Z
X remains stable as long as the pair (Y, Z) does X dep (Y, Z)
Properties:
(= [XdepY a stbY] ^ stbX
If X depends on Y and Y is stable, then so is X.
* (X dep Y a Y dep Z] 3 X dep Z
Dependence is transitive.
1= beg{X = 0) 3 {X®Y)depX
If X initially equals 0, then the bit-and of X and Y depends on X.
1= [X dep Z a Y dep Z] = (X, Y) dep Z
The variables X and Y depend on Z exactly if the pair (X, Y) does.
9
-------
4.8 Adjacent Subintervals
Given a time interval, the formula p; q is true if there is at least one way to
divide the interval into two adjacent subintervals a and a' such that the formula p
is true in the first one, a, and the formula q is true in the second, a'. In particular,
a rising signal can be described by the predicate |X:
tX = [(X « 0); skip; (X « 1)]
This says that X is 0 for a while and then jumps to 1. The gap of quantum length
represented by the test skip is necessary here since a signal cannot be 0 and 1 at
exactly the same instant. Falling signals are analogously described by the construct
JX:
|X = [(X « 1); skip; (X » 0)]
Examples:
Concept
X is stable and Y goes up
The bit-or of X and Y falls
In every subinterval where X rises, Y falls
X goes up and then back down
Properties:
n (TX a fY) => [!(X©y) a T(X©F)]
If two bit signals rise, so do their bit-and and bit-or.
n |X = T ©X
A bit signal falls exactly if its complement rises.
t= [TX a beg(Y = 0) a {Y dep X)] 3 T(X©Y)
If X rises and in addition Y initially equals 0 and depends on X, then the bit-or of
X and Y also rises.
These operators can be extended to include quantitative information specifying
minimum periods of stability before and after the transitions. For example, timing
details can be added to the operator T:
Tm'nX = [(X 0 a len > in); skip; (X « 1 a len > n)]
Formula
stbX a ]Y
1{X©Y)
~(TX 3 IY)
TX; IX
10
-------
A negative pulse with quantitative information can be described as shown
below:
[(X ps 1 a /en > I); skip]
(X ~0 a len > m); skip; (X 1 a len > n)]
4.9 Temporal Assignment .
The formula X —~ Y is true for an interval if X's initial value equals Y's final
value.
Example:
Concept Formula
Z ends up with the complement of Y's initial value 07 —*¦ Z
Properties:
N stbX 3 (X->X)
A stable signal's initial and final values agree.
N [(X Y); (Y Z)\ 3 (X — Z)
If Y gets X's value and then Z gets Y's, the net result is that Z gets X's initial
value.
n (0X -> Y) = (X^0Y)
The bit signal Y gets the complement of X's value exactly if Y's complement gets
the value of X itself.
h [(©Z- Z); (0Z-> Z)] 3 (Z -> Z)
If a signal is twice complemented, it ends up with its original value.
4.10 Repetition
An interval can be broken up into an arbitrary number of successive subin-
tervals, each satisfying some formula p. The construct pn has the same meaning
11
-------
as
p;
s.
n times
For the case of n = 0, an interval a satisfies the operator exactly if ct's length is 0.
Examples:
Concept Formula
The signal Y twice goes up and down (|Y; jY)2
Z is complemented n times (© Z —~ Z)n
Properties:
¥ (0J —~ X)n 3 [J©(nmod 2)- X]
After a series of n complements, X ends up with the initial value of the exclusive-or
of X and (n mod 2). For instance, if n is even, X ends up unchanged.
1= (pm)n = pmn
If a formula p is repeated m times within a further repetition of n cycles, the net
result is the same as iterating p a total of mn times.
§5 Simple Delay Element
Delay is of fundamental importance in digital systems. One of the simplest
types of delay elements has the following structure:
In-
Out
n-unit delay
Here In is the input bit signal and Out is the associated output. The variable
n is a fixed natural number indicating the time delay between a value appearing
on the input and later on the output. The following statement uses intervals to
characterize this behavior:
In every subinterval of length exactly n units, the initial input value
agrees with the final output one.
12
-------
The next predicate Delay captures the required interaction:
Delay(In, Out, n) =def 0[(/en = n) (In —*¦ Out)]
Properties:
• A delay element is also a delay element in every subinterval:
Delay(In, Out, n) 3 IB Delay (In, Out, n)
• Zero delay is the same as temporal equality:
t= Delay (In, Out, 0) = (In ^ Out)
• Two connected delays result in a combined delay:
N [Delay(Inl, Outl, nl) a Delay(In2, Out2, n2) a Outl 7n2]
3 Delay(Inl, Out2, nl + n2)
Note that the total delay nl + rx2 is the sum of the delays nl and n2.
An alternative delay model can be given containing an internal state of n + 1
bits that are shifted as in a queue. The two distinct models are formally equivalent
as can be expressed and demonstrated with the temporal logic.
The object len is used in the definition of Delay to measure time. Actually,
other metrics seem possible. For example, some variable might represent the number
of clock cycles or machine instructions executed in each interval. The properties of
delay remain basically the same.
§6 Multiplication Circuit
The hardware multiplier considered here is motivated by one discussed in
Wagner's work on hardware verification [20]. The desired device behavior is first
described followed by a look at implementation techniques. The multiplier has the
following general structure;
13
-------
Inl\0 ton — 1]=>
In2\ 0 ton — 1] =4
Ck-*-
Ld—
n, count",
cl, c2, c3
The circuit accepts two numbers and after a given number of clock cycles yields
the product. The numbers are represented as unsigned n-bit vectors Inl and In2
while the output Out is a 2n-bii one. In addition to the vector inputs and output,
there are two input bits Ck and Ld which control operation. The signal Ck serves
as the clock input and Ld initiates the loading of the vectors to be multiplied. The
field count tells how many clock cycles are required. The values el, c2 and c3 are
timing coefficients used in the behavioral description.
6.1 Additional Notation
Because the multiplier deals with numbers and their representation as bit
vectors, it is convenient to introduce some extra notation before giving the device's
formal description:
• Subscripts on a vector V = (Vo,..., vn) normally range from 0 on the left to n on
the right. The construct V[i] follows this style. However, to simplify reasoning
about the correspondence between a bit vector and its numerical equivalent, a
slightly different convention is adapted. The alternative notation V{i] indexes V
from the right with the right-most element having subscript 0. For example:
{1, 0, J-){0} = -L, (1,0,-L){1} = 0, (1, 0, _L){2} = 1
For a vector V and i > j, the expression V{z to j) forms a new vector out of the
elements indexed from i down to j. If i < j, the empty vector is returned. For
example,
(0,9, _L, 2){3 to 1} = (0, 9, ±), (0, l){0to0} = (1), (_L, 1,0,1){1 to 2} = ()
• The predicate def X is true for a scalar value X if X does not equal _L. In this
case, X is defined. A vector is defined exactly if all its components are. For
=> Out[0 to 2n — 1]
14
-------
example, the following values are defined;
0, 3, (1,0), ()
The values given below are not defined:
±, (±,±), (J-,0)
• The function rival converts a bit vector to its unsigned numeric value. For
example,
nval{{ 0,1,1)) = 3, nval{{ 1,1,0,0)) = 12
If any element of the vector is undefined, rival yields _L as the result. Thus,
nval(( 1, J_, 0, 0,1)) = ±
6.2 Overview of Description Techniques
In what follows, the predicate Multiplier[M) specifies that desired behavior of a
multiplication circuit. The device's various inputs, outputs and timing coefficients
are represented as fields of the single parameter M. An iterative, timing-independent
multiplication algorithm is then presented which computes a product by a series
of successive additions. Later, the predicate Implementation(H) characterizes a
device which computes sums and in fact has the algorithm's steps embedded within
it. A logical implication is then given, showing how Implementation(H) realizes
Multiplier (M).
6.3 Formal Specification of Multiplication Circuit
The predicate Multiplier formally characterizes the circuit's desired structure
and behavior. The single parameter M is a tuple representing the multiplier. For
example, the expression M.Ck equals the clock input. The predicate's definition
makes reference to other predicates given later:
Multiplier(M) =def
MultStructure(M)
a ~ Calculate(M)
The predicate MultStructure presents M's fields. The predicate Calculate gives the
control sequencing required to perform a multiplication. The operator 0 indicates
that Calculate must be true in all sub'intervals.
15
-------
Definition of Mult Structure'.
The definition below of MultStructure contains information on the physical
structure of the multiplier. Variables starting in upper case represent signals while
lower-case ones are constant. Labels such as "Inputs:" are comments included to
classify the various circuit fields. For example, M.Inl is an input bit vector.
MultStructure(M) =def
Inputs:
(Ck, Ld): Bit,
Inl\n — 1 to 0}: Bit,
In2\n — 1 to 0}: Bit
Outputs:
Out{2n — 1 to 0}: Bit
Parameters:
n: nat,
count: nat,
cl, c2, c3: time
For brevity, the prefix "M" is omitted when a field is referenced below.
Definition of Calculate:
If the inputs behave as specified by the predicate Control, the output Out ends
up with the product of the initial values of Inl and In2. Recall that the function
nvat converts a bit sequence to the corresponding numerical value.
Calculate(M) =def
Control(M) 3
[nval(Inl) • nval(In2)] —~ nval(Out)
Definition of Control'.
The predicate Control describes the required sequencing of the inputs so that
a multiplication takes place. The computation first loads the circuit and then keeps
the load line inactive while the clock is cycled.
Control(M) =aef Load(M); ([Ld « 0] a Cycling(M))
16
-------
Definition of Load",
Loading is done as indicated by the predicate Load. The clock is cycled as
given by the predicate Single Cycle. The control signal Ld starts with the value 1
and together with the other inputs Inl and In2 remains initially stable as long as
the clock input Ck does,
Load(M) —def
SingleCycle(M) a beg{Ld = 1) a {Ld, Inl,In2) dep Ck
Definition of SingleCycle:
An individual clock cycle consists of a negative pulse:
Single Cycle(M) =def It cl,c2,c3Ck
The clock signal falls from 1 to 0 and then rises back to 1. The three times given
indicate the minimum widths of the levels during which the clock is stable.
Definition of Cycling:
The overall cycling of the clock is as follows:
Cycling(M) —def (Single Cycle(M))count
A total of count individual cycles must be performed one after the other, where
each is a negative pulse satisfying the predicate SingleCycle.
Variants of the Specification
The predicate Multiplier does not represent the only way to describe the mul-
tiplier circuit. Alternative approaches based on an internal state can be shown to
be formally equivalent to the one given here. A useful extension to this description
specifies that once the output is computed, it remains stable as long as the control
inputs do. If desired, additional quantitative timing details can readily be included.
6.4 Development of Multiplication Algorithm
The specification predicate Multiplier intentionally makes no reference to any
particular technique for multiplying. Since the process of multiplication does not
17
-------
generally depend on any specific circuit timing, it is natural to separate algorithmic
issues from other.implementation details. The temporal logic now serves as a basis
for deriving a suitable circuit-independent algorithm for determining the product
and in the next section as a means for describing hardware that realizes this method.
The synthesis process can be viewed as a proof in reverse, starting with the goal
and ending with the necessary assumptions to achieve it.
The aim here is to obtain an algorithm describing some way for doing the
multiplication. The variables n, Inl, In 2 and Out are represented as fields of a
variable A. The predicate Goal below specifies the desired result:
:def
Goal(A)
beg(def Inl a def In2) =5
[nval[Inl) ¦ nval(In2)]
rival (Out)
If the data inputs Inl and In2 are initially defined, the output Out should end up
with their product. The presentation given here reduces the problem of multiplying
the two n-bit vectors to that of using repeated additions to determine successively
larger partial products. The algorithm consists of initialization followed by n
successive iterations. After i iterations of the loop, for i < n, the initial product of
Inl and the least significant i bits of In2, that is,
nval(Inl) • nval(In2\i — 1 to0})
is computed and available in the upper n + i bits of Out. Neither Inl nor In2 is
guaranteed to remain stable once initialization is complete. However, their initial
values must be used throughout the calculation. The lower n — i bits of Out hold
the unexamined bits of In2 (i.e., In2{n — 1 to?}). In addition, an extra n-bit variable
Temp is introduced in order to remember the original value of Inl. The following
figure informally depicts the situation after i steps:
partial product
rest of In2
Out: nval(Inl) - nval(In2[i — 1 to0})
In2\n — 1 to i
2n —l
n — % n —* —1
0
n + t bits
n — i bits
value of Inl
Temp:
Inl
n — 1
n bits
After n steps, Out equals the desired 2n-bit multiplication result.
18
-------
The predicate Assert below precisely specifies this behavior over i iterations
for i < n. Note that both inputs Inl and In2 must be initially defined for the
operations to properly take place.
Assert(A, i) =der
beg(def Inl a def In2) 3
[nval(Inl) • nval(In2\i — 1 toO})] —~ nval(Out{2n — 1 ton — t})
a In2\n — 1 to t} —> Out\n — i — 1 to 0}
a Inl —~ Temp
After n steps, the product must be computed. For i = n, Assert indeed
observes this requirement:
Assert(A, n) Goal [A) (*)
Expressed in the logic, the algorithm takes the following form:
Init(A); (Step(A))n
In the next two subsections, the predicates Init and Step are given in detail. Both
Init and Step are derived so as to maintain Assert after looping i times for any
i < n:
[i < n a Init(A.); (Step(A))1] Assert(A, i) (**)
The properties (*) and (**) together ensure that n iterations of the loop calculate
the product:
Init [A); (Step(A))n 3 Goal {A)
Deriving the Predicate Init
The initialization requirement can be obtained by making sure Init satisfies
Assert for i = 0:
Init(A) p Assert (A, 0)
19
-------
Simplification of Assert yields the constraint
Init(A) 3
beg(def Inl a def In2) 3
0 ~+ nval(Out{2n — 1 ton})
a In2 —+ Out{n — 1 to 0}
a Inl —*¦ Temp
This can be achieved by the definition
Init{A) =def
beg(def Inl a def In2) 3
(0,..., 0) —» Out{2n — 1 to n}
a In2 —> Out{n — 1 to 0}
a Inl —*¦ Temp
Deriving the Predicate Step
The iteration step should be constructed so that after i iterations for any i < n,
Step can inductively widen the scope of the assertion to i + 1 increments:
[z < n a Assert(A, i); Step(A)] Assert (A, i + 1)
Each step achieves this by selectively adding Temp's n bits to Out, depending on
Out's least bit, Only the top n bits of Out are actual inputs for the sum.
The top n + 1 bits store the result. The remaining n — 1 bits of Out are simply
shifted right. For Temp the requirement reduces to the formula
Step(A) 3
beg(def Temp) 3 (Temp —~ Temp)
This guarantees that Temp continues to remember the initial value of Inl.
The constraint for Out is
Step(A) 3
beg(def Out a def Temp) 3
[¦nval(Out{2n — 1 ton}) + O«£{0} * nva l(Temp)]
—~ nval{Out{2n — 1 ton — 1})
A Oul{n — 1 to 1} —> Out{n — 2 to 0}
20
-------
Thus the overall incremental step can be realized by the definition
Step^A.^ —def
beg(def Out a def Temp)
[nval(Out{2n — 1 ton}) + Out{0} • nval(Temp)]
—*¦ nval(Out{2n — 1 ton — 1})
a Out{n — 1 to 1} —~ Out{n — 2 to 0}
a Temp —*¦ Temp
6.5 Description of Implementation
The circuit specified below performs the iterative algorithm just given. The
definition includes relevant timing information and is broken down into parts describ-
ing the implementation's physical structure and behavior. The primary predicate
Implementation overviews operation. The device's fields are shown by ImpStructure.
The predicate LoadPhase specifies device operation for initially loading the inputs.
Once this is achieved, the predicate MultPhase indicates how to perform the in-
dividual multiplication steps.
Implementation(H) =def
ImpS tructure (H)
a (3(LoadPhase(H) a MultPhase(H))
Definition of ImpStructure'.
The structure of the implementation differs from that of the original specification
by the addition of the internal state Temp for maintaining the value of Inl and by
the omission of a count field giving the required number of clock cycles for comput-
ing a product.
21
-------
ImpStructure{H) =def
Inputs:
(Ck, Ld): Bit,
Inl{n — 1 to 0}: Bit,
In2\n — 1 to 0}: Bit
Outputs:
Out{2n — 1 to 0}: Bit
Internal:
Temp{n — 1 to 0}: Bit
Parameters:
n: nat,
cl, c2, c3: time
Definition of LoadPhase:
The body of LoadPhase specifies how to load the inputs as described in the
algorithm:
LoadPhase(H) ^def
Load(H) 3 Inii(H)
The predicate Load gives the required loading sequence for the circuit inputs. The
predicate Init refers to algorithm's initialization predicate. The definition of Load
is identical to that of its namesake in Multiplier:
Load{H) =def
SingleCycle{H) a beg{Ld = 1) a {Ld,Inl,In2) dep Ck
Individual clock cycles are also defined as in Multiplier:
SingleCycle{H) =def |tcI,c2,c3^
Definition of MultPha.se:
When the load signal is inactive at 0, the circuit can be clocked to perform a
single iteration. The algorithm's predicate Step takes place over two clock cycles.
MultPhase(H) =def
[Ld « 0 a (SingleCycle{H)f ] 3 Step{H)
22
-------
Implementation Theorem
The correspondence between the implementation Implementation and the original
multiplier device specification Multiplier is now given by the theorem
M.field = H.field; for the fields cJ, c2 and c3
The value of M. count corresponds to the 2n clock cycles needed for doing the
iterative computation.
The behavioral description Implementation can itself be realized by some even
lower-level specification containing further details about the timing and using a still
more concrete algorithm. For example, the iterative steps are decomposible into
separate adds and shifts. If desired, the development ultimately examines such
things as propagation through gates.
§7 Conclusion and Future Plans
Compared with conventional hardware description languages, the approach
used here permits direct reasoning about signal, device and algorithm behavior
at various levels of detail. In addition, the concepts relating specifications with
implementations and hardware with register-transfer operations can be rigorously
expressed within a single mathematical framework. A disadvantage arises from the
inability to directly execute arbitrary descriptions.
Standard temporal logics and other such notations have not been designed to
concisely handle the kinds of quantitative timing properties and signal transitions
found in the examples considered. The intervals of time provide a unifying means
for presenting various features.
The material presented only scratches the formalism's surface. Halpern et al.
[6] and Moszkowski [14] cover many details of the logic, describing and comparing
devices ranging from delay elements up to the Am2901 ALU bit slice developed by
Advanced Micro Devices, Inc. Future work will examine microprocessors, buses and
protocols, DMA, firmware and instruction sets, as well as the combined semantics
of hardware and software.
N Implementation(H) Multiplier(M)
where the mapping from Ws fields to M's is
M. field
M.n
M. count
II.field, for the fields Inl, In2 and Out
H.n
2 H.n
23
-------
§8 Acknowledgements
Many thanks go to the following people for discussions and suggestions con-
cerning the notation's readability (or lack thereof): Patrick Barkhordarian, Russell
Greiner, Kevin Karplus, Amy Lansky, Yoni Malachi, Fumihiro Maruyama, Gudrun
Polak, Alex Strong, Carolyn Talcott and Pierre Wolper. Professors John McCarthy
and Zohar Manna gave much support and guidance as this research developed.
Joseph Halpern provided valuable insights with regard to the logic's theoretical
complexity. If it had not been for my friends at Siemens AG and the Polish Academy
of Sciences, it is unlikely I would have undertaken this investigation. Late-night
trans-Atlantic discussions with Mike Gordon helped provide a sense of intrigue.
High est-quality chocolate and enthusiasm were always available from the Trischlers.
References
1. M. R. Barbacci. Instruction Set Processor Specifications (ISPS): The notation
and its applications. IEEE Transactions on Computers C-80, 1 (January
1981), pages 24-40.
2. G. V. Bochmann. Hardware specification with temporal logic: An example.
IEEE Transactions on Computers C-31, 3 (March 1982), pages 223-231.
3. H. Eveking. The application of Conlan assertions to the correct description of
hardware. Proceedings of the IFIP TC-10 Fifth International Conference on
Computer Hardware Description Languages and their Applications, Kaisers-
lautern, West Germany, September, 1981, pages 37-50.
4. M. Gordon. Register transfer systems and their behavior. Proceedings of
the IF IP TC-10 Fifth International Conference on Computer Hardware De-
scription Languages and their Applications, Kaiserslautern, West Germany,
September, 1981, pages 23-36.
5. B. T. Hailpern and S. Owicki. Verifying network protocols using temporal
logic. Tech. Rept. 192, Computer Systems Laboratory, Stanford University,
June, 1980.
6. J. Halpern, Z. Manna, and B. Moszkowski. A hardware semantics based on
temporal intervals, forthcoming.
7. D. Harel. First-Order Dynamic Logic. Springer-Yerlag, Berlin, 1979. Number
68 in the series Lecture Notes in Computer Science.
8. L. Lamport. Specifying concurrent program modules. Opus 60, Computer
Science Laboratory, SRI International, June, 1981.
9. S. Leinwand and T. Lamdan. Algebraic analysis of nondeterministic behavior.
Proceedings of the 17-th Design Automation Conference, Minneapolis, June,
1980, pages 483-493.
24
-------
10. T. M. McWilliams. Verification of timing constraints on large digital systems.
Proceedings of the 17-th Design Automation Conference, Minneapolis, June,
1980, pages 139-147.
11. Y. Malachi and S. S. Owicki. Temporal specifications of self-timed systems.
VLSI Systems and Computations, Rockville, Maryland, 1981, pages 203-212.
This book is the proceedings of a conference held at the Carnegie-Mellon
University in October, 1981.
12. Z. Manna and A. Pnuelii The modal logic of programs. Tech. Rept. STAN-CS-
79-751, Department of Computer Science, Stanford University, September,
1979.
13. P. Meinen. Formal semantic description of register transfer language elements
and mechanized simulator construction. Proceedings of the 4-th Interna-
tional Symposium on Computer Hardware Description Languages, Palo Alto,
California, October, 1979, pages 69-74.
14. B. Moszkowski. Reasoning about Digital Circuits. Ph.D. Thesis, Dept. of Com-
puter Science, Stanford University, forthcoming.
15. A. C. Parker and J. J. Wallace. SLIDE: An I/O hardware description language.
IEEE Transactions on Computers C-30, 6 (June 1981), pages 423-439.
16. D. A. Patterson. Strum: Structured microprogram development system for
correct firmware. IEEE Transactions on Computers C-25, 10 (October
1976), pages 974-985.
17. N. Rescher and A. Urquart: Temporal Logic. Springer-Verlag, New York, 1971.
18. R. L. Schwartz and P. M. Melliar-Smith. Temporal logic specification of
distributed systems. Proceedings of the Second International Conference on
Distributed Computing Systems, Paris, France, April, 1981, pages 446-454.
19. S. Y. H. Su, C. Huang and P. Y. K. Fu. A new multi-level hardware design
language (LALSD II) and translator. Proceedings of the IFIP TC-10 Fifth
International Conference on Computer Hardware Description Languages and
their Applications, Kaiserslautern, West Germany, September, 1981, pages
155-169.
20. T. Wagner. Hardware Verification. Ph.D. Thesis, Dept. of Computer Science,
Stanford University, September 1977.
25
-------
TECHNICAL REPORT DATA
A E ERL- P" 9 94 (Please read Instructions on the reverse before complet
1. REPORT NO.
EPA/600/A-92/197
2.
3.
4. TITLE AND SUBTITLE
Air Toxics: The Research Challenge of the 1990 Clean
5. REPORT DATE
Air Act Amendments
6. PERFORMING ORGANIZATION COOE
7. AUTHOR(S)
Frank T. Princiotta and Douglas G. McKinney
8. PERFORMING ORGANIZATION REPORT NO,
9. PERFORMING ORGANIZATION NAME AND ADORESS
10. PROGRAM ELEMENT NO.
See Block 12
11. CONTRACT/GRANT NO.
NA (Inhouse)
12. SPONSORING AGENCY NAME AND ADDRESS
EPA, Office of Research and Development
Air and Energy Engineering Research Laboratory
Research Triangle Park, NC 27711
13. TYPE OF REPORT AND PERIOD COVERED
Published paper; 11/91-9/92
14. SPONSORING AGENCY CODE
EPA/600/13
15. supplementary NOTES AEERL project officer is Douglas G. McKinney,
919/541-3006.
Mail Drop 60,
is. abstract The paper describes (1) major provisions of Title III of the 1990 Clean Air
Act Amendments (CAAAs) which formally established a new regulatory approach
which would avoid past impediments and accelerate emission reductions, and (2) the
research that the U. S. EPA has initiated to support state and federal regulatory of-
ficials as they implement the extensive new provisons of the CAAAs, Toxic emis-
sions from stationary air pollution sources have been recognized as a national health
problem for several decades. Unfortunately, a large percentage of these hazardous
air pollutant (HAP) emissions have not been controlled because, between 1977 and
1990, the risk-based federal regulatory program to reduce them addressed only a
few pollutants. Disputes between industry, the U. S. EPA, and environmental groups
over health effects data, exposure levels, and what constitutes an ample margin of
safety to protect the public health were the primary impediments to progress and
limited the number of National Emission Standards for Hazardous Air Pollutants
(NESHAPS) issued to only 10. The lack of progress toward reducing HAP emissions
raised public concern and convinced Congress to design the modified approach.
17.
KEY WORDS AND DOCUMENT ANALYSIS
a. DESCRIPTORS
b.IDENTIFIERS/OPEN ENDED TERMS
c. cosati Field/Group
Pollution
Toxicity
Research
Emission
Pollution Control
Stationary Sources
Air Toxics
Hazardous Air Emission
13 B
06T
14F
14 G
18. DISTRIBUTION STATEMENT
19. SECURITY CLASS (This Report)
Unclassified
21. NO. OF PAGES
8
Release to Public
20. SECURITY CLASS (This page)
Unclassified
22. PRICE
EPA Form 2220-1 (9-73)
------- |