Description and Verification

2010 edition

Thomas Hallgren

Description and Verification

2010 edition


Thomas Hallgren

Description and Verification

Getting hardware designs right
[using ideas from computer science]



Hardware Description Languages

  • VHDL
  • Lava
  • Verilog
entity counter is
  generic( bits : natural;
           bound : integer );
  port( clk, inc, reset : in std_logic;
        o : out unsigned(bits-1 downto 0);
        carry : out std_logic );
end entity counter;

architecture behavioral of counter is
end architecture behavioral;


Informal Idea

Formal Specification ∀ ∃

Circuit Description


  • Simulation
  • Symbolic Simulation
  • Model Checking
  • Theorem Proving
  • ...

Steps in Designing Hardware

According to Slides by Jacob Abraham

Design Implementation Verification

According to Slides by Jacob Abraham

In this course

Focus on Verifying Hardware Descriptions

Organisation of this course

Part 1: Industrial

  • Languages: VHDL and PSL
  • Tools: ModelSim, Jasper Gold, ...
  • Theory: BDDs, Model Checking, ...
  • Lab 1
  • Take home exam 1

Part 2: Research

  • Language: Lava
  • Tools: Lava, SMV, ...
  • Theory: SAT solving, ...
  • Lab 2
  • Take home exam 2

Guest Lectures

At the end of the course

  • Regular written exam




Guest lecturers

People behind the scenes


My background


Your background?

Have you used

Hardware is reliable, software is buggy?

No, hardware is buggy too!


Some examples from my own experience

But these bugs are not so serious. Other bugs could be very serious...

The problem in perspective

1970s: software crisis

1990s: hardware crisis?

Moore's Law

Number of transistors on an a chip

Year Processor Number of transistors
1975 6502 10,000
1985 386 275,000
1993 Pentium 3,100,000
2000 Pentium 4 42,000,000
2006 Core 2 Duo 253,000,000

Increasing circuit size allows more and more complex functionality to be implemented in hardware.

Hardware bugs can be very expensive!

Design Bug Distribution in Pentium 4

According to Slides by Jacob Abraham

Source: EE Times, July 4, 2001
Type of BugPercentage
"Goof" "Goof"12.7
Logic/microcode changes9.3
Corner cases8
Late definition2.8
Incorrect RTL assertions2.8
Design mistake2.6
42 Million transistors,
1+ Million lines of RTL
100 high-level logic bugs found
through formal verification

Benefits of formal verification

It's not just for the big players like Intel and IBM. Formal verification helps in smaller projects too! See article by Ping Yeung: Static verification - what’s old is new again

Is there still a problem?

International Technology Roadmap for Semiconductors 2006:
Without major breakthroughs, verification will be a non-scalable, show-stopping barrier to further progress in the semiconductor industry.

Mission: Impossible?

Your mission, should you decide to accept it, is to make sure that future hardware works correctly!