Recently, I got hold of a Papilio One (which you can think of as the Arduino of FPGAs). The Papilio board has a Xilinx Spartan 3 on board, which is plenty enough to get started learning about FPGAs. Here’s what the board looks like:
Now, it might look big above … . . . → Read More: Testing out my Papilio FPGA!
Yesterday, I was looking at the stats on Ohloh for the Whiley project and noticed that my total line count for the project had increased from around 65KLOCto 143KLOC over a very short amount of time:
Confused, I was pondering this for a while. Then it struck me: I’d checked in . . . → Read More: A Source File with 72KLOC!?
Whilst it’s been over three months since the last release of Whiley, this latest release is chocked full of improvements! I’ve closed around 60 issues in that time, and have completely reworked the theorem prover from scratch. This means compile-time checking of constraints is starting to work better — however, there remains quite a . . . → Read More: Whiley v0.3.17 Released!
Probably the most interesting aspect of the Whiley language is that it supports compile-time verification of preconditions, postconditions and other invariants. There are two main aspects of how this works:
Generation of Verification Conditions (VCs) from the source code. A verification condition is a logical expression which, if proved to be satisfiable, indicates an . . . → Read More: Generating Verification Conditions for Whiley