Formal methods in EDA

References:

  • Electronic Design Automation for IC system Design, Verification, and Testing. By Luciano Lavagno, Igor L. Markov, Grant Martin, and Louis K. Scheffer. 2nd Edition.

More

  • Logic Verification -- languages
  • References: Electronic Design Automation for IC system Design, Verification, and Testing. By Luciano Lavagno, Igor L. Markov, Grant Martin, and Louis K. Scheffer. 2nd Edition. Chaper 15 Steps of IC design design in C/C++ model –> simulators, func good design in RTL –> simulating, and compare with the C/C++ reference model Synthesis: Translate RTL to gate-level netlist. Place and Route: netlist as input, generates polygons that will become wires and transistors on the chip.

  • Logic Verification -- Digital Simulation
  • References: Electronic Design Automation for IC system Design, Verification, and Testing. By Luciano Lavagno, Igor L. Markov, Grant Martin, and Louis K. Scheffer. 2nd Edition. Chapter 16 Simulation: when the program (or model) runs correctly, then one can be reasonably assured that the logic of the design is correct, for the cases that have been tested in the simulation. More

  • Formal Property Verification
  • References: Electronic Design Automation for IC system Design, Verification, and Testing. By Luciano Lavagno, Igor L. Markov, Grant Martin, and Louis K. Scheffer. 2nd Edition. Chapter 20 Intro 1994, Intel spent $500 million to recall the Pentium CPU due to a functional bug that produced erroneous floating-point division results that were off by as much as 61/{1,000,000} [112]; Simulation-based logic verification is becoming less and less effective due to the growing complexity of the systems; Large systems are often decomposed into blocks each of these blocks is simulated separately in its own environment; full-chip/system simulation is carried out after block-level simulation is stable; A dramatic increase in the effort invested in simulation-based verification a complete simulation environment, including tests, checkers, coverage monitors, and environment models, is developed and maintained for each block; Half of the total design efforts is devoted to verification; The number of bugs is growing exponentially, and hundreds of billions of simulation cycles are consumed; Only a negligible percentage of all possible executions of the design is actually being tested.

  • Intro
  • References: Electronic Design Automation for IC system Design, Verification, and Testing. By Luciano Lavagno, Igor L. Markov, Grant Martin, and Louis K. Scheffer. 2nd Edition. 1.1 Introduction Modern integrated circuits (ICs) are enormously complicated, sometimes containing billions of devices. The design of these ICs would not be humanly possible without software (SW) assistance at every stage of the process. The tools and methodologies used for this task are collectively called

Created Mar 11, 2022 // Last Updated Dec 6, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?