adreid

6 ms·

1.
by adreid 2y ago
This has been available for arm for some years. Here is a blog post I wrote at around the time it was released. The easiest bits to use would be the instruction formats and the register fields https://alastairreid.github.io/
2.
by adreid 2y ago
Note that herd contains an ASL1 implementation. https://github.com/herd/herdtools7/tree/master/asllib
3.
by adreid 2y ago
Fixing the whole problem is large but there is a small sequence of steps that would improve things a lot that can be taken. Specify the key formats in a json/xml file then go one by one through tools, docs, etc changing them to use the
4.
by adreid 6y ago
The difference is really about the level of annotation you provide. In testing (and the more automated verifiers) you might add assertions. In the “auto active” tools, you are adding more function contracts, invariants, maybe hints to he
5.
by adreid 6y ago
Burnt Sushi only uses the type to generate values. Proptest lets you constrain the values more precisely. Eg you can create a btreemap with up to 5 entries where the keys are some subset of ints (say) and the values are some subset of some
6.
by adreid 6y ago
This is more at the end of automatic verification tools like KLEE, SMACK, etc. Auto active tools like Prusti are super-interesting too and I suspect that we need a hybrid approach.
7.
by adreid 6y ago
That is the project we are trying to support with our work. Unfortunately, this means I have to solve lots of hard problems like scaling, usability, modular verification, etc.
8.
Rust testing or verifying: Why not both?(alastairreid.github.io)
143 points by adreid 6y ago|28 comments
9.
by adreid 9y ago
Yes, that is a large part of what I was saying. Also, some things are so hard to specify formally that we still don't know have any kind of formal spec. Memory concurrency semantics is an example. It is only in the last couple of yea
10.
by adreid 9y ago
Knowing more ways of tackling more problems makes you a better programmer. The more difference there is between what you do at home and what you do at work, the more you will learn. If at work you write C/C++/Java, learn Haskell
11.
by adreid 9y ago
There has been a steady industry of people retyping the manuals of all the major architectures for use in formal verification. At PLDI last year, there was even a paper where a team used synthesis techniques to automatically generate an in
12.
by adreid 9y ago
Incidentally, there was some discussion about this on reddit too. https://www.reddit.com/r/programming/comments/66kyez/arm_rel... Topics included the license, what you can do with it, what other specs ar
13.
by adreid 9y ago
I agree - that should definitely be possible. Not necessarily easy though - but if anybody is looking for a PhD topic or, better yet, a whole research group looking for a challenge, you have all the bits you need to make it happen.
14.
by adreid 9y ago
Probably best not to get too excited about generating hardware from the specs... That would compete with ARM's main source of revenue and my reading of the license is that that is the one thing you cannot do with the spec. But I am no
15.
by adreid 9y ago
Yes, ARM's architecture licensees (companies allowed to design their own ARM-compatible processors) have had access to the v8-A specs for years. The new bit is making it available so that researchers, companies and individuals can use
16.
by adreid 9y ago
I've been working on making the specs be more than just a way of killing trees since April/May 2011. So I have had time to do a few things with it. I would say I have a love-hate relationship with XML - your feelings seem to be l
17.
by adreid 10y ago
Since you have to feed it ultrasonic energy to power it, I suspect it is not too bad because, IIRC, ultrasonic has a short range. You could feed it electromagnetic energy - but then all you really have is a smaller version of the Great Seal
18.
by adreid 10y ago
From reading (ok, skimming) the paper, it seems that the sensor is powered by an external ultrasonic transducer and, I think, returns data by modulating that signal (a bit like RFID). That means that you lose power when the ultrasonic is re
19.
Graphene-Enabled Paper Makes for Flexible Display(spectrum.ieee.org)
1 points by adreid 10y ago|0 comments
20.
by adreid 10y ago
It takes a lot of effort to write a specification. Just think how much software you have ever seen complete specifications for - and how close that number is to zero. So if you are going to write a specification, you really want to get max
21.
by adreid 10y ago
Thanks for the pointers to other HDLs. I was aware of Chisel but had not seen Clash before. Another Haskell Hardware DSL is Lava: http://ku-fpg.github.io/software/kansas-lava/ Chisel is very similar to Lava in man
22.
by adreid 10y ago
A few clarifications: The paper is about searching for bugs in ARM's designs - not designs by ARM's architecture licensees. (ARM has two types of partner: those who use ARM designed processors exactly as provided by ARM and those