diff options
| -rw-r--r-- | algorithm.tex | 6 | ||||
| -rw-r--r-- | references.bib | 69 | ||||
| -rw-r--r-- | verilog.tex | 2 |
3 files changed, 58 insertions, 19 deletions
diff --git a/algorithm.tex b/algorithm.tex index fb70bee..4c4c7d4 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -4,6 +4,10 @@ This section covers the main architecture of the HLS tool, and the way in which the back end was added to \compcert{}. This section will also cover an example of converting a simple C program into hardware, expressed in the Verilog language. +First of all, the choice of C for the input language of \vericert{} is because it is the most widely supported language for HLS, and most major HLS tools also use it as an input. As a lot of existing code is also written in C for HLS, supporting C as an input language compared to a custom domain-specific language means that \vericert{} is more practical. Next, Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist. This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog. Verilog was chosen as the output language for \vericert{} because it is one of the most popular hardware description languages and there already exist a few formal semantics for it that could be used as a target~\cite{loow19_verif_compil_verif_proces,meredith10_veril}. + +The framework that was chosen for the frontend was \compcert{}, as it is a mature framework for simulation proofs about intermediate languages, in addition to already providing a validated parser~\cite{jourdan12_valid_lr_parser} from C into the internal representation of Clight. Other frameworks were also considered, such as Vellvm~\cite{zhao12_formal_llvm_inter_repres_verif_progr_trans}, as LLVM IR in particular is often used by HLS tools anyways, however, these would require more work to support a higher level language such as C as input, or even providing a parser for LLVM IR.\@ + \begin{figure} \centering \resizebox{0.47\textwidth}{!}{ @@ -40,7 +44,7 @@ The main work flow of \vericert{} is shown in Figure~\ref{fig:rtlbranch}, which \compcert{} is made up of 11 intermediate languages in between the Clight input and the assembly output. These intermediate languages each serve a different purpose and contain various optimisations. When designing a new back end for \compcert{}, it is crucial to know where to branch off, so as to benefit from all the useful optimisations that \compcert{} performs, but not performing optimisations that are not useful, which include optimisations that are specific to the target CPU architecture or. These optimisations include register allocation, as there is not a fixed number of registers that need to be targeted. -To choose where to branch off at, each intermediate language in \compcert{} can be evaluated to see if it is suitable to be transformed into hardware. Existing HLS compilers often use LLVM IR as an intermediate representation when performing HLS-specific optimisations, as each instruction can be mapped quite well to hardware that performs the same behaviour. Looking at the intermediate languages in \compcert{} shown in Figure~\ref{fig:rtlbranch}, there are many languages to choose from. Clight and CminorSel are an abstract syntax tree (AST) representation of the C code, which does not correspond to a more assembly like language similar to LLVM IR.\@ In addition to that, looking at the languages from LTL to PPC, even though these languages do contain basic blocks, which are desirable when doing HLS, starting from LTL the number of registers is limited +To choose where to branch off at, each intermediate language in \compcert{} can be evaluated to see if it is suitable to be transformed into hardware. Existing HLS compilers often use LLVM IR as an intermediate representation when performing HLS-specific optimisations, as each instruction can be mapped quite well to hardware that performs the same behaviour. Looking at the intermediate languages in \compcert{} shown in Figure~\ref{fig:rtlbranch}, there are many languages to choose from. Clight and CminorSel are an abstract syntax tree (AST) representation of the C code, which does not correspond to a more assembly like language similar to LLVM IR.\@ In addition to that, looking at the languages from LTL to PPC, even though these languages do contain basic blocks, which are desirable when doing HLS, starting from LTL the number of registers is limited. Register allocation limits the number of registers when translating 3AC into LTL, and stores variables on the stack if that is required. This is not needed when performing HLS, as there are many more registers available, and it is preferable to use these instead of RAM whenever possible. \compcert{}'s three-address code (3AC)\footnote{Three-address code (3AC) is also known as register transfer language (RTL) in the \compcert{} literature, however, 3AC is used in this paper instead so as not to confuse it with register-transfer level (RTL), which is another name for the final hardware target of the HLS tool.} is the intermediate language that resembles LLVM IR the most, as it also has an infinite number of pseudo-registers and each instruction maps well to hardware. 3AC is represented as a control flow graph (CFG) in CompCert. Each instruction is a node in the graph and links to the instructions that follow it. This CFG then describes how the computation should proceed, and is a good representation for performing optimisations on as well as local transformations. However, one difference between LLVM IR and 3AC is that 3AC uses operations of the target architecture and performs architecture specific optimisations as well, which is not the case in LLVM IR where all the instructions are quite abstract. This can be mitigated by making \compcert{} target a specific architecture such as x86\_32, where most operations translate quite well into hardware. In addition to that, many optimisations that are also useful for HLS are performed in 3AC, which means that if it is supported as the input language, the HLS algorithm benefits from the same optimisations. It is therefore a good candidate to be chosen as the input language to the HLS back end. The complete flow that \vericert{} takes is show in figure~\ref{fig:rtlbranch}. diff --git a/references.bib b/references.bib index 29bd581..cb7f441 100644 --- a/references.bib +++ b/references.bib @@ -382,19 +382,6 @@ title = {Synthesis and Optimization of Digital Circuits}, year = 1994, publisher = {McGraw-Hill Higher Education}, - abstract = {From the Publisher:Synthesis and Optimization of Digital Circuits offers a - modern, up-to-date look at computer-aided design (CAD) of very large-scale - integration (VLSI) circuits. In particular, this book covers techniques for - synthesis and optimization of digital circuits at the architectural and logic - levels, i.e., the generation of performance-and/or area-optimal circuits - representations from models in hardware description languages. The book provides a - thorough explanation of synthesis and optimization algorithms accompanied by a - sound mathematical formulation and a unified notation. The text covers the - following topics: modern hardware description languages (e.g., VHDL, Verilog); - architectural-level synthesis of data flow and control units, including algorithms - for scheduling and resource binding; combinational logic optimization algorithms - for two-level and multiple-level circuits; sequential logic optimization methods; - and library binding techniques, including those applicable to FPGAs.}, edition = {1st}, isbn = 0070163332, } @@ -469,7 +456,7 @@ @inproceedings{bourgeat20_essen_blues, author = {Bourgeat, Thomas and Pit-Claudel, Cl\'{e}ment and Chlipala, Adam and Arvind}, - title = {The Essence of Bluespec: A Core Language for Rule-Based Hardware Design}, + title = {The Essence of {Bluespec}: A Core Language for Rule-Based Hardware Design}, booktitle = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation}, year = 2020, @@ -487,7 +474,7 @@ @inproceedings{yang11_findin_under_bugs_c_compil, author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John}, - title = {Finding and Understanding Bugs in C Compilers}, + title = {Finding and Understanding Bugs in {C} Compilers}, booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation}, year = 2011, @@ -506,7 +493,7 @@ @inproceedings{blazy05_formal_verif_memor_model_c, author = "Blazy, Sandrine and Leroy, Xavier", - title = "Formal Verification of a Memory Model for C-Like Imperative + title = "Formal Verification of a Memory Model for {C}-Like Imperative Languages", tags = {verification}, booktitle = "Formal Methods and Software Engineering", @@ -520,7 +507,7 @@ @inproceedings{slind08_brief_overv_hol4, author = "Slind, Konrad and Norrish, Michael", - title = "A Brief Overview of HOL4", + title = "A Brief Overview of {HOL4}", booktitle = "Theorem Proving in Higher Order Logics", year = 2008, pages = "28--32", @@ -530,3 +517,51 @@ keywords = {theorem proving;HOL}, publisher = "Springer Berlin Heidelberg", } + +@inproceedings{meredith10_veril, + author = {P. {Meredith} and M. {Katelman} and J. {Meseguer} and + G. {Ro{\c{s}}u}}, + title = {A formal executable semantics of {Verilog}}, + tags = {semantics}, + booktitle = {Eighth ACM/IEEE International Conference on Formal Methods and + Models for Codesign (MEMOCODE 2010)}, + year = 2010, + pages = {179-188}, + doi = {10.1109/MEMCOD.2010.5558634}, + url = {https://doi.org/10.1109/MEMCOD.2010.5558634}, + month = {July} +} + +@inproceedings{jourdan12_valid_lr_parser, + author = "Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and + Leroy, Xavier", + title = "Validating LR(1) Parsers", + booktitle = "Programming Languages and Systems", + year = 2012, + pages = "397--416", + address = "Berlin, Heidelberg", + editor = "Seidl, Helmut", + isbn = "978-3-642-28869-2", + publisher = "Springer Berlin Heidelberg" +} + +@article{zhao12_formal_llvm_inter_repres_verif_progr_trans, + author = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic, + Steve}, + title = {Formalizing the {LLVM} Intermediate Representation for Verified Program + Transformations}, + journal = {SIGPLAN Not.}, + volume = {47}, + number = {1}, + pages = {427-440}, + year = {2012}, + doi = {10.1145/2103621.2103709}, + url = {https://doi.org/10.1145/2103621.2103709}, + address = {New York, NY, USA}, + issn = {0362-1340}, + issue_date = {January 2012}, + keywords = {LLVM, memory safety, Coq}, + month = jan, + numpages = {14}, + publisher = {Association for Computing Machinery}, +} diff --git a/verilog.tex b/verilog.tex index 64e1ee6..95ec74e 100644 --- a/verilog.tex +++ b/verilog.tex @@ -4,7 +4,7 @@ This section describes the Verilog semantics that were chosen for the target language, including the changes that were made to the semantics to be a better fit as an HLS target. -Verilog~\cite{06_ieee_stand_veril_hardw_descr_languag} is a hardware description language commonly used to design hardware. A Verilog design can then be synthesised into logic gates which describes how different gates connect to each other, called a netlist. This representation can then be mapped onto either a field-programmable gate array (FPGA) or turned into an application-specific integrated circuit (ASIC) to implement the design that was described in Verilog. The Verilog standard is quite large, and not all Verilog features are needed to be able to describe hardware. Many Features are only useful for simulation and do not affect the hardware itself. We can therefore restrict the Verilog semantics to the synthesisable subset of Verilog~\cite{05_ieee_stand_veril_regis_trans_level_synth}. In addition to that, HLS dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed. Supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated and synthesised by existing tools and how it is dictated by the standard. +The Verilog standard is quite large, and not all Verilog features are needed to be able to describe hardware. Many Features are only useful for simulation and do not affect the hardware itself. We can therefore restrict the Verilog semantics to the synthesisable subset of Verilog~\cite{05_ieee_stand_veril_regis_trans_level_synth}. In addition to that, HLS dictates which Verilog constructs are generated, meaning the Verilog subset that has to be modelled by the semantics can be reduced even further to only support the constructs that are needed. Supporting a smaller subset in the semantics also means that there is less chance that the standard is misunderstood, and that the semantics actually model how the Verilog is simulated and synthesised by existing tools and how it is dictated by the standard. The Verilog semantics are based on the semantics proposed by \citet{loow19_verif_compil_verif_proces}, which was used to create a formal translation from a logic representation encoded in the HOL4~\cite{slind08_brief_overv_hol4} theorem prover into an equivalent Verilog design. These semantics are quite practical as they restrict themselves to a small subset of Verilog, which can nonetheless be used to model all hardware constructs one would want to design. The main features that are supported by the syntax and semantics are module items, such as variable declarations and always blocks, statements and expressions. As hardware designs normally describe events that will be executed periodically for an infinite amount of time, the top-level of the semantics can be described using small-step semantics, whereas the execution of one small step is then described using big-step semantics. |