Idioma:

A formally verified system for logic synthesis

Aagaard, M. ; Leeser, M.

[1991 Proceedings] IEEE International Conference on Computer Design: VLSI in Computers and Processors, 1991, p.346-350

Texto completo disponível

Citações Citado por

Título:
A formally verified system for logic synthesis
Autor: Aagaard, M. ; Leeser, M.
Assuntos: Algorithm design and analysis ; Boolean algebra ; Boolean functions ; Circuit synthesis ; Computer languages ; Hardware ; High level synthesis ; Logic programming ; Process design ; Registers
É parte de: [1991 Proceedings] IEEE International Conference on Computer Design: VLSI in Computers and Processors, 1991, p.346-350
Descrição: The correctness of a logic synthesis system is implemented and proved. The algorithm is based on the weak division algorithm for Boolean simplification previously presented. The implementation is in the programming language ML; and the proof is in the Nuprl proof development system. This study begins with a proof of the algorithm previously presented and extends it to a level of detail sufficient for proving the implementation of the system. In the process of developing the proof many definitions presented in previous accounts of the algorithms were clarified, and several errors in the implementation were discovered. The result is that the designs generated by the implementation can be claimed to be correct by construction, since the correctness of the system was proven.< >
Editor: IEEE Comput. Soc. Press
Idioma: Inglês

Voltar para lista de resultados

Resultado 1 Avançar Ir para próxima página