Formal Synthesis in Circuit Design -- A Classification and Survey
---
paper_title: The high-level synthesis of digital systems

paper_content:

High-level synthesis systems start with an abstract behavioral specification of a digital system and find a register-transfer level structure that realizes the given behavior. The various tasks involved in developing a register-transfer level structure from an algorithmic level specification are described. In particular, it is shown how the high-level synthesis task can be decomposed into a number of distinct but not independent subtasks. The techniques that have been developed for solving those subtasks are presented. Areas related to high-level synthesis that are still open problems are examined. >
---
paper_title: Formal hardware verification methods: a survey

paper_content:

Growing advances in VLSI technology have led to an increased level of complexity in current hardware systems. Late detection of design errors typically results in higher costs due to the associated time delay as well as loss of production. Thus it is important that hardware designs be free of errors. Formal verification has become an increasingly important technique towards establishing the correctness of hardware designs. In this article we survey the research that has been done in this area, with an emphasis on more recent trends. We present a classification framework for the various methods, based on the forms of the specification, the implementation, and the proff method. This framework enables us to better highlight the relationships and interactions between seemingly different approaches.
---
paper_title: On verifying the correctness of retimed circuits

paper_content:

We address the problem of verifying a retimed circuit. After retiming, some latches in a sequential circuit are repositioned to reduce the clock cycle time and thus the behavior of the combinational portion is changed. Here, we present a novel approach to check the correctness of a retimed circuit according to the definition of 3-valued equivalence. This approach is based on our verification framework using sequential ATPG techniques. We further incorporate an algorithm to pre-process the circuits and make the verification process even more efficient. We will present the experimental results of verifying the retimed circuits with hundreds of flip-flops on ISCAS89 benchmark circuits to show its capability.
---
paper_title: Exploiting functional dependencies in finite state machine verification

paper_content:

This paper proposes a novel verification method for finite state machines (FSMs), which automatically exploits the relation between the state encodings of the FSMs under consideration. It is based on the detection and utilization of functionally dependent state variables. This significantly extends the ability of the verification method to handle FSMs with similar state encodings. The effectiveness of the proposed method is illustrated by experimental results on well-known benchmarks.
---
paper_title: Using Nuprl for the verification and synthesis of hardware

paper_content:

The Nuprl proof development system, based on constructive type theory, has a sophisticated proof editor and user interface which facilitates the development of proofs and specifications. We present our experience using Nuprl for hardware verification and. synthesis. We have verified floating point hardware and are extending this work to reasoning about the IEEE floating point specification. In addition we are using Nuprl to reason about software for synthesizing hardware designs at several different levels. We present two efforts in this area. In the first, we prove a system that synthesizes CMOS circuits from boolean equations. The second system, PBS, minimizes large sets of boolean formulae by using the weak division algorithm.
---
paper_title: High level synthesis and generating FPGAs with the BEDROC system

paper_content:

Bedroc is a digital hardware synthesis system that automatically translates a behavioral description written in a hardware description language to field programmable gate arrays.Bedroc allows designers to specify their designs at a very high level of abstraction, and compile them into designs that can be realized in one of many different technologies. It can synthesize a wide variety of synchronous designs including signal processing applications, arithmetic applications, and general purpose processors. An additional aim of theBedroc project is to incorporate formal methods into the hardware synthesis process. By verifying the algorithms used for synthesis instead of the synthesized designs, we give the designer many of the benefits of formal methods without their having to learn new techniques. We have usedBedroc to synthesize several circuits from the High Level Synthesis Workshop benchmarks, including a wave digital elliptic filter.
---
paper_title: Verifying a logic-synthesis algorithm and implementation: a case study in software verification

paper_content:

We describe the verification of a logic synthesis tool with the Nuprl proof development system. The logic synthesis tool, Pbs, implements the weak division algorithm. Pbs consists of approximately 1000 lines of code implemented in a functional subset of Standard ML. It is a proven and usable implementation and is an integral part of the Bedroc high level synthesis system. The program was verified by embedding the subset of Standard ML in Nuprl and then verifying the correctness of the implementation of Pbs in the Nuprl logic. The proof required approximately 500 theorems. In the process of verifying Pbs we developed a consistent approach for using a proof development system to reason about functional programs. The approach hides implementation details and uses higher order theorems to structure proofs and aid in abstract reasoning. Our approach is quite general, should be applicable to any higher order proof system, and can aid in the future verification of large software implementations. >
---
paper_title: The BEDROC high level synthesis system

