國立虎尾科技大學 |

Versatile hardware analysis techniques = from waveform-based analysis to formal verification /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Versatile hardware analysis techniques/ by Lucas Klemmer, Daniel Große.
其他題名:	from waveform-based analysis to formal verification /
作者:	Klemmer, Lucas.
其他作者:	Grosse, Daniel.
出版者:	Cham :Springer Nature Switzerland : : 2025.,
面頁冊數:	xvi, 190 p. :ill., digital ; : 24 cm.;
Contained By:	Springer Nature eBook
標題:	Formal methods (Computer science) -
電子資源:	https://doi.org/10.1007/978-3-031-83093-8
ISBN:	9783031830938

Versatile hardware analysis techniques = from waveform-based analysis to formal verification /
Klemmer, Lucas.

Versatile hardware analysis techniquesfrom waveform-based analysis to formal verification /[electronic resource] :by Lucas Klemmer, Daniel Große. - Cham :Springer Nature Switzerland :2025. - xvi, 190 p. :ill., digital ;24 cm.

Chapter 1 Introduction -- Chapter 2 Background -- Chapter 3 Processor Verification by Equivalent Program Execution -- Chapter 4 A Formally Verified Microcoded RISC-V Platform -- Chapter 5 The Waveform Analysis Language -- Chapter 6 Programmable Analysis of RISC-V Processors using WAL -- Chapter 7 HDL-Integrated Waveform Analysis -- Chapter 8 An Interactive Debugging Methodology Based on WAL -- Chapter 9 Netlist Optimization using Formal Methods under ExternalConstraints -- Chapter 10 Conclusion and Outlook.

This book describes several versatile hardware analysis techniques that tackle existing and new challenges. These techniques cover different phases of the hardware development process, including the verification, debugging, and post-synthesis optimization phases. The authors introduce the Waveform Analysis Language (WAL), which allows users to code analysis tasks in the form of programs that run on waveforms. The book covers processor verification, formal microcode verification, programmable automated waveform analysis demonstrated for a large variety of previously manual analysis tasks, as well as netlist optimization leveraging formal methods. All methods are available as open source, typically include examples on RISC-V analysis problems, providing a strong foundation for the community. Introduces automated waveform analysis based on a DSL to execute programs on waveforms; Includes practical examples for waveform analysis including demonstrations for RISC-V processors; Presents novel approaches for processor verification, microcode verification and netlist optimization with formal methods.

ISBN: 9783031830938

Standard No.: 10.1007/978-3-031-83093-8doiSubjects--Topical Terms:

564790
Formal methods (Computer science)

LC Class. No.: QA76.9.F67

Dewey Class. No.: 004.0151

Versatile hardware analysis techniques = from waveform-based analysis to formal verification /
LDR:02639nam a2200325 a 4500 001 1161205
003 DE-He213
005 20250307115233.0
006 m d
007 cr nn 008maaau
008 251029s2025 sz s 0 eng d
020 $a 9783031830938 $q (electronic bk.)
020 $a 9783031830921 $q (paper)
024 7 $a 10.1007/978-3-031-83093-8 $2 doi
035 $a 978-3-031-83093-8
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.9.F67
072 7 $a TJFC $2 bicssc
072 7 $a TEC008010 $2 bisacsh
072 7 $a TJFC $2 thema
082 0 4 $a 004.0151 $2 23
090 $a QA76.9.F67 $b K64 2025
100 1 $a Klemmer, Lucas. $3 1488205
245 1 0 $a Versatile hardware analysis techniques $h [electronic resource] : $b from waveform-based analysis to formal verification / $c by Lucas Klemmer, Daniel Große.
260 $a Cham : $c 2025. $b Springer Nature Switzerland : $b Imprint: Springer,
300 $a xvi, 190 p. : $b ill., digital ; $c 24 cm.
505 0 $a Chapter 1 Introduction -- Chapter 2 Background -- Chapter 3 Processor Verification by Equivalent Program Execution -- Chapter 4 A Formally Verified Microcoded RISC-V Platform -- Chapter 5 The Waveform Analysis Language -- Chapter 6 Programmable Analysis of RISC-V Processors using WAL -- Chapter 7 HDL-Integrated Waveform Analysis -- Chapter 8 An Interactive Debugging Methodology Based on WAL -- Chapter 9 Netlist Optimization using Formal Methods under ExternalConstraints -- Chapter 10 Conclusion and Outlook.
520 $a This book describes several versatile hardware analysis techniques that tackle existing and new challenges. These techniques cover different phases of the hardware development process, including the verification, debugging, and post-synthesis optimization phases. The authors introduce the Waveform Analysis Language (WAL), which allows users to code analysis tasks in the form of programs that run on waveforms. The book covers processor verification, formal microcode verification, programmable automated waveform analysis demonstrated for a large variety of previously manual analysis tasks, as well as netlist optimization leveraging formal methods. All methods are available as open source, typically include examples on RISC-V analysis problems, providing a strong foundation for the community. Introduces automated waveform analysis based on a DSL to execute programs on waveforms; Includes practical examples for waveform analysis including demonstrations for RISC-V processors; Presents novel approaches for processor verification, microcode verification and netlist optimization with formal methods.
650 0 $a Formal methods (Computer science) $3 564790
650 0 $a RISC microprocessors. $3 655517
650 1 4 $a Electronics Design and Verification. $3 1387809
650 2 4 $a Embedded Systems. $3 1026431
650 2 4 $a Logic Design. $3 670915
700 1 $a Grosse, Daniel. $3 1488206
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer Nature eBook
856 4 0 $u https://doi.org/10.1007/978-3-031-83093-8
950 $a Engineering (SpringerNature-11647)