Add twitter archive

4 files changed, 453 insertions, 1 deletions

diff --git a/content.org b/content.org
index acea238..4c2ba15 100644
--- a/content.org
+++ b/content.org
@@ -1735,6 +1735,459 @@ The following is a non-exhaustive list of books I've read.
 - /Why We Sleep/, by Mathew Walker
 - /On Writing Well/, by William Zinsser
 
+* Twitter
+:PROPERTIES:
+:EXPORT_FILE_NAME: _index
+:EXPORT_HUGO_SECTION: twitter
+:END:
+
+*@watislaw* *@notypes* Yep that's very fair
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532392678100455424][Thu Jun 02 16:04:19 +0000 2022]])
+
+--------------
+
+*@watislaw* *@notypes* But this
+https://twitter.com/watislaw/status/1532380177254187009?s=20&t=FI55wZOiaasTGO7ezfp11Q
+does explain why assign can be modelled as ~always_comb~ and not ~always @*~.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532391377207758850][Thu Jun 02 15:59:09 +0000 2022]])
+
+--------------
+
+*@watislaw* *@notypes* Yeah OK, I just took their word but it would have been
+better with a reference! But OK, I really need to look more at ~always_comb~ vs
+~always @*~, because I thought that even with no multidriven and no delays,
+~assign != always @*~.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532390966572769283][Thu Jun 02 15:57:31 +0000 2022]])
+
+--------------
+
+*@watislaw* *@notypes* What's not quite right? That ~assign~ can be modelled as
+~always @*~? Because I think they agree with that in the paper. They really only
+say that the standard says that this should be done, but even without
+multidriven nets it has inconsistencies.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532385129020153857][Thu Jun 02 15:34:19 +0000 2022]])
+
+--------------
+
+*@notypes* This assumes using blocking assignment inside of the combinational
+always block though. Also *@watislaw* might be able to add a better explanation!
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532382576362528769][Thu Jun 02 15:24:11 +0000 2022]])
+
+--------------
+
+*@notypes* Meredith et
+al. (https://ieeexplore.ieee.org/abstract/document/5558634) try to address
+this. They state the Verilog standard basically says that the semantics of
+src_verilog[:exports code]{assign x = y;} should be handled like
+src_verilog[:exports code]{always @* x = y;} But say that this can lead to
+inconsistencies between the "hardware semantics" and simulation
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532381674851409921][Thu Jun 02 15:20:36 +0000 2022]])
+
+--------------
+
+I have also now created a poster for *@splashcon* about our paper on "Formal
+Verification High-Level Synthesis" that we are presenting on Friday 22nd at
+20:05 BST at OOPLSA'21! Here is a summary thread about the paper. 1/7
+
+https://yannherklotz.com/docs/splash21/poster.pdf
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063840343887873][Mon Oct 18 11:38:55 +0000 2021]])
+
+--------------
+
+FPGAs are a great alternative to CPUs for many low-power applications, because
+the circuit can be specialised to each application. An FPGA is traditionally
+programmed using a logic synthesis tool by writing in a hardware description
+language like Verilog. 2/7
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063842554298368][Mon Oct 18 11:38:55 +0000 2021]])
+
+--------------
+
+However, writing Verilog can be quite daunting if one doesn't have hardware
+design experience, and it can also take a long time to test and get right.
+
+One alternative to this is high-level synthesis (HLS), allowing you to write C
+which will get translated into Verilog. 3/7
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063844253093896][Mon Oct 18 11:38:56 +0000 2021]])
+
+--------------
+
+Current HLS tools focus on generating optimal Verilog, however, they can be
+quite unreliable because of that, negating any testing that was done on the C
+code. This means the generated Verilog needs to be thoroughly tested again. 4/7
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063845918224384][Mon Oct 18 11:38:56 +0000 2021]])
+
+--------------
+
+Our solution is Vericert, a formally verified HLS tool, so that any guarantees
+made in C also automatically translate to the Verilog code.  Vericert is based
+on the CompCert C compiler, so that it can translate C code into Verilog. 5/7
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063847587467267][Mon Oct 18 11:38:56 +0000 2021]])
+
+--------------
+
+The bad news is that we are 27x slower than an existing optimised HLS tools when
+divisions are present, as we implement divisions naïvely in Verilog.
+
+However, the better news is, with division implemented as an iterative
+algorithm, we are only 2x slower. 6/7
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063849231638529][Mon Oct 18 11:38:57 +0000 2021]])
+
+--------------
+
+If you are interested in knowing more, I have added links to a blog post, our
+paper, and our GitHub repository: 7/7
+
+- https://vericert.ymhg.org/2021/10/a-first-look-at-vericert/
+- https://doi.org/10.1145/3485494
+- https://github.com/ymherklotz/vericert
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063850963968006][Mon Oct 18 11:38:57 +0000 2021]])
+
+--------------
+
+*@jinxmirror13* *@CamlisOrg* *@kaixhin* *@LboroVC* Congrats!!! Enjoy attending
+in person! 🎉
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1446958594835075072][Sat Oct 09 21:59:46 +0000 2021]])
+
+--------------
+
+*@lorisdanto* Thanks!
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1446958086678319107][Sat Oct 09 21:57:45 +0000 2021]])
+
+--------------
+
+*@jinxmirror13* Thank youu!!
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1446958044462686212][Sat Oct 09 21:57:35 +0000 2021]])
+
+--------------
+
+I have finally gotten around to writing an introductory blog post about
+Vericert, our formally verified HLS tool that we will be presenting on Friday
+22nd at OOPSLA'21!
+
+https://vericert.ymhg.org/2021/09/a-first-look-at-vericert/
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1446828476833619968][Sat Oct 09 13:22:44 +0000 2021]])
+
+--------------
+
+*@watislaw* *@jfdm* That sounds really interesting actually. I have realised
+that I don't really know too much about the details of synthesis myself, so
+might try building a simple one using Lutsig as an example.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1437437352809488391][Mon Sep 13 15:25:45 +0000 2021]])
+
+--------------
+
+*@jfdm* Which parts did you find hand wavy?
+
+I hope it does, but the main overlap between this and Lutsig is the Verilog
+semantics, and we only really go into details about the differences.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1437384017293291520][Mon Sep 13 11:53:49 +0000 2021]])
+
+--------------
+
+Just finished the camera ready version of our (with *@wicko3*, *@nadeshr5* and
+James Pollard) paper "Formal Verification of High-Level Synthesis", which will
+be presented at OOPSLA'21 *@splashcon*!
+
+Stay tuned for a blog post about this paper soon.
+
+https://yannherklotz.com/papers/fvhls_oopsla21.pdf
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1437358477119270916][Mon Sep 13
+10:12:20 +0000 2021]])
+
+--------------
+
+Although my supervisor *@wicko3* has already written a great summary of the
+paper!
+
+https://johnwickerson.wordpress.com/2021/08/27/vericert/
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1437358478734118915][Mon Sep 13 10:12:20 +0000 2021]])
+
+--------------
+
+*@gabeusse* *@gconstantinides* *@imperialcas* @jianyi_cheng* *@Stanford* *@UCLA*
+**@Penn* Yep, our short paper preprint is available here:
+
+https://yannherklotz.com/papers/esrhls_fccm2021.pdf
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1392202613769244678][Tue May 11 19:39:03 +0000 2021]])
+
+--------------
+
+RT *@wicko3*: Here is a short blog post about an #FCCM2021 paper that will be
+presented next week by *@ymherklotz* about our work (with Zewei D...
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1390670893798629382][Fri May 07 14:12:33 +0000 2021]])
+
+--------------
+
+*@wicko3* I'll have to read that then, it seems like it is a very nice
+introduction to concurrent computation as well.
+
+Bigraphs seem really interesting though because such a visual representation can
+describe distributed computations.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1341516552500359168][Tue Dec 22 22:50:44 +0000 2020]])
+
+--------------
+
+*@wicko3* Oh interesting! I haven't heard of those before, but it makes sense
+that there is a formalisation.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1341512000984281088][Tue Dec 22 22:32:39 +0000 2020]])
+
+--------------
+
+Decided to write a bit about a note-taking method that finally seems to work for
+me, following closely how Niklas Luhmann took his notes in his famous
+Zettelkasten. Currently using #emacs with #orgmode which works perfectly for it.
+
+https://yannherklotz.com/blog/2020-12-21-introduction-to-luhmanns-zettelkasten.html
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1341145333083107328][Mon Dec 21 22:15:39 +0000 2020]])
+
+--------------
+
+*@gconstantinides* Thank you! Glad to have had such a great discussion.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1328760838900113408][Tue Nov 17 18:04:05 +0000 2020]])
+
+--------------
+
+*@watislaw* I was actually doing the same which is why I came across this weird
+behaviour. I think this is a similar example to the one I gave, where single
+always blocks never recurse, and therefore don't update signals again. Here when
+they are separated they never reach a steady state.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318852927814045696][Wed Oct 21 09:53:35 +0000 2020]])
+
+--------------
+
+*@watislaw* Yes that's true, and I think in this case they do actually follow
+the standard correctly, even though I would expect them to recurse in the same
+always block when signals in the sensitivity list change and maybe reach some
+steady state, although I don't know how feasible that is.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318561007770488832][Tue Oct 20 14:33:36 +0000 2020]])
+
+--------------
+
+*@watislaw* That's exactly what I was looking for actually, I must have missed
+it in the standard, thanks! I was looking in the combinational circuits part.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318560200673140746][Tue Oct 20 14:30:24 +0000 2020]])
+
+--------------
+
+However, synthesis tools will produce the following netlist, where the input is
+directly connected to the output. Is this a bug in the simulator or the
+synthesis tool? Or is this mismatch correct and should that be the case?
+
+[[file:./static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png]]
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318551579151245322][Tue Oct 20 13:56:08 +0000 2020]])
+
+--------------
+
+What should the following Verilog design produce?
+
+Should it be a latched shift register, where the output is equal to the previous
+input?
+
+Or should it be a direct assignment from input to output?
+
+[[file:./static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png]]
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318551572889194496][Tue Oct 20 13:56:07 +0000 2020]])
+
+--------------
+
+Even this simple piece of Verilog has ambiguities in Simulation and Synthesis.
+
+Simulators will just execute the always block when the input changes, and the
+output will therefore be set to the previous value of the input.
+
+The whole testbench is here:
+
+https://gist.github.com/ymherklotz/e8600f8c2e1564f4679fe3a99146a874
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318551574793359360][Tue Oct 20 13:56:07 +0000 2020]])
+
+--------------
+
+Vericert is written in Coq and will allow for a trustworthy, verified
+translation from C to Verilog using CompCert as the front end.
+
+This eliminates the need to manually verify the correctness of the generated
+hardware, which is tedious and expensive.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1286616989583265792][Fri Jul 24 10:59:29 +0000 2020]])
+
+--------------
+
+We just made our (James Pollard, *@nadeshr5*, *@wicko3*) work-in-progress
+formally verified high-level synthesis tool Vericert public!
+
+https://github.com/ymherklotz/vericert
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1286616987871981568][Fri Jul 24 10:59:28 +0000 2020]])
+
+--------------
+
+*@kumastz* *@wicko3* Thanks!!
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1273726889367080963][Thu Jun 18 21:18:49 +0000 2020]])
+
+--------------
+
+*@Helidcotor22* *@wicko3* Thank you!
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1273726579697483777][Thu Jun 18 21:17:35 +0000 2020]])
+
+--------------
+
+I really enjoyed the student research competition at #PLDI2020 enjoyed talking
+to everyone who came by my poster and also got great feedback from the judges!
+https://twitter.com/wicko3/status/1273710075966885889
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1273723966046318593][Thu Jun 18 21:07:12 +0000 2020]])
+
+--------------
+
+Really enjoyed presenting our work on fuzzing synthesis tools at #FPGA2020
+https://twitter.com/gconstantinides/status/1232464094659104768
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1232466970500456449][Wed Feb 26 00:46:38 +0000 2020]])
+
+--------------
+
+*@wicko3* I'm guessing because it's a package manager for *nix systems. Makes it
+really hard to google for errors though because it just comes up with linux
+search results.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1229156715637223424][Sun Feb 16 21:32:52 +0000 2020]])
+
+--------------
+
+Been using Coq with OCaml extraction lately, with various dependencies for both
+and have found Nix really useful to build the project reliably and on different
+platforms.
+
+Wrote a post on how to set up a quick derivation for Coq.
+
+https://yannherklotz.com/blog/2020-02-15-nix-for-coq-development.html
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1229149071790747649][Sun Feb 16 21:02:29 +0000 2020]])
+
+--------------
+
+Congratulations Dr. He Li !!!!
+
+https://twitter.com/DrHelicopter2/status/1228018755072073729
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1228095080105435136][Thu Feb 13 23:14:18 +0000 2020]])
+
+--------------
+
+*@fangyi_zhou_* You could try out Nix, been working great for me for Coq and
+Ocaml.
+
+https://nixos.org/nix/
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1224983007406317568][Wed Feb 05 09:08:02 +0000 2020]])
+
+--------------
+
+*@jianyi_cheng* Looking forward to the presentation!
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1206378185027411971][Mon Dec 16 00:59:07 +0000 2019]])
+
+--------------
+
+The final version of our FPGA '20 paper "Finding and Understanding Bugs in FPGA
+Synthesis Tools" is now ready.
+
+We added many more runs for various Yosys versions and have now managed to
+properly test Quartus.
+
+https://yannherklotz.com/papers/fubfst_fpga2020.pdf
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1206300348656291842][Sun Dec 15 19:49:49 +0000 2019]])
+
+--------------
+
+Congrats Sina!!
+
+https://twitter.com/sinaxs/status/1205115213411950595
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1205952393038446592][Sat Dec 14 20:47:10 +0000 2019]])
+
+--------------
+
+*@tom_verbeure* *@johnregehr* *@whitequark* @oe1cxw* Most of the bugs found in
+*Yosys were in the optimisation passes, which I don't think are applied when
+*Yosys passes the design to ABC or an SMT solver, so these were not affected. We
+*are looking into using multiple equivalence checkers so that these are tested
+*at the same time.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1193947458621116419][Mon Nov 11 17:43:51 +0000 2019]])
+
+--------------
+
+*@johnregehr* *@whitequark* *@oe1cxw* Link to VlogHammer:
+
+http://www.clifford.at/yosys/vloghammer.html
+
+There is also a random Verilog generation tool called VERGEN from 2003, but I
+don't think it was used to fuzz existing tools properly.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1193940002637590528][Mon Nov 11 17:14:13 +0000 2019]])
+
+--------------
+
+*@johnregehr* *@whitequark* *@oe1cxw* has written a tool called VlogHammer which
+focused on fuzzing expressions in synthesis tools and also reported many bugs to
+these vendors. However, these took a long time to fix in commercial tools and
+some still are not fixed.
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1193938897560121344][Mon Nov 11 17:09:50 +0000 2019]])
+
+--------------
+
+*@jrenauardevol* *@johnregehr* *@mithro* Yes, currently hosted on github:
+
+https://github.com/ymherklotz/verismith
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1193922618388340741][Mon Nov 11 16:05:08 +0000 2019]])
+
+--------------
+
+Currently working on my Entity Component System for my game engine! More info at
+
+https://github.com/ymherklotz/YAGE
+
+(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1008858830216880128][Mon Jun 18 23:47:43 +0000 2018]])
+
 * Photos
 :PROPERTIES:
 :EXPORT_FILE_NAME: _index
diff --git a/static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png b/static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png
new file mode 100644
index 0000000..cc6e4ea
--- /dev/null
+++ b/static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png
diff --git a/static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png b/static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png
new file mode 100644
index 0000000..72a0f61
--- /dev/null
+++ b/static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png
diff --git a/themes/ymherklotz/static/css/default.css b/themes/ymherklotz/static/css/default.css
index f9e7ef3..0aa1b1f 100644
--- a/themes/ymherklotz/static/css/default.css
+++ b/themes/ymherklotz/static/css/default.css
@@ -170,7 +170,6 @@ body {
 
 p {
   margin-top: 0.5em;
-  text-align: justify;
   hyphens: auto;
 }