Hardware
Description and Verification

2009 edition

Thomas Hallgren

Start

Hardware
Description and Verification

2009 edition

http://www.cse.chalmers.se/edu/course/TDA956/

Thomas Hallgren

Hardware
Description and Verification

Getting hardware designs right
[using ideas from computer science]

Hardware?

Description?

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;

Verification?

Informal Idea

Formal Specification ∀ ∃

Circuit Description

Circuit

  • 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, ...
  • 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

Schedule

People

Teachers

Guest lecturers

People behind the scenes

People

My background

People

Your background?

Have you used

Hardware is reliable, software is buggy?

No, hardware is buggy too!

[6502]

Some examples from my own experience

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
Miscommunication11.4
Microarchitecture9.3
Logic/microcode changes9.3
Corner cases8
Powerdown5.7
Documentation4.4
Complexity3.9
Initialization3.4
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

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!

Conclusion