paper_content:

BEDROC is a digital hardware synthesis system that automatically translates a behavioral description written in a hardware description language to field programmable gate arrays. The authors have used BEDROC to synthesize several circuits from the high level synthesis workshop benchmarks. BEDROC is unusual in its aim to incorporate formal methods into the hardware synthesis process. By verifying the algorithms used for synthesis instead of the synthesized designs, the designer gets many of the benefits of formal methods without having to learn new techniques. >
---
paper_title: PBS: proven Boolean simplification

paper_content:

We describe PBS, a formally proven implementation of multi-level logic synthesis based on the weak division algorithm. We have proved that for all legal input circuits, PBS generates an output circuit that is functionally correct and has minimal size. PBS runs on large examples in reasonable time for a prototype system. PBS, was verified using the Nuprl proof development system. The proof of PBS, which required several months, was well worth the effort since the benefits are realized every time the program is run. When engineers use a verified synthesis tool, they get the increased confidence of applying formal methods to their designs without the cost of varying each design produced. >
---
paper_title: The T-Ruby design system

paper_content:

This paper describes the T-Ruby system for designing VLSI circuits, starting from formal specifications in which they are described in terms of relational abstractions of their behaviour. The design process involves correctness-preserving transformations based on proved equivalences between relations, together with the addition of constraints. A class of implementable relations is defined. The tool enables such relations to be simulated or translated into a circuit description in VHDL. The design process is illustrated by the derivation of a circuit for 2-dimensional convolution.
---
paper_title: Transformational Rewriting with Ruby

paper_content:

Abstract This paper describes a tool for use in user-directed synthesis of circuits specified using the relational VLSI description language Ruby. The synthesis method is based on transformational rewriting of Ruby terms in accordance with previously defined term equivalences. The tool permits the introduction of constraints into the specification, thus enhancing the usefulness of the rewrite system in relation to simple rewriting.
---
paper_title: Specification and Formal Synthesis of Digital Circuits

paper_content:

Abstract To reduce the ‘time to market’ and be competitive, new design methodologies must be introduced in order to guarantee rigor of design practice and correctness and reliability of implementations. Formally based synthesis at the most abstract levels of design can be used to reach such goals. In the following we describe the activities carried on in the Design Automation Laboratory of Italtel concerning post design validation using OTTER, and formal synthesis using LAMBDA ( * ) . Particular emphasis is given to the problem of the integration of these design phases into the consolidated Italtel design flow through EDIF and VHDL interfaces. Comments on benefits and drawbacks as perceived by the industrial environment are included.
---
paper_title: Quantitative Evaluation of Formal Based Synthesis in ASIC Design

paper_content:

Formal based synthesis allows design space exploration to identify optimized implementations conforming to the initial abstract specification. Wepropose to exploit the synergies between formal synthesis (at high level of abstraction) and logic synthesis (at lower levels of abstraction). In this way a two-fold goal is reached: quantitative figures are provided as a measureof the applicability of formal reasoning in the design process, and the good integration of the two phases in a unified design flow is demonstrated. Users' benefits include both improved quality of the design process (reduced time-to-market) and improved reliability of the final products (increased competitive profile).
---
paper_title: Dependent types and formal synthesis

paper_content:

The relative advantages offered by the use of dependent types (rather than polymorphic ones) in a higher-order logic used for reasoning about digital systems are explored. Dependent types and subtypes are shown to provide an effective means of expressing the bounded, parametrized types typically encountered in this field. Heuristic methods can be used to minimize problems arising from the loss of decidable type-checking. A second topic discussed is formal synthesis, an approach to design in which the activities of behavioural synthesis and of formal verification are combined. The starting point is a behavioural specification, the end result is a specification of an implementation together with a proof of its correctness.
---
paper_title: Formally embedding existing high level synthesis algorithms

paper_content:

