Remove vericert blog post

1 files changed, 0 insertions, 47 deletions

diff --git a/content.org b/content.org
index 9e3b2e0..4c8a1c5 100644
--- a/content.org
+++ b/content.org
@@ -33,53 +33,6 @@ is located.
 
 Here you can find all my previous posts:
 
-** TODO 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