Modeling a Hardware Synthesis Methodology in Isabelle.
Formal Synthesis is a methodology developed at the university of Kent for combining circuit design and verification, where a circuit is constructed from a proof that it meets a given formal specification. We have reinterpreted this methodology in ISABELLES theory of higher-order logic so that circuits are incrementally built during proofs using higher-order resolution. Our interpretation simplifies and extends Formal Synthesis both conceptually and in implementation. It also supports integration of this development style with other proof-based synthesis methodologies and leads to techniques for developing new classes of circuits, e.g., recursive descriptions of parametric designs.
Introduction
Verification by formal proof is time intensive and this is a burden in bringing
formal methods into software and hardware design. One approach to reducing the
verification burden is to combine development and verification by using a calculus
where development steps either guarantee correctness or, since proof steps are in
parallel to design steps, allow early detection of design errors. We present such
an approach here, using resolution to synthesize circuit designs during proofs of
their correctness. Our approach is based on modeling a particular methodology
for hierarchical design development within a synthesis by resolution framework.
Our starting point is a novel methodology for hardware synthesis, called Formal
Synthesis, proposed by the Veritas group at Kent [7]. In Formal Synthesis,
one starts with a design goal, which specifies the behavioral properties of a circuit
to be constructed, and interactively refines the design using a small but powerful
set of techniques, which allows the developer to hierarchically decompose specifications
and introduce subdesigns and library components in a natural way.
Internally, each technique consists of a pair of functions: a subgoaling function
and a validation function. The former decomposes a specification Spec into sub-
specifications Spec i . The latter takes proofs that some Circ i achieve Spec i , and
constructs an implementation Circ with a proof that Circ achieves Spec. When
the refinement is finished, the system composes the validation functions that
were applied and this constructs a theorem that a (synthesized) circuit satisfies
the original design goal.
To make the above clearer, consider one of the simpler techniques, called
Split. The subgoaling function reduces a design goal Spec 1 - Spec 2 to two new
design goals, one for each conjunct. The validation function is based on the rule
which explains how to combine implementations that achieve the subgoals into
an implementation which achieves the original goal. This kind of top-down problem
decomposition is in the spirit of (LCF style) tactics and designing a good
set of techniques is analogous to designing an appropriate set of tactics for a
problem domain. However, tactics decompose a goal into subgoals from which
a validation proves the original goal, whereas with techniques, the validation
proves a different theorem altogether. Formal Synthesis separates design goals
and techniques from ordinary theorem-proving goals and tactics. This is a conceptual
separation: they are different sorts of entities with different semantics.
Moreover they are treated differently in the implementation too and Formal
Synthesis required extending the Veritas theorem prover itself.
We show how to reinterpret Formal Synthesis as deductive synthesis based on
higher-order resolution. To do this, we begin with the final theorem that the Formal
Synthesis validations should deliver: a circuit achieves a stated specification.
However the circuit is not given up front; instead it is named by a metavariable.
Proof proceeds by applying rules in Isabelle which correspond to Veritas
validation rules like (1). Because rule application uses resolution, the metavari-
able is incrementally instantiated to the synthesized circuit. Let us illustrate this
with the Split technique. Our goal (simplifying slightly) is to prove a theorem
like ?Circ!Spec, where the question mark means that Circ is a metavariable.
If Spec is a conjunction, Spec 1 - Spec 2 , then we can resolve ?Circ!Spec 1 - Spec 2
with the rule in (1). The result is a substitution, ?Circ =?Imp 1 -?Imp 2 , and the
subgoals ?Imp 1 !Spec 1 and ?Imp 2 !Spec 2 . Further refinement of these subgoals
will generate instances of the ?Imp i and hence ?Circ.
There are a number of advantages to this reinterpretation. It is conceptually
simple. We do away with the subgoal and validation functions and let resolution
construct circuits. It is simple to implement. No changes are required to the
Isabelle system; instead, we derive rules and program tactics in an appropriate
extension of Isabelle's theory of higher-order logic (HOL). Moreover, the reinterpretation
makes it easy to implement new techniques that are compatible with
the Formal Synthesis style of development. In the past, we have worked on rules
and tactics for the synthesis of logic programs [1] and these programs are similar
to circuits: both can be described as conjunctive combinations of primitive relations
where existential quantification is used to 'pass values'. By moving Formal
Synthesis into a similar theorem proving setting, we could adapt and apply many
of our tactics and rules for logic programming synthesis to circuit synthesis. For
example, rules for developing recursive programs yield new techniques for developing
parameterized classes of circuits. We also exhibit (cf. Section 6) that the
kind of rules used for resolution-based development in the Lambda system are
compatible with our reinterpretation.
Background
We assume familiarity with Isabelle [10] and higher-order logic. Space limitations
restrict us to reviewing only notation and a few essentials.
Isabelle is an interactive tactic-based theorem prover. Logics are encoded
in Isabelle's metalogic by declaring a theory, which is a signature and set of
axioms. For example, propositional logic might have a type F orm of formulae,
with constructors like - and a typical proof rule would be !!
(B =) A - B). Here =) and !! are implication and universal quantification
in Isabelle's metalogic. Outermost (meta-)quantifiers are often omitted and
iterated implication is written in a more readable list notation, e.g.,
A - B. These implicitly quantified variables are treated as metavariables, which
can be instantiated when applying the rule using higher-order unification. In our
work we use Isabelle's theory of higher-order logic, extended with theories of
sets, well founded recursion, natural numbers, and the like.
Isabelle supports proof construction by higher-order resolution. Given a proof
state with subgoal / and a proof rule we unify OE with /. If this
succeeds, then unification yields a substitution oe and the proof state is updated
by applying oe to it and replacing / with the subgoals oe(OE
unification is used to apply rules, the proof state itself may contain metavariables.
We use this to synthesize circuits during proofs. Note that a proof rule can
be read as an intuitionistic sequent where the OE i are the hypotheses. Isabelle's
resolution tactics apply rules in a way that maintains this illusion of working
with sequents and we will often refer to the OE i as assumptions.
Veritas [8] is a tactic based theorem prover similar to Isabelle and HOL,
but its higher-order logic is augmented with constructions from type theory,
e.g., standard type constructors such as (dependent) function space, product,
and subtype. When used to reason about hardware, one proves theorems that
relate circuits, Circ, to specifications, Spec, e.g.,
are the external port names. As is common, hardware is represented
relationally, where primitive constructors (e.g., transistors, gates, etc.)
are relations combined with conjunction and 'wired together' using existential
quantification [3]. The variables in p1 are typed, and the primary difference
between Veritas and similar systems is that one can use richer types in such
specifications. For example, if we are defining circuits operating over 8-bit words,
we would formalize this requirement on word-length in the types.
3 Formal Synthesis
Formal Synthesis is based on techniques. As previously indicated, each technique
combines a subgoaling function with a validation. The validations are executed
when a derivation is completed to build a proof that a circuit achieves an im-
plementation. Before giving the techniques we introduce some notation used
by Formal Synthesis. A design specification spec which is to be implemented is
written 2spec (2 is just a symbol; there is no relationship to modal logics). A
formula Thm to be proved is written as ' Thm. A term Tm to be demonstrated
well typed is written as 3Tm. A proof in Veritas is associated with a support
Name Subgoaling rule Validation rule
'Imp!Spec
Reveal 29dec: Spec
'(9dec: Imp)!(9dec:Spec)
Inside 2Circ b= -dec: Spec
ports
Library 2library part args
'library part args!library part args
Subdesign 2Spec
'(let c b
Design 2subdesign args
'subdesign args!subdesign args
Proof 'Thm \PiTm
'Thm 'Tm

Table

1. Veritas design techniques
signature, which contains the theory used (e.g., datatype definitions), definitions
of predicates, and the like. In Veritas, the signature can be extended dynamically
during proof. If a technique extends the signature of a goal Spec, then this
is written as [[extension]]Spec. Finally, the initial design goal must be of the form
Circ is the name assigned to the circuit.
There are eight techniques and these are adequate to develop any combinational
circuit in a structured hierarchical way. The subgoaling and validation
functions are both based on rules. The subgoaling rules should be read top-
down: to implement the goal above the line, solve all subgoals below the line.
The validation rules operate in the opposite direction: the goal below the line is
established from proofs of the goals above the line. These rules behave as follows:
Claim: The subgoaling function yields a new design goal Spec 0 and a subgoal
that this suffices for Spec. The validation is based on the transitivity of !.
Split: The subgoaling function decomposes a conjunctive specification into the
problem of implementing each conjunct. The validation constructs a design from
designs for the two subparts.
Reveal: Shifts internally quantified ports into the signature, allowing further
refinement.
Inside: Since the initial design goal is given as a lambda abstraction, a technique
is needed to remove this binding. To implement the circuit Circ means to
implement the specification Spec. The validation theorem states that the implementation
is correct for all port-values that can appear at the ports port , which
are declared in the declaration dec.
Library: The subgoaling function imports components from a database of pre-defined
circuits. The validation corresponds to the use of a lemma.
Subdesign: A subdesign, submitted as a lambda abstraction, may be intro-
duced. It must be implemented (second subgoal) and may be used in proving
the original design goal (first subgoal).
Design: Like the Library technique, this enables the user to apply a design that
has already been implemented. In this case, the implementation is a subdesign
introduced during the design process.
Proof: Veritas is used to prove a theorem.
4 Implementation and Extension
We now describe our reinterpretation of Formal Synthesis in Isabelle. We divide
our presentation in several parts, which roughly correspond to Isabelle
theories that we implemented: circuit abstractions and 'concrete technology',
technique reinterpretation, and new techniques.
4.1 Circuit Abstractions and Concrete Technology
We represent circuits as relations over port-values. We model kinds of signals as
sets and we use Isabelle's set theory (in HOL) to imitate the dependent types
of the Veritas logic; hence quantifiers used in our encoding are the bound
quantifiers of Isabelle's set theory. We name the connectives that serve as
constructors for circuits with the following definitions.
We will say more about the types P and W shortly. After definition, we derive
rules which characterize these operators and use these rules in subsequent proofs
(rather than expanding definitions). For example, using properties of conjunction
and implication we derive (hence we are guaranteed of their correctness) in
Isabelle the following rules which relate Join to Sat.
Associating definitions with such characterization theorems increases comprehensibility
and provides some abstraction: if we change definitions we can reuse
our theories provided the characterization theorems are still derivable. Definitions
have a second function: they distinguish circuit constructors from propositional
connectives and this restricts resolution (e.g., Join does not unify with
-) and makes it easier to write tactics that automate design.
Using the above abstractions, we can express the correctness of a (to be
synthesized) circuit with respect to a specification as
This is not quite adequate though to simulate Formal Synthesis style proofs.
A small problem is that the application of the techniques Reveal, Inside, and
Subdesign extend the Veritas signature. As there is no direct analog of dynamic
signature extension in Isabelle, we model Reveal and Inside using bounded
quantification and achieve an effect similar to signature extension by adding
declaration information to the assumptions of the proof state according to the
rules of set theory. Subdesign, which in Veritas extends the signature with a
new definition is slightly trickier to model; we regard the new definition as a
condition necessary for the validity of the correctness theorem and we express
this condition using ordinary implication. Of course, when stating the initial
goal we do not yet know which definitions will be made, so again we use a
metavariable to leave this as an unknown. Thus a theorem that we prove takes
the initial form
Analogous to the Formal Synthesis design goals we call such a theorem a design
theorem. The constant is simply the identity function and Def(?Definitions)
serves as a kind of 'definition context'. Each time a definition is made, ?Definitions
is instantiated to a conjunction of the definition and a fresh metavariable, which
can be instantiated further with definitions made later.
In the design theorem, wires are bound to types these types are defined
in theories about 'concrete technologies', e.g., representations of voltage, signals,
and the like. A simple instance is where port values range over a datatype bin
where voltage takes either the value Lo or Hi. We use Isabelle's HOL set theory
to define a set bin containing these two elements. Afterwards, we derive standard
rules for bin, e.g., case-analysis over binary values.
We extend our theory with tactics that automate most common kinds of
reasoning about binary values. For example, we have tactics that perform exhaustive
analysis on Port values quantified over bin and tactics that combine
such case analysis with Isabelle's simplifier and heuristic based proof procedure
(fast tac) for HOL. These tactics automate almost all standard kinds of
reasoning about combinational circuits.
We extend our voltage theory with a theory of gates that declares the types
of gates and axiomatizes their behavior. For example, the and gate is a predicate
of type [bin; bin; bin] ) bool whose behaviour is axiomatized as
Such axioms form part of a library of circuit specifications and are used to
synthesize parts of circuits.
4.2 Reinterpreting Techniques
We have implemented tactics that simulate the first seven techniques (for
the Proof technique we simply call the prover). Table 2 lists the tactics and the
derived rules corresponding to the Veritas techniques. The tactics are based
Reveal: reveal tac i
Inside: inside tac i
Library: library tac dels elims thm i
Subdesign: subdesign tac str i
Design: design tac dels elims i

