It was 1992 and I was about to leave Rockwell-Collins and move to Austin, Texas to work for Computational Logic Inc., a formal verification research company. My co-worker Bud and I were chatting while walking back from the cafeteria.
“So, what will you be doing for this new company?”
Bud was a long time Collins employee, self-taught in many things and with a healthy dose of skepticism about “the latest thing.”
“I will be doing research on formal verification.”
“What’s that mean?”
“Using a mathematically precise language to describe designs. That way, instead of just testing every case you can think of, you can use a tool they have developed to prove properties about the design.”
“Hmmm. Sounds like Iverson Language.”
“Iverson Language? What’s that?”
I had spent some time looking into different formal verification research efforts but hadn’t heard of Iverson Language.
While we walked, Bud went on to explain that several years earlier, our company’s revered founder, Art Collins, had gone to a lecture by Kenneth Iverson who was visiting the University of Iowa. At the lecture, Iverson had shown how computer designs could be described using a precise mathematical language. Art immediately saw the benefit of clearly communicating design intent.
When we got to his office, Bud pulled a yellow book from the shelf and flipped through it until he came to this figure:
There it was: a specification for “Complete Instruction Fetch” using some sort of mathematical notation!
Why hadn’t I heard of Iverson language?
What was this book?
I looked at the cover and realized that actually, I had not only heard of it, but that I had used it briefly when I was in college.
A programming language survey class I had taken had a section on the programming language APL aka Iverson Language. We used it for array programming problems and the most memorable part for me was that we had to change the Selectric print head on the interactive terminal to get the mathematical symbols.
Paging back to the beginning of the chapter with the instruction fetch specification, I found this introduction:
Microprograms may be used to define a computer instruction set for the programmer, to define the detailed algorithms by which the computer circuits produce the operations of the instruction set, or for a variety of other purposes. In the design and development of a computer, for example, it is important to maintain precise and complete communication between the computer programmer, the computer (or system) designer, and the logical circuit (or hardware) designer. The system designer will, in fact, ordinarily begin with a description at the programmer’s level and proceed through increasing detail to the hardware designer’s level. Meanwhile, the programmers concerned with evaluating potential performance and with developing systems of metaprograms (so-called automatic programming systems) should be enabled to follow and to influence the evolving design.
The use of microprogramming will be illustrated by a description of the IBM 7090 computer (to be called the 7090) at a level approximately suited to the programmer and the system designer. The final section treats some problems in the extension to the hardware design level.
After a few pages describing instruction fetching and branching came the
figure defining and text explaining “Complete instruction fetch” shown above, followed by more text and figures defining the execution of different classes of instructions.
The final section of the chapter was on “Detailed Logic Design” which discussed implementation of a processor’s instruction set in terms of simpler operations in the face of implementation constraints.
So Iverson language used mathematical notation to describe processor instruction sets and implementations, but was it intended for formal verification? From the book’s preface:
Chapter 7 (The Logical Calculus) emphasizes the formal manipulability of the language and its utility in theoretical work.
The idea of formal specification and constructing proofs was clearly there, but hardware was simple enough that the need for formal verification was not obvious.
What was old is new again
Looking at the title page, I found that the book was copyrighted in 1962.
Just to set the context, in 1962 COBOL had been around 3 years and C wouldn’t show up for another 10, it would be another year before ASCII was created and the computer mouse conceived, and John Glenn made the first U.S. manned orbital flight aboard Mercury 6.
So what ever happened to Art’s venture into Iverson language?
According to Bud, Art arranged for his design managers to get classes from Iverson, so that they in turn could teach their designers. It turns out that the managers found this new description language too difficult and it was eventually abandoned.
Ironically, years later Rockwell-Collins went on to do some of the most extensive instruction and microcode-level formal verification in the world, but this time using ACL2, not Iverson Language.
My take-aways
What seemed like the beginning of a promising new field in 1992 was already 30 years old. We have been at it now for over half a century and it seems like we are still just getting started (how many things in the computer industry can you say that about?).
Also, technology transfer is hard. While there have and continue to be limitations in tool capacity, the real challenge has been getting the technology we have incorporated into real design flows. This is also not new.
What if?
By the time that hardware was complicated enough to need formal verification, simulation-based verification flows were already well established and formal methods were lagging design complexity by quite a ways.
What if Iverson Language in the design of hardware had caught on at that early time? What would our design and verification flows look like today?
You can download a copy of Iverson’s A Programming Language book from Computer History Museum’s Software Preservation Group here
© Ken Albin and System Semantics, 2015. All Rights Reserved.