Skip to main content
  • Book
  • © 2001

Synchronous Equivalence

Formal Methods for Embedded Systems

Buy it now

Buying options

eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (9 chapters)

  1. Front Matter

    Pages i-xi
  2. Introduction

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 1-10
  3. The Polis Codesign Framework

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 11-22
  4. Codesign Finite State Machines

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 23-39
  5. Formal Verification of CFSM Specifications

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 41-56
  6. Synchronous Equivalence

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 57-65
  7. Static Equivalence Analysis

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 67-79
  8. Communication Analysis

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 81-106
  9. Refining Communication Analysis

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 107-125
  10. Conclusions and Future Directions

    • Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli
    Pages 127-129
  11. Back Matter

    Pages 131-136

About this book

An embedded system is loosely defined as any system that utilizes electronics but is not perceived or used as a general-purpose computer. Traditionally, one or more electronic circuits or microprocessors are literally embedded in the system, either taking up roles that used to be performed by mechanical devices, or providing functionality that is not otherwise possible.
The goal of this book is to investigate how formal methods can be applied to the domain of embedded system design. The emphasis is on the specification, representation, validation, and design exploration of such systems from a high-level perspective. The authors review the framework upon which the theories and experiments are based, and through which the formal methods are linked to synthesis and simulation.
A formal verification methodology is formulated to verify general properties of the designs and demonstrate that this methodology is efficient in dealing with the problem of complexity and effective in finding bugs. However, manual intervention in the form of abstraction selection and separation of timing and functionality is required. It is conjectured that, for specific properties, efficient algorithms exist for completely automatic formal validations of systems.
Synchronous Equivalence: Formal Methods for Embedded Systems presents a brand new formal approach to high-level equivalence analysis. It opens design exploration avenues previously uncharted. It is a work that can stand alone but at the same time is fully compatible with the synthesis and simulation framework described in another book by Kluwer Academic Publishers Hardware-Software Co-Design of Embedded Systems: The POLIS Approach, by Balarin et al.
Synchronous Equivalence: Formal Methods for Embedded Systems will be of interest to embedded system designers (automotive electronics, consumer electronics, and telecommunications), micro-controller designers, CAD developers and students, as well as IP providers, architecture platform designers, operating system providers, and designers of VLSI circuits and systems.

Authors and Affiliations

  • University of California at Berkeley, USA

    Harry Hsieh, Alberto Sangiovanni-Vincentelli

  • Cadence Berkeley Laboratories, USA

    Felice Balarin

Bibliographic Information

  • Book Title: Synchronous Equivalence

  • Book Subtitle: Formal Methods for Embedded Systems

  • Authors: Harry Hsieh, Felice Balarin, Alberto Sangiovanni-Vincentelli

  • DOI: https://doi.org/10.1007/978-1-4615-1659-0

  • Publisher: Springer New York, NY

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer Science+Business Media New York 2001

  • Hardcover ISBN: 978-0-7923-7262-2Published: 31 December 2000

  • Softcover ISBN: 978-1-4613-5664-6Published: 05 November 2012

  • eBook ISBN: 978-1-4615-1659-0Published: 06 December 2012

  • Edition Number: 1

  • Number of Pages: XI, 136

  • Topics: Circuits and Systems, Artificial Intelligence, Computer-Aided Engineering (CAD, CAE) and Design, Electrical Engineering

Buy it now

Buying options

eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access