{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/24159"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/24159","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Goldmine: An integration of data mining and static analysis for automatic generation of hardware assertions","abstract":"\"We present GoldMine, a methodology for generating assertions automatically. Our method involves a combination of data mining and static analysis of the Register Transfer Level (RTL) design. The RTL design is first simulated to generate data about the design’s dynamic behavior. The generated data is then mined for \"\"candidate assertions\"\" that are likely to be invariants. We present both a decision tree supervised learning algorithm as well as a coverage guided mining algorithm for generating high-quality assertions. These candidate assertions are then passed through a formal verification engine to filter out the spurious candidates. The assertions that are attested as true by the formal engine are system invariants. These are then evaluated by a process of designer ranking that is provided as feedback to the data mining engine. We present results of using GoldMine for assertion generation of the RTL of Sun’s OpenSparc T2 many-threaded processor. Our results show that GoldMine can generate complex, high-coverage assertions in RTL, thereby minimizing human effort in this process.\"","abstract_html":""We present GoldMine, a methodology for generating assertions automatically. Our method involves a combination of data mining and static analysis of the Register Transfer Level (RTL) design. The RTL design is first simulated to generate data about the design’s dynamic behavior. The generated data is then mined for ""candidate assertions"" that are likely to be invariants. We present both a decision tree supervised learning algorithm as well as a coverage guided mining algorithm for generating high-quality assertions. These candidate assertions are then passed through a formal verification engine to filter out the spurious candidates. The assertions that are attested as true by the formal engine are system invariants. These are then evaluated by a process of designer ranking that is provided as feedback to the data mining engine. We present results of using GoldMine for assertion generation of the RTL of Sun’s OpenSparc T2 many-threaded processor. Our results show that GoldMine can generate complex, high-coverage assertions in RTL, thereby minimizing human effort in this process."","abstract_has_math":false,"creators":["Sheridan, David"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Vasudevan, Shobha"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-05-25T15:04:06Z","date_published":"2011-05-25T15:04:06Z","updated_at":"2026-07-22T22:25:23Z","subjects":["GoldMine","assertion","generation","automatic","integration","static analysis","data mining","dynamic analysis","decision tree","association mining","coverage guided mining","OpenSparc","invariant","simulation","Register Transfer Level (RTL)","Hardware","design"],"languages":["en"],"rights":["Copyright 2011 David Sheridan"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/24159","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Vasudevan, Shobha"]},{"key":"dc:creator","label":"Author","values":["Sheridan, David"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-05-25T15:04:06Z","2011-05"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["GoldMine","assertion","generation","automatic","integration","static analysis","data mining","dynamic analysis","decision tree","association mining","coverage guided mining","OpenSparc","invariant","simulation","Register Transfer Level (RTL)","Hardware","design"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2011 David Sheridan"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/24159"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["\"We present GoldMine, a methodology for generating assertions automatically. Our method involves a combination of data mining and static analysis of the Register Transfer Level (RTL) design. The RTL design is first simulated to generate data about the design’s dynamic behavior. The generated data is then mined for \"\"candidate assertions\"\" that are likely to be invariants. We present both a decision tree supervised learning algorithm as well as a coverage guided mining algorithm for generating high-quality assertions. These candidate assertions are then passed through a formal verification engine to filter out the spurious candidates. The assertions that are attested as true by the formal engine are system invariants. These are then evaluated by a process of designer ranking that is provided as feedback to the data mining engine. We present results of using GoldMine for assertion generation of the RTL of Sun’s OpenSparc T2 many-threaded processor. Our results show that GoldMine can generate complex, high-coverage assertions in RTL, thereby minimizing human effort in this process.\"","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-04-27T00:42:51Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 Sheridan_David.tar.bz2: 1051644 bytes, checksum: 1f2e9ce856ea70ae982583bc9aa3cad6 (MD5) Sheridan_David.pdf: 1432634 bytes, checksum: b1631942172c83f9183998310ef22231 (MD5)","Made available in DSpace on 2011-05-25T15:04:06Z (GMT). No. of bitstreams: 3 Sheridan_David.pdf: 1432634 bytes, checksum: b1631942172c83f9183998310ef22231 (MD5) license.txt: 4064 bytes, checksum: 007d6ce4793f2a0ccfca8e8eedd8b631 (MD5) Sheridan_David.tar.bz2: 1051644 bytes, checksum: 1f2e9ce856ea70ae982583bc9aa3cad6 (MD5)"]},{"key":"dc:title","label":"Title","values":["Goldmine: An integration of data mining and static analysis for automatic generation of hardware assertions"]}]}],"canonical_facts":{"dc:contributor":["Vasudevan, Shobha"],"dc:creator":["Sheridan, David"],"dc:date":["2011-05-25T15:04:06Z","2011-05"],"dc:description":["\"We present GoldMine, a methodology for generating assertions automatically. Our method involves a combination of data mining and static analysis of the Register Transfer Level (RTL) design. The RTL design is first simulated to generate data about the design’s dynamic behavior. The generated data is then mined for \"\"candidate assertions\"\" that are likely to be invariants. We present both a decision tree supervised learning algorithm as well as a coverage guided mining algorithm for generating high-quality assertions. These candidate assertions are then passed through a formal verification engine to filter out the spurious candidates. The assertions that are attested as true by the formal engine are system invariants. These are then evaluated by a process of designer ranking that is provided as feedback to the data mining engine. We present results of using GoldMine for assertion generation of the RTL of Sun’s OpenSparc T2 many-threaded processor. Our results show that GoldMine can generate complex, high-coverage assertions in RTL, thereby minimizing human effort in this process.\"","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-04-27T00:42:51Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 Sheridan_David.tar.bz2: 1051644 bytes, checksum: 1f2e9ce856ea70ae982583bc9aa3cad6 (MD5) Sheridan_David.pdf: 1432634 bytes, checksum: b1631942172c83f9183998310ef22231 (MD5)","Made available in DSpace on 2011-05-25T15:04:06Z (GMT). No. of bitstreams: 3 Sheridan_David.pdf: 1432634 bytes, checksum: b1631942172c83f9183998310ef22231 (MD5) license.txt: 4064 bytes, checksum: 007d6ce4793f2a0ccfca8e8eedd8b631 (MD5) Sheridan_David.tar.bz2: 1051644 bytes, checksum: 1f2e9ce856ea70ae982583bc9aa3cad6 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/24159"],"dc:language":["en"],"dc:rights":["Copyright 2011 David Sheridan"],"dc:subject":["GoldMine","assertion","generation","automatic","integration","static analysis","data mining","dynamic analysis","decision tree","association mining","coverage guided mining","OpenSparc","invariant","simulation","Register Transfer Level (RTL)","Hardware","design"],"dc:title":["Goldmine: An integration of data mining and static analysis for automatic generation of hardware assertions"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:23Z"}