Greaves describes how formal methods can be used to design systems and circuits. In his approach, he exploits the existence of SAT solvers to check if a system satisfies its specification or not. Systems to be checked are modeled as field-programmable gate array (FPGA) constructs, and converted into predicate logic formulas. These formulas are then converted into conjunctive normal form, with free variables being considered universally quantified. This supports the breaking down of predicate logic formalisms of theorem proving to the propositional level. The approach is illustrated with two examples: an encoder/decoder, and a two-rail coder.

The author points out that the SAT instances that are generated from the tested examples have been solved very quickly, though they are rather large (with respect to the number of variables involved). This point might be worth more in-depth study. In particular, it would be interesting to see what the structure of the generated formulas exactly looks like (with respect to some regularities, or similar parameters).

The problem with this paper is the following: although the approach is not that difficult to understand, the treatment is (in my opinion) much too short. This might be the result of a page limit set by the organizers of the workshop, so a more detailed paper would be helpful.