{"id":{"repo_id":"soton","oai_identifier":"oai:eprints.soton.ac.uk:171695"},"canonical_url":"https://search.dev.ndltd.org/etd/soton/oai:eprints.soton.ac.uk:171695","repository":{"repo_id":"soton","name":"University of Southampton","base_url":"https://eprints.soton.ac.uk/cgi/oai2"},"display":{"title":"Guarded atomic actions and refinement in a system-on-chip development flow: bridging the specification gap with Event-B","abstract":"Modern System-on-chip (SoC) hardware design puts considerable pressure on existing design and verification flows, languages and tools. The Register Transfer Level (RTL)description, which forms the input for synchronous, logic synthesis-driven design is at too low a level of abstraction for efficient architectural exploration and re-use. The existing methods for taking a high-level paper specification and refining this specification to an implementation that meets its performance criteria is largely manual and error-prone and as RTL descriptions get larger, a systematic design method is necessary to address explicitly the timing issues that arise when applying logic synthesis to such large blocks.<br/><br/>Guarded Atomic Actions have been shown to offer a convenient notation for describing microarchitectures that is amenable to formal reasoning and high-level synthesis. Event-B is a language and method that supports the development of specifications with automatic proof and refinement, based on guarded atomic actions. Latency-insensitive design ensures that a design composed of functionally correct components will be independent of communication latency. A method has been developed which uses Event-B for latency-insensitive SoC component and sub-system design which can be combined with high-level, component synthesis to enable architectural exploration and re-use at the specification level and to close the specification gap in the SoC hardware flow.","abstract_html":"Modern System-on-chip (SoC) hardware design puts considerable pressure on existing design and verification flows, languages and tools. The Register Transfer Level (RTL)description, which forms the input for synchronous, logic synthesis-driven design is at too low a level of abstraction for efficient architectural exploration and re-use. The existing methods for taking a high-level paper specification and refining this specification to an implementation that meets its performance criteria is largely manual and error-prone and as RTL descriptions get larger, a systematic design method is necessary to address explicitly the timing issues that arise when applying logic synthesis to such large blocks.&lt;br/&gt;&lt;br/&gt;Guarded Atomic Actions have been shown to offer a convenient notation for describing microarchitectures that is amenable to formal reasoning and high-level synthesis. Event-B is a language and method that supports the development of specifications with automatic proof and refinement, based on guarded atomic actions. Latency-insensitive design ensures that a design composed of functionally correct components will be independent of communication latency. A method has been developed which uses Event-B for latency-insensitive SoC component and sub-system design which can be combined with high-level, component synthesis to enable architectural exploration and re-use at the specification level and to close the specification gap in the SoC hardware flow.","abstract_has_math":false,"creators":["Colley, John"],"institution":"University of Southampton","degree_name":"Ph.D.","degree_level":"doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Butler, Michael"],"committee_chairs":[],"committee_members":[],"year":2010,"date_issued":"2010-11","date_published":"2010-11","updated_at":"2026-07-24T04:36:21Z","subjects":[],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":null,"outbound_label":null,"outbound_source":null},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Butler, Michael"]},{"key":"dc:creator","label":"Author","values":["Colley, John"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2010-11"]},{"key":"dc:date.issued","label":"Date","values":["2010-11"]},{"key":"dc:publisher.department","label":"Dc Publisher Department","values":["DSSE (pre 2011 reorg)","School of Electronics and Computer Science"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Southampton"]},{"key":"dc:relation.isreferencedby","label":"Dc Relation Isreferencedby","values":["https://eprints.soton.ac.uk/171695/"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["Ph.D."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://eprints.soton.ac.uk/171695/1/PhDThesisJohnColley.pdf"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["Modern System-on-chip (SoC) hardware design puts considerable pressure on existing design and verification flows, languages and tools. The Register Transfer Level (RTL)description, which forms the input for synchronous, logic synthesis-driven design is at too low a level of abstraction for efficient architectural exploration and re-use. The existing methods for taking a high-level paper specification and refining this specification to an implementation that meets its performance criteria is largely manual and error-prone and as RTL descriptions get larger, a systematic design method is necessary to address explicitly the timing issues that arise when applying logic synthesis to such large blocks.<br/><br/>Guarded Atomic Actions have been shown to offer a convenient notation for describing microarchitectures that is amenable to formal reasoning and high-level synthesis. Event-B is a language and method that supports the development of specifications with automatic proof and refinement, based on guarded atomic actions. Latency-insensitive design ensures that a design composed of functionally correct components will be independent of communication latency. A method has been developed which uses Event-B for latency-insensitive SoC component and sub-system design which can be combined with high-level, component synthesis to enable architectural exploration and re-use at the specification level and to close the specification gap in the SoC hardware flow."]},{"key":"dc:format","label":"Dc Format","values":["text"]},{"key":"dc:title","label":"Title","values":["Guarded atomic actions and refinement in a system-on-chip development flow: bridging the specification gap with Event-B"]}]}],"canonical_facts":{"dc:contributor.advisor":["Butler, Michael"],"dc:creator":["Colley, John"],"dc:date":["2010-11"],"dc:date.issued":["2010-11"],"dc:description.abstract":["Modern System-on-chip (SoC) hardware design puts considerable pressure on existing design and verification flows, languages and tools. The Register Transfer Level (RTL)description, which forms the input for synchronous, logic synthesis-driven design is at too low a level of abstraction for efficient architectural exploration and re-use. The existing methods for taking a high-level paper specification and refining this specification to an implementation that meets its performance criteria is largely manual and error-prone and as RTL descriptions get larger, a systematic design method is necessary to address explicitly the timing issues that arise when applying logic synthesis to such large blocks.<br/><br/>Guarded Atomic Actions have been shown to offer a convenient notation for describing microarchitectures that is amenable to formal reasoning and high-level synthesis. Event-B is a language and method that supports the development of specifications with automatic proof and refinement, based on guarded atomic actions. Latency-insensitive design ensures that a design composed of functionally correct components will be independent of communication latency. A method has been developed which uses Event-B for latency-insensitive SoC component and sub-system design which can be combined with high-level, component synthesis to enable architectural exploration and re-use at the specification level and to close the specification gap in the SoC hardware flow."],"dc:format":["text"],"dc:identifier.uri":["https://eprints.soton.ac.uk/171695/1/PhDThesisJohnColley.pdf"],"dc:publisher.department":["DSSE (pre 2011 reorg)","School of Electronics and Computer Science"],"dc:publisher.institution":["University of Southampton"],"dc:relation.isreferencedby":["https://eprints.soton.ac.uk/171695/"],"dc:title":["Guarded atomic actions and refinement in a system-on-chip development flow: bridging the specification gap with Event-B"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["doctoral"],"dc:type.qualificationname":["Ph.D."]},"updated_at":"2026-07-24T04:36:21Z"}