Update content

1 files changed, 104 insertions, 89 deletions

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
-  <!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
-#+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
-  <!-- markdown-toc end -->
-#+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 <nixpkgs> {};
 
   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 <nixpkgs> {};
 
   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 <nixpkgs> {};
 
   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: