From bea851a5e36f46e79036f58633cc45916b53acee Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 10 Sep 2021 19:24:42 +0100 Subject: Update content --- config.toml | 1 + content.org | 193 +++++++++++++++++++++++++++++++-------------------------- data/news.toml | 2 +- 3 files changed, 106 insertions(+), 90 deletions(-) diff --git a/config.toml b/config.toml index ff7d97d..2ec5b6d 100644 --- a/config.toml +++ b/config.toml @@ -6,6 +6,7 @@ theme = "ymherklotz" [params] description = "Welcome to my blog! I am a final year student studying Electronic and Information Engineering at Imperial College London." katex = true + offen = true [markup.goldmark.renderer] unsafe = true diff --git a/content.org b/content.org index 0637ffd..b64392f 100644 --- a/content.org +++ b/content.org @@ -25,6 +25,53 @@ I have also worked on random testing for FPGA synthesis tools. [Verismith](https Here you can find all my previous posts: +** Vericert :coq:hardware:FPGA:verilog: +:PROPERTIES: +:EXPORT_DATE: 2021-09-07 +:EXPORT_FILE_NAME: 2021-09-07-vericert +:EXPORT_HUGO_SECTION: blog +:EXPORT_HUGO_CUSTOM_FRONT_MATTER: :summary "Vericert is a formally verified high-level synthesis tool, translating C code into a hardware design expressed in Verilog." +:CUSTOM_ID: vericert +:END: + +Compilers are increasingly being relied upon to produce binaries from code without introducing any +bugs in the process. Therefore, formally verified compilers like [[https://compcert.org][CompCert]] were introduced to +formally prove that the compilation process does not change the behaviour of the program. This +allowed companies like Airbus to move critical code from pure assembly to C. + +Similarly, the hardware industry in general mainly uses hardware description languages, such as +Verilog or VHDL, to design their hardware, which can then either be placed on an FPGA for quick +testing, or eventually turned into an ASIC. As there are many commercial tools available for the +verification of HDLs, designers prefer to have full control over the hardware and therefore use the +HDL directly. Alternatives exist, such as high-level synthesis tools (HLS), or higher-level +hardware description languages. + +So why not use higher-level HDLs then? They seem to solve all the problems that current HDLs face. +Well, the adoption is hindered by the fact that even though it seems like the perfect solution to +have a new language dedicated to hardware design that provides a higher-level of abstraction than +existing HDLs, the fact is that the syntax and semantics of such a language often change drastically +compared to the existing HDLs which everyone is familiar with. It is already the case that there is +a shortage of hardware designers, and it is therefore even more unlikely that these hardware +designers would know an alternative hardware design language. + +HLS, on the other hand, tackles the problem from a different perspective, and instead ideally aims +to bring hardware design to the software designer. This is achieved by compiling a subset of valid +software programs directly into hardware, therefore making it much easier to get started with +hardware design and write algorithms in hardware. This not only brings hardware design to a larger +number of people, but also brings all the benefits of the software ecosystem to verify the hardware +designs and algorithms. The following sections will describe the benefits and drawbacks of HLS in +more detail, as well as why one would even consider having to formally verify the translation as +well. + +*** A bit about HLS + +*** How do we formally verify it? + +*** Useful links + +- [[https://yannherklotz.com/papers/fvhls_oopsla21.pdf][OOPSLA'21 paper]] to appear. +- [[https://github.com/ymherklotz/vericert][Github repository]]. +- [[https://vericert.ymhg.org][Vericert documentation website]]. ** Introduction to Luhmann's Zettelkasten :writing:emacs: :PROPERTIES: :EXPORT_DATE: 2020-12-21 @@ -41,33 +88,6 @@ notes. This post will describe the general note-taking workflow that Luhmann use implementation of the Zettelkasten in Emacs' built-in [[https://orgmode.org/][=org-mode=]], which I have been using regularly for my notes and has been working well. -#+begin_html - -#+end_html - -*Table of Contents* - -- [[#zettelkasten-compared-to-other-note-taking-solutions][Zettelkasten - compared to other note-taking solutions]] -- [[#general-setup][General setup]] -- [[#inserting-new-notes][Inserting new notes]] - - - [[#permanent-notes][Permanent notes]] - - [[#index-notes][Index notes]] - -- [[#keeping-track-of-references][Keeping track of references]] -- [[#emacs-implementation][Emacs implementation]] - - - [[#linking-to-other-notes][Linking to other notes]] - - [[#some-automation-for-id-creation][Some automation for ID - creation]] - -- [[#conclusion][Conclusion]] - -#+begin_html - -#+end_html - *** Zettelkasten compared to other note-taking solutions :PROPERTIES: :CUSTOM_ID: zettelkasten-compared-to-other-note-taking-solutions @@ -236,13 +256,13 @@ need is one which generates an ID for us. We'll need two functions, one which in ID, and one which will branch off of the current ID and create a parallel one. We can therefore first create a simple =ymhg/incr-id= function which simply increments the last character of the ID. -#+begin_example +#+begin_src emacs-lisp (defun ymhg/incr-id (ident) (let* ((ident-list (append nil ident nil)) (last-ident (last ident-list))) (setcar last-ident (+ (car last-ident) 1)) (concat ident-list))) -#+end_example +#+end_src However, one problem is that if we get to an ID with a =9= at the end, it will wrap around and generate a =0= at the end, followed by then generating an =a=, which will break the naming scheme. This @@ -252,12 +272,12 @@ assume that manual intervention will be required sometimes. Then, to create the generates an ID branching off of the current one, we just have to check if the current id ends with a number or a character, and add a =a= or =1= accordingly. -#+begin_example +#+begin_src emacs-lisp (defun ymhg/branch-id (ident) (if (string-match-p ".*[0-9]$" ident) (concat ident "a") (concat ident "1"))) -#+end_example +#+end_src Finally, we just need functions that create a new headline underneath the current one, with the correct level and the correct ID. To do this, we first need two functions, one which creates a new @@ -268,31 +288,31 @@ these functions are extremely similar, the only differences being what heading t increment the ID, we can create a general function that will get an ID, increment it and then generate a new heading somehow using that ID. -#+begin_example +#+begin_src emacs-lisp (defun ymhg/org-zettelkasten-create (incr newheading) (let* ((current-id (org-entry-get nil "CUSTOM_ID")) (next-id (funcall incr current-id))) (funcall newheading) (org-set-property "CUSTOM_ID" next-id))) -#+end_example +#+end_src Using that general function, we can then first create the function that will insert a heading at the same level as the previous heading and increments the last value of the ID. -#+begin_example +#+begin_src emacs-lisp (defun org-zettelkasten-create-heading () (ymhg/org-zettelkasten-create 'ymhg/incr-id 'org-insert-heading)) -#+end_example +#+end_src Then we create the function that will increment the ID by adding an =a= or =1= after the ID, and inserts a sub-heading. -#+begin_example +#+begin_src emacs-lisp (defun org-zettelkasten-create-subheading () (ymhg/org-zettelkasten-create 'ymhg/branch-id '(lambda () (org-insert-subheading "")))) -#+end_example +#+end_src For the final part of automation, we can then create a function that will correctly use the =create-next= and =create-branch= function depending on the current location of the cursor. To see which @@ -302,7 +322,7 @@ same level using =org-forward-heading-same-level=. If these are at different loc that there is a next heading on the same level, which means that we need to branch off of the current one. If we are still in the same location, then we can create a new note at the same level. -#+begin_example +#+begin_src emacs-lisp (defun org-zettelkasten-create-dwim () (interactive) (let ((current-point (save-excursion @@ -314,14 +334,14 @@ current one. If we are still in the same location, then we can create a new note (if (= current-point next-point) (org-zettelkasten-create-heading) (org-zettelkasten-create-subheading)))) -#+end_example +#+end_src Finally, we can then add the =create-dwim= function to our keybinding map and we're ready to create as many notes as possible. -#+begin_example +#+begin_src emacs-lisp (define-key org-mode-map (kbd "C-c y n") #'org-zettelkasten-create-dwim) -#+end_example +#+end_src *** Conclusion :PROPERTIES: @@ -432,23 +452,23 @@ with. Just like many other functional languages, Nix has =let= expressions which bind an expression to a name. -#+begin_example +#+begin_src emacs-lisp let name = expr; in body -#+end_example +#+end_src It also supports importing an expression, which just evaluates and inserts an expression. -#+begin_example +#+begin_src emacs-lisp import ./expression.nix; -#+end_example +#+end_src The =with= expression is also interesting, which makes all the attributes of a set available in the next expression, unqualified. -#+begin_example +#+begin_src emacs-lisp with set; expr -#+end_example +#+end_src There are many other useful constructs such as recursive sets (allows you to refer to keys from the set inside the set), inheriting (copy the @@ -488,7 +508,7 @@ of the source code (=src=). These are the only two required attributes for the =mkDerivation= function, however, that does not mean it will build yet. -#+begin_example +#+begin_src emacs-lisp with import {}; stdenv.mkDerivation { @@ -500,7 +520,7 @@ build yet. url = "https://github.com/vellvm/vellvm"; }; } -#+end_example +#+end_src To actually get it to build, there are a few attributes that we need to specify in addition to those. The first is customise the build step @@ -509,11 +529,11 @@ execute =make=, however, in this project the =makefile= is actually in the =src= directory. We therefore have to change to that directory first before we can do anything. -#+begin_example +#+begin_src emacs-lisp buildPhase = '' cd src && make ''; -#+end_example +#+end_src This will now execute the makefile correctly, however, it will fail the build because =Vellvm= has a few dependencies that need to be installed @@ -523,25 +543,25 @@ Coq dependencies using =coqPackages=, OCaml dependencies using =ocamlPackages=, and finally command line tools such as the OCaml compiler or the OCaml build system =dune=. -#+begin_example +#+begin_src emacs-lisp buildInputs = [ git coq ocamlPackages.menhir dune coqPackages.flocq coqPackages.coq-ext-lib coqPackages.paco coqPackages.ceres ocaml ]; -#+end_example +#+end_src Finally, Nix will execute =make install= automatically at the end to install the program correctly. In this case, we need to set the =COQLIB= flag so that it knows where to place the compiled Coq theories. These can be set using the =installFlags= attribute. -#+begin_example +#+begin_src emacs-lisp installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; -#+end_example +#+end_src We then have the following Nix derivation which should download =Vellvm= and build it correctly. -#+begin_example +#+begin_src emacs-lisp with import {}; stdenv.mkDerivation { @@ -559,7 +579,7 @@ and build it correctly. installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; } -#+end_example +#+end_src However, one last problem we'll have is that =coqPackages.ceres= does not actually exist in =coqPackages=, we were a bit too optimistic. To @@ -573,7 +593,7 @@ and that derivations using this package will also need. In this case, any derivation using =ceres= will need Coq, otherwise it would not be useful. -#+begin_example +#+begin_src emacs-lisp ceres = stdenv.mkDerivation { name = "coq${coq.coq-version}-ceres"; @@ -585,7 +605,7 @@ useful. installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; }; -#+end_example +#+end_src Finally, we can use a =let= expression to insert it as a dependency into our own derivation. We now have a complete nix expression that will @@ -595,7 +615,7 @@ always build =Vellvm= correctly in a containerised manner. nix-prefetch-url --unpack https://github.com/Lysxia/coq-ceres/archive/4e682cf97ec0006a9d5b3f98e648e5d69206b614.tar.gz #+end_src -#+begin_example +#+begin_src emacs-lisp with import {}; let @@ -636,7 +656,7 @@ always build =Vellvm= correctly in a containerised manner. installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; } -#+end_example +#+end_src If one saves the file in =default.nix=, one can then build the nix expression using the =nix-build= command. This should return a binary @@ -678,8 +698,7 @@ also thank all the organisers of the workshop. Four microsoft projects were presented, with the main themes being custom hardware and optical electronics. -**** [[https://www.microsoft.com/en-us/research/project/honeycomb/][Honeycomb]]: -Hardware Offloads for Distributed Systems +**** [[https://www.microsoft.com/en-us/research/project/honeycomb/][Honeycomb]]: Hardware Offloads for Distributed Systems :PROPERTIES: :CUSTOM_ID: honeycomb-hardware-offloads-for-distributed-systems :END: @@ -703,8 +722,7 @@ layer can be customised and reworked for that specific use case. Even the data structure can be optimised for the FPGA so that it becomes extremely fast to traverse the data and find it's location. -**** [[https://www.microsoft.com/en-us/research/project/project-silica/][Silica]]: -Optical Storage +**** [[https://www.microsoft.com/en-us/research/project/project-silica/][Silica]]: Optical Storage :PROPERTIES: :CUSTOM_ID: silica-optical-storage :END: @@ -733,12 +751,10 @@ a femtosecond laser, which can then be read back using LEDs. The deformities have different properties such as angle and phase which dictate the current value at that location. -#+caption: Project silica: image of 1978 "Superman" movie encoded on -silica glass. Photo by Jonathan Banks for Microsoft. +#+caption: Project silica: image of 1978 "Superman" movie encoded on silica glass. Photo by Jonathan Banks for Microsoft. [[/images/msr_research/project_silica.jpg]] -**** [[https://www.microsoft.com/en-us/research/project/sirius/][Sirius]]: -Optical Data Center Networks +**** [[https://www.microsoft.com/en-us/research/project/sirius/][Sirius]]: Optical Data Center Networks :PROPERTIES: :CUSTOM_ID: sirius-optical-data-center-networks :END: @@ -752,8 +768,7 @@ Instead, one can switch on the incoming light directly using optical switches, which reduce the switching latency to a few nanoseconds. This makes it possible to have fully optical data-centers. -**** [[https://www.microsoft.com/en-us/research/project/iris/][Iris]]: -Optical Regional Networks +**** [[https://www.microsoft.com/en-us/research/project/iris/][Iris]]: Optical Regional Networks :PROPERTIES: :CUSTOM_ID: iris-optical-regional-networks :END: @@ -1019,7 +1034,7 @@ of posts, which are called *collections* in Jekyll. My layout, which supports project descriptions for a portfolio and blog posts, looks like the following. -#+begin_example +#+begin_src emacs-lisp . ├── assets │   ├── css @@ -1032,7 +1047,7 @@ posts, looks like the following. ├── _layouts ├── _portfolio └── _posts -#+end_example +#+end_src *** Portfolio Collection :PROPERTIES: @@ -1041,22 +1056,22 @@ posts, looks like the following. To make Jekyll recognise the =_portfolio= directory, it has to be declared in Jekyll's configuration file =_config.yml=. -#+begin_example +#+begin_src emacs-lisp collections: portfolio: output: true -#+end_example +#+end_src Jekyll will now parse and turn the markdown files into HTML. To get a coherent link to the files, it is a good idea to add a *permalink* to the YAML front matter like the following. -#+begin_example +#+begin_src emacs-lisp --- title: FMark permalink: /portfolio/fmark/ --- -#+end_example +#+end_src This means that the file will then be accessible using =https://www.website.com/portfolio/fmark/=. @@ -1075,24 +1090,24 @@ the projects, and even use a limit to limit the projects to a specific number. This can be useful when showing a few projects on the main page, and also want a page displaying all the projects. -#+begin_example +#+begin_src emacs-lisp {%- raw -%} {% assign proj_reverse = site.portfolio | reverse %} {% for project in proj_reverse limit: 3 %} {% endraw %} -#+end_example +#+end_src By default, the projects are listed from earliest to latest, so to display the three latest projects, the list first has to be reversed. Inside the for loop, variables like -#+begin_example +#+begin_src emacs-lisp {%- raw -%} {{ project.title }} {{ project.excerpt }} {% endraw %} -#+end_example +#+end_src can be used to access the variables declared in the YAML, to generate views of the projects. @@ -1280,19 +1295,19 @@ download the emails from and how to authenticate properly. The most important parts to set up in the config file are -#+begin_example +#+begin_src emacs-lisp IMAPAccount gmail Host imap.gmail.com User user@gmail.com Pass password SSLType IMAPS CertificateFile /etc/ssl/certs/ca-certificates.crt -#+end_example +#+end_src to setup the account, and then the following to setup the directories where it should download emails to -#+begin_example +#+begin_src emacs-lisp IMAPStore gmail-remote Account gmail @@ -1307,7 +1322,7 @@ where it should download emails to Patterns * Create Both SyncState * -#+end_example +#+end_src It should then be mostly ready to download all the emails. If using two factor authentication, one can generate an app password which can be @@ -1345,9 +1360,9 @@ work after it has been configured correctly in emacs. To use =mu= in emacs as well, one first has to load the emacs lisp file using -#+begin_example +#+begin_src emacs-lisp (require 'mu4e) -#+end_example +#+end_src After that, =mu4e= can be configured with different things like the home directory, and shortcuts that should be used in emacs. The full @@ -1363,13 +1378,13 @@ Sending emails from Emacs requires a different protocol which is SMTP, however, that is already included in Emacs. The most basic setup can be seen below. -#+begin_example +#+begin_src emacs-lisp (smtpmail-smt-user . "email@gmail.com") (smtpmail-local-domain . "gmail.com") (smtpmail-default-smtp-server . "smtp.gmail.com") (smtpmail-smtp-server . "smtp.gmail.com") (smtpmail-smtp-service . 587) -#+end_example +#+end_src *** Conclusion :PROPERTIES: diff --git a/data/news.toml b/data/news.toml index 1099a6e..3a26104 100644 --- a/data/news.toml +++ b/data/news.toml @@ -1,6 +1,6 @@ [[news]] date = 2021-08-31 -event = "Paper on Vericert accepted at OOPSLA'21" +event = "Paper on Vericert accepted at OOPSLA'21." [[news]] date = 2021-05-31 -- cgit