Showing posts from May, 2017

Reasoning about digital circuits using string diagrams

Hardware and software, two worlds apart As I drifted between the worlds of programming languages and hardware design over the last ten years or so, I was quite struck by one significant and maybe difficult to explain difference when it comes to modelling and semantics. 
In the world of software the workhorse of formal verification and validation is operational semantics: programming languages come with a set of syntactical rules showing how the program and other components of its configuration (e.g. the state) evolves during execution.  Let's take, for example, a simple language of commands. We may want to model a program (c) by showing how it changes the state (s), which is a function mapping memory location (addresses) into values. A configuration is a program together with its state, (c, s). We show the execution of a program in a state to a new state as run (c, s) = s' or, using fancier mathy notation (c, s⇓ s'. Here are some sample rules (this list is quite boring,…