東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

A Type-Safe Hdl Verified in Coq /

Tavante, Hanneli Carolina Andreazzi,

Linked to FindBook

Google Book

Amazon

博客來

A Type-Safe Hdl Verified in Coq /

Record Type:	Electronic resources : Monograph/item
Title/Author:	A Type-Safe Hdl Verified in Coq // Hanneli Carolina Andreazzi Tavante.
Author:	Tavante, Hanneli Carolina Andreazzi,
Description:	1 electronic resource (104 pages)
Notes:	Source: Masters Abstracts International, Volume: 85-01.
Contained By:	Masters Abstracts International85-01.
Subject:	Calculus. -
Online resource:	https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30548896
ISBN:	9798379861988

A Type-Safe Hdl Verified in Coq /
Tavante, Hanneli Carolina Andreazzi,

A Type-Safe Hdl Verified in Coq /Hanneli Carolina Andreazzi Tavante. - 1 electronic resource (104 pages)

Source: Masters Abstracts International, Volume: 85-01.

Hardware Description Languages (HDL), such as VHDL and Verilog, simplify the circuit specifcation, simulation, and synthesis by enabling different types of abstractions. Hardware verifcation pipelines reduce design faults caused by erroneous transformations of a design specifcation into the layout description. However, there is little work on the language aspect of Verilog itself, and designers tend to trust the language as a source of truth. Unfortunately, unverifed languages may be unreliable and lead to circuit design faults. For instance, in Verilog, values can be converted automatically from one type to another when the context of use requires it, generating undesired bugs due to the automatic conversion.In this thesis, we address the need for a verifed, type-safe language that can rule out undesired faults in hardware projects occasioned by language issues. We present Verifoq,a strongly typed HDL based on a subset of the original Verilog language.Verifoq is developed in the Coq proof assistant, and uses the Simply-Typed Lambda Calculus (STLC) as its core foundation. We develop a fexible small-step operational semantics for our language, and combined with its set of typing rules, we prove that Verifoqis a type-safe language.We also provide several use cases for Verifoq,including a composed verifcation pipeline with Hoare Logic and a multi-staged hardware verifcation pipeline. Finally, we also present possible integration scenarios for High-Level Synthesis applications.

English

ISBN: 9798379861988Subjects--Topical Terms:

517463
Calculus.

A Type-Safe Hdl Verified in Coq /
LDR:04748nmm a22004333i 4500 001 2430307
005 20250519115938.5
006 m o d
007 cr|nu||||||||
008 261011s2023 miu||||||m |||||||eng d
020 $a 9798379861988
035 $a (MiAaPQD)AAI30548896
035 $a (MiAaPQD)McGill_jm214v69x
035 $a AAI30548896
040 $a MiAaPQD $b eng $c MiAaPQD $e rda
100 1 $a Tavante, Hanneli Carolina Andreazzi, $e author. $3 3818561
245 1 2 $a A Type-Safe Hdl Verified in Coq / $c Hanneli Carolina Andreazzi Tavante.
264 1 $a Ann Arbor : $b ProQuest Dissertations & Theses, $c 2023
300 $a 1 electronic resource (104 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Masters Abstracts International, Volume: 85-01.
500 $a Advisors: Maheswaran, Muthucumaru; Zilic, Zeljko.
502 $b M.Sc. $c McGill University (Canada) $d 2023.
520 $a Hardware Description Languages (HDL), such as VHDL and Verilog, simplify the circuit specifcation, simulation, and synthesis by enabling different types of abstractions. Hardware verifcation pipelines reduce design faults caused by erroneous transformations of a design specifcation into the layout description. However, there is little work on the language aspect of Verilog itself, and designers tend to trust the language as a source of truth. Unfortunately, unverifed languages may be unreliable and lead to circuit design faults. For instance, in Verilog, values can be converted automatically from one type to another when the context of use requires it, generating undesired bugs due to the automatic conversion.In this thesis, we address the need for a verifed, type-safe language that can rule out undesired faults in hardware projects occasioned by language issues. We present Verifoq,a strongly typed HDL based on a subset of the original Verilog language.Verifoq is developed in the Coq proof assistant, and uses the Simply-Typed Lambda Calculus (STLC) as its core foundation. We develop a fexible small-step operational semantics for our language, and combined with its set of typing rules, we prove that Verifoqis a type-safe language.We also provide several use cases for Verifoq,including a composed verifcation pipeline with Hoare Logic and a multi-staged hardware verifcation pipeline. Finally, we also present possible integration scenarios for High-Level Synthesis applications.
520 $a Les langages de description materielle (en anglais, Hardware Description languages, ou les HDL), tels que le VHDL et le Verilog, simplifent la specifcation, la simulation et la synthese des circuits en permettant differents types d'abstractions. Les pipelines de verifcation materielle reduisent les defauts de conception causes par des transformations erronees d'une specifcation de conception en description de mise en page. Cependant, il y a peu de travail sur l'aspect langage du Verilog lui-meme, et les concepteurs ont tendance a faire confance au langage comme source de verite. Malheureusement, les langages non verifes peuvent ne pas etre fables et conduire a des defauts de conception de circuit. Par exemple, dans le Verilog, les valeurs peuvent etre converties automatiquement d'un type a un autre lorsque le contexte d'utilisation l'exige, generant des bogues indesirables dus a la conversion automatique.Dans cette these, nous abordons le besoin d'un langage verife et de type securise qui peut exclure les defauts indesirables dans les projets materiels occasionnes par des problemes de langage. Nous presentons Verifoq,une HDL fortement type base sur un sous-ensemble du langage Verilog original.Verifoq est developpe dans l'assistant de preuve Coq et utilise le calcul lambda simplement type (en anglais, Simply-Typed Lambda Calculus, ou le STLC) comme base de base. Nous developpons une semantique operationnelle fexible a petits pas pour notre langage, et combinee avec son ensemble de regles de typage, nous prouvons que Verifoqest un langage de type securise.Nous fournissons egalement plusieurs cas d'utilisation pour Verifoq,y compris un pipeline de verifcation compose avec le Hoare Logic et un pipeline de verifcation materielle en plusieurs etapes. Pour terminer, nous presentons egalement des scenarios d'integration possibles pour les applications de synthese de haut niveau.
546 $a English
590 $a School code: 0781
650 4 $a Calculus. $3 517463
650 4 $a Behavior. $3 532476
650 4 $a Programming languages. $3 3683658
650 4 $a Syntax. $3 897045
650 4 $a Temporal logic. $3 3681666
650 4 $a C plus plus. $3 3687413
650 4 $a Boolean. $3 3683493
650 4 $a Circuits. $3 3555093
650 4 $a Design specifications. $3 3683440
650 4 $a Theorems. $3 3686073
650 4 $a Semantics. $3 520060
650 4 $a Computer science. $3 523869
650 4 $a Design. $3 518875
650 4 $a Electrical engineering. $3 649834
650 4 $a Logic. $3 529544
650 4 $a Mathematics. $3 515831
690 $a 0984
690 $a 0389
690 $a 0544
690 $a 0395
690 $a 0405
710 2 $a McGill University (Canada). $e degree granting institution. $3 3759190
720 1 $a Maheswaran, Muthucumaru $e degree supervisor.
720 1 $a Zilic, Zeljko $e degree supervisor.
773 0 $t Masters Abstracts International $g 85-01.
790 $a 0781
791 $a M.Sc.
792 $a 2023
856 4 0 $u https://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30548896