English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Derivation and verification represent alternate approaches to design. Derivation aims at deriving a "correct by construction" design while verification aims at constructing a post factum "proof of correctness" for a design. However, as researchers and engineers gain design experience in a formal framework, both approaches are emerging as interdependent facets of design. The thesis of this work is that alternate forms of formal reasoning must be integrated if formal methods are to support the natural analytical and generative reasoning that takes place in engineering practice. As a vehicle for this research, the DDD digital design derivation system was implemented to study formal hardware design in an algebraic framework. DDD is a first-order transformation system which mechanizes a basic design algebra for synthesizing digital circuit descriptions from high-level functional specifications. The system is a collection of correctness preserving transformations that promote a top-down design methodology where the discipline of applicative programming is adapted to hardware verification. As a non-trivial illustration of these ideas, the derivation of the DDD-FM9001 is presented. The DDD-FM9001 is a 32-bit general purpose microprocessor mechanically derived directly from Hunt's Boyer-Moore Logic FM9001 microprocessor specification. The derivation involved the use of three mechanical verification tools: the DDD digital design derivation system, the Nqthm theorem prover, and the COSMOS boolean tautology checker. The DDD digital design derivation system was used to derive a significant portion of the design leaving relatively small portions to be verified by the other verification tools. The result of this experiment was a derived FM9001 defined by a rigorous path to hardware.

DDD-FM9001: Derivation of a verified microprocessor