This paper introduces a general scheme for formally embedding high level synthesis by formulating its basic steps as transformations within higher order logic. A functional representation of a data flow graph is successively refined by means of generic logical transformations. Algorithms that are based on logical transformations guarantee “correctness by design”. They not only construct an implementation but also derive the proof for its formal correctness, on the fly. An extra postsynthesis-verification step becomes obsolete. The logical transformations presented in this paper form a framework for formally embedding existing high-level-synthesis procedures.
---
paper_title: Introduction to HOL: a theorem proving environment for higher order logic

paper_content:

Part I. Tutorial: 1. Introduction to ML 2. The HOL logic 3. Introduction to proof with HOL 4. Goal-oriented proof: tactics and tacticals 5. Example: a simple parity checker 6. How to program a proof tool 7. Example: the binomial theorem Part II. The Meta-Language ML: 8. The history of ML 9. Introduction and examples 10. Syntax of ML 11. Semantics of ML 12. ML types 13. Primitive ML identifier bindings 14. General purpose and list processing functions 15. ML system functions Part III. The Hol Logic: 16. Syntax and semantics 17. Theories Part IV. The Hol System: 18. The HOL logic in ML Part V. Theorem-Proving With HOL: 19. Derived inference rules 20. Conversions 21. Goal-directed proof: tactics and tacticals Appendices.
---
paper_title: Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL

paper_content:

This article describes the embedding of high level synthesis algorithms in HOL. For given standard synthesis steps, we describe, how its data can be mapped to terms in HOL and the synthesis process be expressed by means of a logical derivation. In contrast to post-synthesis verification techniques our approach is constructive in a sense that the proof is derived during synthesis rather than “guessed” afterwards. Therefore one does not get into the hardship of NP-completeness or undecidability. Our approach ensures correctness based on the HOL system and is also performed fully automatically.
---
paper_title: An Automata Theory Dedicated towards Formal Circuit Synthesis

paper_content:

We present a theory for automata in HOL, which is dedicated towards formal hardware synthesis. The theory contains definitions for formally representing and transforming automata. In this approach hardware is represented by automata descriptions and formal synthesis is performed by applying formally proven theorems. The approach presented is constructive — i.e. starting from specifications at higher levels of abstractions, synthesis can be performed by repeated applications of these transformations. Specialized refinements and optimizations at the RT and gate levels are discussed.
---

Title: Formal Synthesis in Circuit Design -- A Classification and Survey
Section 1: Introduction
Description 1: Discuss the concept of synthesis in circuit design, including the differences between handmade and automated synthesis approaches, and the motivation for formal synthesis.

Section 2: Definition and Delimitation of Formal Synthesis
Description 2: Define formal synthesis and differentiate it from related correct synthesis approaches like pre-synthesis verification, formal synthesis, and post-synthesis verification.

Section 3: Circuit Designer's Viewpoint
Description 3: Describe the criteria relevant to circuit designers, including synthesis time, automation, and the requirement for skills in formal methods.

Section 4: Tool Developer's Viewpoint
Description 4: Discuss the criteria important to tool developers, such as complexity of tool development, tool maintenance, and the skills required for developing the tools.

Section 5: Summary
Description 5: Summarize the discussion on pre-synthesis verification, formal synthesis, and post-synthesis verification, and weigh their acceptability from the viewpoints of circuit designers and tool developers.

Section 6: Classification of Formal Synthesis
Description 6: Classify formal synthesis into synthesis step-specific verification techniques and transformational derivation, and compare hardware-specific calculus with general-purpose calculus.

Section 7: Hardware-specific Calculus vs. General-purpose Calculus
Description 7: Compare the efficiency and security of hardware-specific calculus and general-purpose calculus approaches in transformational derivation.

Section 8: Transformational Derivation vs. Synthesis-Step Specific Verification
Description 8: Compare transformational derivation with synthesis-step specific verification in the context of guaranteeing correct synthesis.

Section 9: Examples
Description 9: Provide a brief overview of systems developed for formal synthesis, including PBS, RLEXT, RUBY, DDD, LAMBDA/DIALOG, VERITAS, and HASH.

Section 10: Comparison
Description 10: Compare the described formal synthesis systems based on the criteria of hardware representation, hardware transformation, and synthesis control.

Section 11: Conclusions
Description 11: Conclude with thoughts on the acceptance of formal methods, the limitations of post-synthesis verification, and the potential of formal synthesis for deriving correct designs.