{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/150194"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/150194","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Specification and verification of sequential machines in rule-based hardware languages","abstract":"The design of correct hardware is an important concern in the age of information, where more and more companies are designing chips tailored to their workloads. This raises two well-known problems: how to specify what is a correct design, and, once the notion of correctness is set, how to prove that a given design is correct. Standard practice relies on a mix of techniques. It uses testing to run concrete scenarios to verify a concrete property: “this specific test passed,” but this gives only weak overall correctness guarantees. The other technique is to use hardware formal verification, which phrases correctness as custom temporal-logic formulae and checks that a concrete design verifies those properties by solving a large set of corresponding Boolean equations. This thesis addresses the hardware-verification question from a different angle: we intend to mechanically formalize the specifications and correctness arguments that architects make in their minds when they design machines, and we encode them in an interactive theorem prover. For this, we address three challenges: (1) We build an expressive framework in which we can express both synthesizable designs and abstract specifications, and we connect and navigate between them in the proof assistant. (2) We enforce several strict language restrictions, allowing us to side-step previous difficulties in specifications and proofs. (3) After acknowledging that we need a modular methodology to keep the verification effort under control, we showcase previously ignored difficulties in specifying complex sequential machines modularly. We introduce generalized specifications and develop various proof techniques to prove that concrete designs are instances of their modular specifications. We finally apply our methodology to prove modularly the correctness of a family of pipelined processors, independently of its memory.","abstract_html":"The design of correct hardware is an important concern in the age of information, where more and more companies are designing chips tailored to their workloads. This raises two well-known problems: how to specify what is a correct design, and, once the notion of correctness is set, how to prove that a given design is correct. Standard practice relies on a mix of techniques. It uses testing to run concrete scenarios to verify a concrete property: “this specific test passed,” but this gives only weak overall correctness guarantees. The other technique is to use hardware formal verification, which phrases correctness as custom temporal-logic formulae and checks that a concrete design verifies those properties by solving a large set of corresponding Boolean equations. This thesis addresses the hardware-verification question from a different angle: we intend to mechanically formalize the specifications and correctness arguments that architects make in their minds when they design machines, and we encode them in an interactive theorem prover. For this, we address three challenges: (1) We build an expressive framework in which we can express both synthesizable designs and abstract specifications, and we connect and navigate between them in the proof assistant. (2) We enforce several strict language restrictions, allowing us to side-step previous difficulties in specifications and proofs. (3) After acknowledging that we need a modular methodology to keep the verification effort under control, we showcase previously ignored difficulties in specifying complex sequential machines modularly. We introduce generalized specifications and develop various proof techniques to prove that concrete designs are instances of their modular specifications. We finally apply our methodology to prove modularly the correctness of a family of pipelined processors, independently of its memory.","abstract_has_math":false,"creators":["Bourgeat, Thomas"],"institution":"Massachusetts Institute of Technology","degree_name":"Doctoral","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Arvind","Chlipala, Adam"],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023-02","date_published":"2023-02","updated_at":"2026-07-22T22:22:13Z","subjects":[],"languages":[],"rights":["In Copyright - Educational Use Permitted","Copyright MIT"],"rights_urls":["http://rightsstatements.org/page/InC-EDU/1.0/"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/150194","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Arvind","Chlipala, Adam"]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"]},{"key":"dc:creator","label":"Author","values":["Bourgeat, Thomas"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2023-03-31T14:38:50Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2023-03-31T14:38:50Z"]},{"key":"dc:date.issued","label":"Date","values":["2023-02"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctoral","Doctor of Philosophy"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright - Educational Use Permitted","Copyright MIT"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/page/InC-EDU/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/150194"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["The design of correct hardware is an important concern in the age of information, where more and more companies are designing chips tailored to their workloads. This raises two well-known problems: how to specify what is a correct design, and, once the notion of correctness is set, how to prove that a given design is correct. Standard practice relies on a mix of techniques. It uses testing to run concrete scenarios to verify a concrete property: “this specific test passed,” but this gives only weak overall correctness guarantees. The other technique is to use hardware formal verification, which phrases correctness as custom temporal-logic formulae and checks that a concrete design verifies those properties by solving a large set of corresponding Boolean equations. This thesis addresses the hardware-verification question from a different angle: we intend to mechanically formalize the specifications and correctness arguments that architects make in their minds when they design machines, and we encode them in an interactive theorem prover. For this, we address three challenges: (1) We build an expressive framework in which we can express both synthesizable designs and abstract specifications, and we connect and navigate between them in the proof assistant. (2) We enforce several strict language restrictions, allowing us to side-step previous difficulties in specifications and proofs. (3) After acknowledging that we need a modular methodology to keep the verification effort under control, we showcase previously ignored difficulties in specifying complex sequential machines modularly. We introduce generalized specifications and develop various proof techniques to prove that concrete designs are instances of their modular specifications. We finally apply our methodology to prove modularly the correctness of a family of pipelined processors, independently of its memory."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["Ph.D."]},{"key":"dc:title","label":"Title","values":["Specification and verification of sequential machines in rule-based hardware languages"]}]}],"canonical_facts":{"dc:contributor.advisor":["Arvind","Chlipala, Adam"],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"],"dc:creator":["Bourgeat, Thomas"],"dc:date.accessioned":["2023-03-31T14:38:50Z"],"dc:date.available":["2023-03-31T14:38:50Z"],"dc:date.issued":["2023-02"],"dc:description.abstract":["The design of correct hardware is an important concern in the age of information, where more and more companies are designing chips tailored to their workloads. This raises two well-known problems: how to specify what is a correct design, and, once the notion of correctness is set, how to prove that a given design is correct. Standard practice relies on a mix of techniques. It uses testing to run concrete scenarios to verify a concrete property: “this specific test passed,” but this gives only weak overall correctness guarantees. The other technique is to use hardware formal verification, which phrases correctness as custom temporal-logic formulae and checks that a concrete design verifies those properties by solving a large set of corresponding Boolean equations. This thesis addresses the hardware-verification question from a different angle: we intend to mechanically formalize the specifications and correctness arguments that architects make in their minds when they design machines, and we encode them in an interactive theorem prover. For this, we address three challenges: (1) We build an expressive framework in which we can express both synthesizable designs and abstract specifications, and we connect and navigate between them in the proof assistant. (2) We enforce several strict language restrictions, allowing us to side-step previous difficulties in specifications and proofs. (3) After acknowledging that we need a modular methodology to keep the verification effort under control, we showcase previously ignored difficulties in specifying complex sequential machines modularly. We introduce generalized specifications and develop various proof techniques to prove that concrete designs are instances of their modular specifications. We finally apply our methodology to prove modularly the correctness of a family of pipelined processors, independently of its memory."],"dc:description.degree":["Ph.D."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/150194"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["In Copyright - Educational Use Permitted","Copyright MIT"],"dc:rights.uri":["http://rightsstatements.org/page/InC-EDU/1.0/"],"dc:title":["Specification and verification of sequential machines in rule-based hardware languages"],"dc:type":["Thesis"],"thesis:degree_name":["Doctoral","Doctor of Philosophy"]},"updated_at":"2026-07-22T22:22:13Z"}