Table

2. Isabelle Techniques (Name, Tactic, and Rule)
on the derived rules, which correspond to the validation rule associated with the
Veritas technique; their function is mostly self explanatory.
Claim and Split: The tactics apply rules that are direct translations of the
corresponding Veritas validation rules. The specification Spec 0 is supplied as a
string str to claim tac.
Reveal and Inside: These are identical to the Veritas techniques except that
internal wiring, or quantification over ports, is converted to quantification at
the metalevel and type constraints (expressed in Isabelle's HOL set-theory)
become assumptions. The rules state that if an implementation satisfies its spec-
ification, then we can wire a signal to a port with Inside or we can hide it as
an internal wiring with Reveal. reveal tac and inside tac apply their respective
rule as many times as possible to the specified goal.
Library: library tac solves the design goal R by using a previously implemented
design, supplied by the user. The rule is a form of implication elimination. The
first subgoal is instantiated with the component's design theorem. The second
is solved by extending the definition context of the overall design. The third
establishes the correctness of the design using the specification of the library
component. This involves type checking for the ports, which depends on the
concrete technology of the designs; hence we supply the tactic with additional
'elimination' and `deletion' rules, which solve the type checking goals.
Subdesign: We have given an informal rule schema (the others are formally
derived) that represents infinitely many rules (there are arbitrarily many quan-
tifiers, indicated by the ellipses). subdesign tac simulates the effect of applying
such a rule. The user gives the design goal of the subdesign to be implemented
in the same form as the initial goal. Three new subgoals are generated by the
tactic. The first corresponds to the subdesign definition and the tactic discharges
this by adding it to the definition context of the main design. The second sub-goal
commits us to implement the subdesign. The third allows us to use the
subdesign when proving the original subgoal.
Design: This solves a design goal by using a previously introduced subdesign.
The subdesign has been given as a design goal, which is part of the assumptions
of the goal to be solved. The tactic removes all port quantifiers for the assumption
by repeatedly applying the associated rule. For each port a new subgoal is
generated, which concerns the type of that port, and is solved as in the Library
technique; hence we provide lists of type checking rules to the tactic.
Proof: General proof goals arise from the application of the Claim rule. These
are undecidable in general and must be proven by the user.
4.3 Extensions of the Calculus
The techniques defined by Formal Synthesis are effective for developing combinational
circuits. However, nontrivial circuits are often best developed as instances
of parametric designs. For example, rather than designing a 16-bit adder it is
preferable to develop one parameterized by word-length and afterwards to compute
particular instances. We have developed new techniques that are compatible
with our reinterpretation of Formal Synthesis and construct such parameterized
circuits. Structural induction is used to build parameterized linear circuits and
more generally n-dimensional grids, and course-of-values induction is used to
build general recursively defined designs. We will consider course-of-values induction
below and later apply it to build a tree-structured addition circuit.
The idea for such extensions is motivated by previous work of ours on calculi
in Isabelle for synthesizing recursive logic programs [1]. There we developed
rules and tactics based on induction which extend definition contexts with templates
(a function or predicate name with a metavariable standing in for the
body) for recursive definitions and leave the user with a goal to prove where
use of the induction hypothesis builds a recursive program. This past work has
much in common with our technique-based calculus for circuits. Syntactically,
logic programs and circuits are similar: both can be described as conjunctive
combinations of primitive relations where existential quantification 'passes val-
ues'. It turns out that we could (with very minor adaptation) directly use the
rules and tactics we developed for synthesizing logic programs to build recursive
circuits. We find this kind of reuse, not just of concepts but also of actual rules
and tactics, an attractive advantage of interpreting different synthesis methodologies
in a common framework. We will address this point again in Section 6
where we consider how techniques developed for the Lambda system can also
be applied in the Formal Synthesis setting.
We construct a parameterized circuit by proving a parameterized design the-
orem, which is a design theorem where the outermost quantifier (or quantifiers)
ranges over an inductively defined datatype like the natural numbers, e.g.,
specifies an implementation whose size depends on the number n. We use induction
to instantiate Circ to a recursively specified design. Isabelle's HOL comes
with a theory of natural numbers (given as an inductive definition) from which
it is easy to derive the following course-of-value induction rule.
We use this rule as the basis for a tactic, cov induct tac, which functions as if
the following rule schema were applied.
When this rule is applied by higher-order resolution, Spec will unify with
the specification of the design theorem, and Circ with the metavariable standing
for the circuit. The first subgoal sets up a parameterized circuit definition:
an equality for Circ is defined, where it is equal to Definition , which will be a
metavariable. Our tactic discharges this subgoal by adding it to the definitions
of the main design. This leaves us with the second goal, which is the design
goal. However, now we build a circuit named Definition and instantiating this
in subsequent proof steps will instantiate our definition for Circ. Moreover, we
now have a new assumption (the induction hypothesis),which states that Circ
achieves Spec for smaller values of k. If we can reduce the problem to implementing
a smaller design, then we can resolve with the induction hypothesis and this
will build a recursive design by instantiating the definition body of Circ with an
instance of Circ. How this works in practice will become clearer in Section 5.2.
Parameterized specifications require parameterized input types, e.g., rather
than having input ports, we have parameterized input busses. To support this we
develop a theory of busses encoded as lists of specified lengths (there are other
possibilities, but this allows us to directly use Isabelle's list theory). Some of
our definitions are as follows.
A bus (B bus (n)) is a list of length n and whose members are from the set
B. The functions upper and lower return the upper and lower n bits (when they
exist) from a bus b and l'n returns the nth element of a bus. We have proven
many standard facts about these definitions, e.g., we can decompose busses.
5 Examples
We present two examples. Our first example is a comparator developed using
Formal Synthesis in [7]. It illustrates how we can directly mimic Formal Synthesis
to create hierarchical designs. Our second example uses induction to construct
a parameterized tree-shaped adder.
5.1 Comparator Cell
A comparator takes as input two words A and B, representing numerals, and
determines their relative order, i.e., which of the three cases A ! B,
holds. Such a circuit can be built in a ripple-carry fashion from comparator
cells. These cells (left-hand figure in Figure 1) compare a bit from A and B and
also have as input three bits (one for each case) which are the result of previous
comparisons (grin , eqin , and lsin), and as output three bits (grout , eqout , lsout).
The behavioral specification is:
CompCellS(a, b, grin, eqin, lsin, grout, eqout, lsout) ==
The function vl is defined in our theory of binary values:
We can now submit the following design theorem to Isabelle.
(Port a:bin b:bin grin:bin eqin:bin lsin:bin grout:bin eqout:bin lsout:bin.
CompCellS(a, b, grin, eqin, lsin, grout, eqout, lsout))
We apply an initialization tactic which sets up the design goal by implication
introduction (which moves the definition context into the assumption list) and
applies the Inside tactic; this yields the following proof state (we elide some
information about the typing of the ports).
CompCellS(a, b, grin, eqin, lsin, grout, eqout, lsout))
1. !! a b grin eqin lsin grout eqout lsout.
grin
eqin
lsin
grin
eqin
lsin
a b
a b
BitComp
CompCell
lsout
eqout
grout
grout
eqout
lsout
Fig. 1. Comp-cell and its claimed implementation
The original goal is given on the first-three lines; it contains two metavariables
?Circ and ?H standing for the implementation of CompCellS and the definitions
that will be made, respectively. These are also present in the following lines
(which contain the subgoal that must be established to prove the original goal)
and will be instantiated when proving this subgoal. Next we introduce a new
subdesign BitComp that we will use as a component. The idea is that we first
compare the two bits a and b representing the current digit. Then we combine
the result of this comparison with information coming from comparisons of less
significant bits to give the result. The specification of the BitComp subdesign is
the following.
We apply subdesign tac and this yields two subgoals. At the top, we see our
original goal where the definition context ?H was extended with a definition for
BitComp and there is a new metavariable ?G for further definitions. The first
subgoal is a design theorem for the subdesign. The second is the original design
theorem but now with an additional assumption that there is an implementation
of the subdesign which satisfies the specification BitCompS.
(Port a:bin b:bin gr:bin eq:bin ls:bin.
CompCellS(a, b, grin, eqin, lsin, grout, eqout, lsout)
1.
2. !! a b grin eqin lsin grout eqout lsout.
BitLess BitLess
BitComp
BitLess
ls eq gr
a
z
x y
Fig. 2. Claimed implementations of bit-comp and bit-less
Given this subdesign we use claim tac to state that the following specification
entails the original goal (Figure 1).
EX gr:bin eq:bin ls:bin x:bin y:bin.
andS(eq, eqin, eqout) & andS(eq, lsin, ls) & orS(ls, y, lsout)
Due to space limitations we will just sketch the remaining proof. First we
show that the claimed specification entails the original one; we prove this automatically
using a tactic that performs case-analysis and simplification. After,
we implement it by using reveal tac to strip existential quantifications (and
introduce internal wires) and then use split tac to break up the conjunctions
(and Join together subcircuits). The components are each implemented either
by introducing simpler subdesigns and implementing those (see below), or using
library tac, which accesses appropriate library parts, and using design tac, to
apply developed subdesigns.
Let us sketch one of these remaining tasks: implementing the subdesign
BitCompS. We proceed in the same manner as earlier and we introduce a new
subdesign BitLess ; then we build the above BitComp using BitLess twice as shown
in

Figure

2. Finally, BitLessS is so simple that we can claim a direct implementation
consisting of components from the library. After these steps, the design
theorem that we have proved is the following.
(Port x:bin y:bin z:bin. ?BitLess(x, y, y, z))) -?
and(eq, eqin, eqout) Join and(eq, lsin, ls) Join or(ls, y, lsout))
Sat CompCellS(a, b, grin, eqin, lsin, grout, eqout, lsout)
The metavariable ?H has become instantiated with the conjunction of the
definitions of the subdesigns used in the implementation of the main design goal,
i.e., BitComp and BitLess . In the main goal, the unknown ?Circ has become a
predicate that represents the structure of the desired circuit and is built from
these subdesigns and additional and and or gates. Overall, our proof builds the
same circuit and uses the identical sequence of technique applications as that
presented in [7]. The difference is not so much in the techniques applied, but
rather the underlying conceptualization and implementation: in the Veritas
system, the implementation is constructed at the end of the proof by the validation
functions, whereas in our setting, the design takes shape incrementally
during the proof. We find this advantageous since we can directly see the effects
of each design decision taken.
5.2 Carry Lookahead Adder
Our second example illustrates how our well-founded induction technique synthesizes
parameterized designs: We synthesize a carry lookahead adder (henceforth,
cla-adder) that is parametric in its bit-width n. For n-bit numbers, such an adder
has a height that is proportional to log(n) and thus computes the sum s and a
carry co from two numbers a, b and an incoming carry c i in O(log(n)) time. Instead
of propagating the carry from digit to digit as it is done in a ripple-carry
adder, we compute more detailed information (c.f. [9]). A generate bit g indicates
when a carry is generated by adding the digits of a and b and a propagate bit
indicates if an incoming carry is handed through. From this information we
obtain the carry bit co for the adder in the following way: it is Hi if Hi or
if both carry lookahead adder is implemented, roughly
speaking, by recursively decomposing it in two adders, each half the size of the
original. The propagate and generate bits for the overall adder are obtained by
combining the corresponding bits of the subparts with the incoming carry c i . In
the case of adding single digits of a and b (the base case of the recursion) the
propagate bit corresponds to the logical or and the generate bit corresponds to
the logical and of the digits.
The adder we synthesize is built from two components (Figure 3). The first,
cla, computes the sum s, the propagate bit p and the generate bit g from the
numbers a and b and the incoming carry c i . The second is an auxiliary component
aux , which is used to combine the propagate bit, the generate bit and the
incoming carry to the outgoing carry co . This component consists of two gates
and can be derived in a few steps. We focus here on the development of the more
interesting component cla . We can specify its behavior using data abstraction
by an arithmetic expression.
claS(n,a,b,s,p,g,ci) ==
case g of
Hi =?
Note that numbers are represented by busses (i.e. bit vectors) and the value of
a bus as a natural number is given by val. We assume busses to have a nonzero
length. Hence in the following design theorem, we restrict induction to the set
nnat(1) of natural numbers greater than zero.
bus n) b:(bin bus n) s:(bin bus n) p:bin g:bin ci:bin.
n)
cla(
Carry lookahead adder
aux
s a b
ci
aux
co
x
Fig. 3. Implementation of a cla-adder from two components
As before, we begin by shifting the definition environment Def(?H) to the as-
sumptions. After, we apply the course-of-values induction tactic which yields the
following proof state
bus n) b:(bin bus n) s:(bin bus n) p:bin g:bin ci:bin.
?cla(n, a, b, s, p, g,
(ALL n:nnat(1). Port a:(bin bus n) b:(bin bus n) s:(bin bus n) p:bin g:bin ci:bin .
?cla(n, a, b, s, p, g, ci) Sat claS(n, a, b, s, p, g, ci))
1. !!n. [-
(Port a:(bin bus
?cla(k, a, b, s, p, g, ci) Sat claS(k, a, b, s, p, g, ci)) -] ==?
a:(bin bus n) b:(bin bus n) s:(bin bus n) p:bin g:bin ci:bin .
?D16(n, a, b, s, p, g, ci) Sat claS(n, a, b, s, p, g, ci)
As previously described, ?H is extended with a definition template and further
definitions are collected in ?Q2 . The metavariable at the left-hand side of
the definition serves as the name for the design being defined. The metavariable
on the right-hand side will be instantiated with the implementation when we
prove subgoal 1. The induction hypothesis is added to the assumptions of that
subgoal: We may assume that we have an implementation for all k less than n
and that we can use this to build a circuit of size n.
We proceed by performing a case analysis on n. We type by(if-tac "n=1" 1),
which resolves subgoal 1 with the rule
where P is instantiated with
bus n) b:(bin bus n) s:(bin bus n) p:bin g:bin ci:bin .
?cla(n, a, b, s, p, g,
cla-base
s a b
cla(
c
c
aux
aux
carry
carry
c
lower( upper(
lower(
lower( upper(
l, a
l, s
l, b
u, a )
u, b
u, s
cla(
Fig. 4. Base case (left) and recursive decomposition (middle/right) where
and
(ALL n:nnat(1). Port a:(bin bus n) b:(bin bus n) s:(bin bus n) p:bin g:bin ci:bin .
?cla(n, a, b, s, p, g, ci) Sat claS(n, a, b, s, p, g, ci))
1. !!n a b s p g ci.
[-
(Port a:(bin bus
cla(k, a, b, s, p, g, ci) Sat claS(k, a, b, s, p, g, ci));
a:bin bus n; b:bin bus n; s:bin bus n; p:bin; g:bin; ci:bin;
?C23(n, a, b, s, p, g, ci) Sat claS(n, a, b, s, p, g, ci)
2. !!n a b s p g ci.
[-
(Port a:(bin bus
cla(k, a, b, s, p, g, c) Sat claS(k, a, b, s, p, g, ci));
a:bin bus n; b:bin bus n; s:bin bus n; p:bin; g:bin; ci:bin; n ~= 1 -] ==?
?C'23(n, a, b, s, p, g, ci) Sat claS(n, a, b, s, p, g, ci)
In the overall design goal, the right-hand side of the definition has been instantiated
with a conditional whose alternatives ?C23 and ?C 0
are the respective
implementations for the base and the step case. The former is to be implemented
by proving subgoal 1 under the assumption the latter by proving subgoal
2 under the assumption n 6= 1. The base case is solved by the subdesign cla base

Figure

in a few simple steps.
In the step case we build the adder from two smaller adders of half the size:
We decompose the busses a, b and s each in a segment lower(n div 2; ) containing
the inferior n div 2 bits of the bus and a segment upper(n div 2+nmod 2; ), containing
the remaining bits. The lower (upper) segments of a and b can be added by
an adder of bit-width n div 2 (n div 2+nmod 2) yielding the lower (upper) segment
of the sum s. The propagate, generate and carry bit for the overall adder and
the carry flowing from the lower to the upper part of the adder are computed
by some additional circuitry collected in a new subdesign. Accordingly we can
reformulate the specification for the component cla as follows.
claim-tac
" EX p0:bin. EX g0:bin. EX p1:bin. EX g1:bin. EX c1:bin.
claS(n div 2, lower(n div 2, a), lower(n div 2, b), lower(n div 2, s), p0, g0, c) &
claS(n
The proof that this new specification entails the original is accomplished automatically
by a tactic we implemented that performs exhaustive case analysis
on the values of the carry, propagate and generate bits and performs simplification
of arithmetic expressions.
We decompose the new specification into its subparts and implement the
recursive occurrences of the specification claS by using the induction hypothesis.
This is done by applying design tac twice. The remaining specification carryS is
solved by a new subdesign, which is implemented as shown in Figure 4. Note
that we reuse the formerly developed aux here. Thus, all design goals are solved
and after 39 steps we are finished.
bus n) b:(bin bus n) s:(bin bus n) p:bin g:bin ci:bin.
?cla(n, a, b, s, p, g,
Wire p0:bin g0:bin p1:bin g1:bin c1:bin.
?cla(n div 2, lower(n div 2,a), lower(n div 2,b), lower(n div 2,s), p0, g0, ci) Join
(Port a:bin b:bin s:bin p:bin g:bin ci:bin.
(Wire w:bin. xor(a, b, w) Join xor(w, ci, s) Join or(a, b, p) Join and(a, b,
(Port p0:bin g0:bin p1:bin g1:bin c1:bin p:bin g:bin ci:bin .
(Port u:bin v:bin w:bin x:bin .
(ALL n:nnat(1). Port a:(bin bus n) b:(bin bus n) s:(bin bus n) p:bin g:bin ci:bin .
?cla(n, a, b, s, p, g, ci) Sat claS(n, a, b, s, p, g, ci))
In our definition context, ?H has become instantiated by four definitions.
There is a one to one correspondence between the implementations shown in

Figures

3 and 4 and the predicates defining them.
6 Comparison and Conclusion
We have combined two development methodologies: Formal Synthesis as implemented
in Veritas and resolution based synthesis in Isabelle. The result is a
simple realization of Formal Synthesis that is compatible with other approaches
to resolution based synthesis. Moreover, our implementation supports structural,
behavioral, and data-abstraction as well as independence from the concrete circuit
technology. Our implementation is based on a series of extensions to higher-order
logic and we were able to directly utilize standard Isabelle theories in our
work as well as Isabelle's simplification tactics. Most of our derived rules were
proven in one step proofs by Isabelle's classical prover.
The idea of using first-order resolution to build programs goes back to Green
in the 1960s [6]. More recently, within systems like Isabelle, interactive proof
by higher-order resolution has been used to construct verified programs and
hardware designs [1, 4, 10]. The work most closely related to ours is that of Mike
Fourman's group based on the Lambda system, which is a proof development
system that supports synthesis based on second-order resolution [5]. Motivated
by Isabelle, they too use rules in order to represent the design state. The difference
lies in the particular approach they use in proof construction; 1 instead
of using general purpose techniques as in Formal Synthesis, they derive (intro-
duction) rules for each component from its definition. These rules are applied
to the proof state in order to simplify the specification and thereby refine the
implementation. The specialized form of their rules supports a higher degree of
automation than general purpose techniques. Conversely, the generality of the
Formal Synthesis techniques provides a more abstract view of the design process
and better supports hierarchical development.
Just as we have extended Formal Synthesis with techniques for induction,
it is possible to adapt their methodology within our setting. We have carried
out some initial experiments which indicate both that we can use our Formal
Synthesis techniques to synthesize Lambda style design rules and that such rules
can be combined with techniques in circuit development. As a simple illustration,
suppose we have an axiom for an adder circuit given by
We can apply our techniques to synthesize a partial implementation for a schematic
specification Spec, which contains a subexpression of the form a
a:nat b:nat. ?Circ(a,b) Sat Spec(a+b)
After applying the techniques Inside, Claim, Reveal and Split, and solving the
proof obligation from Claim, we arrive at the following intermediate proof state.
a:nat b:nat.
(Wire s:nat.
1. !!a b s. [- a:nat; b:nat; s:nat -] ==?
After discharging the first subgoal by assuming it and removing the Port quan-
tifiers, we arrive at a Lambda-style design rule.
?a:nat; ?b:nat
Explaining this as a technique, it says that we can reduce a specification involving
the addition of a + b to one instead involving s. The validation tells us that the
1 In the end, there are only so many (700?) proof development systems, but there are
many more strategies for constructing proofs.
circuit built for Spec(s), when hooked up appropriately to an adder, builds a
circuit for the original specification. It would not be difficult to build tactics that
enable us to integrate such Lambda techniques with the others we developed,
taking advantage of the different strengths of these two approaches.
We conclude with a brief mention of deficiencies and future work. Currently,
the amount of information present during proof can be overwhelming. A short-term
solution is to instruct Isabelle to elide information; however, a graphical
interface, like that in Lambda would be of tremendous value both in displaying
designs and giving specifications. Another weakness is automation. We have
automated many simple kinds of reasoning by combining Isabelle's simplifiers
with case-analysis over binary values. The resulting tactics are effective, but
their execution is slow. There are decision procedures based on BDDs that can
more effectively solve many of these problems. We have started integrating one
of these with our synthesis environment, namely, a decision procedure for a
decidable monadic logic that is well-suited for modeling hardware [2]. We hope
that this is a step towards a synthesis framework in which different verification
methodologies may be integrated.



--R

Logic frameworks for logic programs.
Hardware verification using monadic second-order logic
Hardware verification using higher-order logic
Interactive program derivation.
Formal system design - interactive synthesis based on computer-assisted formal reasoning
Application of theorem proving to problem solving.
Formal synthesis of digital sys- tems

Computer Architecture
Isabelle : a generic theorem prover
--TR
higher-order logic;hardware verification and synthesis;higher-order unification;theorem proving