Embedded Systems: Theory, Modeling and Verification August 2006
Instructors: Matthieu Moy (moy@csa) Prabhat Mishra (prabhat@csa) K. Gopinath (gopi@csa)
Lectures: Tue/Thu 10:00 - 11:30 AM CSA 252
Overview:
Embedded systems run the computing devices hidden inside a vast array
of everyday products and appliances such as cell phones, toys, handheld PDAs,
cameras, and microwave ovens. Cars are full of them, as are airplanes,
satellites, and advanced military and medical equipments. As applications
grow increasingly complex, so do the complexities of the embedded computing
devices. The goal of this course is to develop a comprehensive understanding
of the technologies behind the embedded systems design. The students develop
an appreciation of the existing capabilities and limitations of various
steps in overall design methodology - modeling/specification, exploration,
partitioning, synthesis(hardware/software/interface), and
validation/verification of embedded systems.
Prerequisites:
Good skills in programming and basic knowledge of computer organization/architecture or consent of instructor(s).
Assignment: lustre-assignment.pdf: Assignment with the Lustre language. Deadline: September 19th 2006. Last minute note for using Lustre:
On some recent systems, tail +n (give the last but n lines) is not accepted anymore, but some lustre tools still use it.
To fix this, download this tail shell script wrapper, and put it in a directory at the beginning of your PATH.
For example, in $HOME/bin, and then put export PATH=${HOME}/bin:${PATH} in your shell configuration file.
Correction: (New!)
The correction is available in the subdirectory lustre-corrected/ of this site (I'm not putting a link to avoid robots to go there. Just add lustre-corrected at the end of the current URL). You have tramway.lus which is a quick correction of the tramway problem, and one .tar.gz per person. This .tar.gz file contains your code plus my remarks. Just grep 'MM:' -rn . in it to see my remarks, also available in remarks.txt.
Example Programs:
env.lus: A system in which the proof
uses only the environment specification, not the program to
proove!
Documentation in the docs/ directory of the SystemC
distribution.
"A Methodology for SoC Top-Level Validation using Esterel
Studio"
(PDF).
Gives you an idea of how synchronous language can be used in a
verification framework (for both TLM and RTL).
Erratum: I forgot to mention the role of the
interrupt signal in the SystemC assignment. The interrupt signal
is low (false) by default, and is raised to
true by the component "multiplier" when the result of
computation is ready. The CPU is sensitive to positive edge on
this signal. The interrupt is reset to false when a
value is read on a register.
(New!) Correction: simple-system.cpp, router.map (not very well commented, but
gives you an idea of what I expected). (New!) My comments on your code are
available in the subdirectory systemc-corrected/ of
this site (just add systemc-corrected/ to this URL.
Assignment: Choose any one of the following topics and write a one-page description of a new research direction. You need to survey the domain to understand what has been done so far and what are the remaining important challenges. Formulate an approch for addressing (solving) one or more of these challenges. The one-page document should clearly describe the problem (challenge) and your proposed solution (methodology). Send the PDF by email to me on or before Nov 7, 2006. Some of the related conferences are DAC, ICCAD, DATE, CODES+ISSS, FPGA, ISCA, CAV, and ISLPED.
Low Power Scheduling Algorithms for Real-time Embedded Systems
Modeling and Verification of Pipelined Processors using Petri-Nets
Readings: The first two items are available from here or can be accessed directly from Rushby's website. The last two items are available from Kopetz's publications and presentations websites.