« September 2004 | Main | November 2004 »
October 28, 2004
[Research] Hybrid Model Checking
[Project: Model checking methods and tools for hybrid logics (NIWI)] Thinking about building some real-time and continuous space models for environments in which embedded systems operate.
- Hytech paper a classic hybrid model checking paper. The hytech homepage
- Tom Henzinger's homepage
Posted by jones at 11:45 AM | Comments (0)
[Misc.] Buying a car on the third market
[Brigham Young University Surplus Property InformationMaintained by the BYU Purchasing Department, UCCU Repos for sale] Let's say you want to buy a new junker to replace your old junker. Here's a few handy sites, well, in Utah county at least.
Posted by jones at 08:24 AM | Comments (0)
October 27, 2004
[Research] Open source embedded mp3 players
[EE Times -Trio builds open-source MP3 player] Makes an interesting verification pilot project. We want to use our formal verification tools to verify properties of such a design. The tools can't handle such complexity now, but that's what makes it interesting research. If you've got an open or closed source MP3 player for an embedded processor you need verified (well, not anytime soon, but you'd like some intense debug time spent on it for free) let me know. We'll sign any NDA put before us :).
Interestingly, the open source MP3 player listed above was released on a Cirrus EP7212 board. Surprisingly, the EP7212 board uses an ARM720T processor. That's not all bad since we have an ARM720T simulator with gdb 6.1. Now, the twist is that the EP7212 is discontinued, but, the EP7312 has since been released and also uses the ARM720T. Can the old MP3 code be used on the new board?
Here's a few other open source mp3 player projects...
- list of mp3 player projects
- Coldfire and some SnapGear NETtel thing that uses various open source decoders and uc Linux to implement an MP3 player that reads off ethernet. uCLinux on the Motorola ColdFire. The coldfire page. ucLinux tools for the mac. The gdb 6.1 docs describe a m68k sim directory and how to make it simulate a coldfire. But, my 6.1 distro on my Mac has no such directory :(
- Very cool and very open source mp3 player but, it doesn't appear to be implemented on a "standard" processor that we can simulate in gdb 6.1.
- My German isn't so good. But I think that's an AtmelAT90S8515Eight-BitMikrocontroller it that mp3 player, with open source code.
- an MP3 player for the ARM 9 not sure where all the source code is.
Posted by jones at 03:58 PM | Comments (0)
[Research] NSF CFP for emb/hyb ssystems for 2004
[Computer Systems Research (CSR) nsf04609] We are doing some very cool work on verification of machine code instances of embedded software using explicit model checking. We use gdb (or any other simulator) to define the instruction semantics. In the end, we prove or verify that the execution of a given binary on a given processor (or at least its simulator...) either does or doesn't satisfy a property. This NSF program may be a good place to fund this work.
If you have some resources (which include code examples, simulators, tough verification problems from the real world, or even plain old money) that you'd like to donate to support this work, drop me a line at jones@cs.byu.edu
Posted by jones at 01:42 PM | Comments (0)
[Misc.] how does one do ftp in a .net application?
[WinInet API Programming] Its a tough question because obvious answers, like, use the ftp api are replaced with more confusing claims about "use the requenst and response layer" good idea. What does that mean? Hopefully the answer will appear here shortly.
- how to do it in VB.net. Pretty low level. One is reading bytes out of a socket in this code.
- How to do it in C# using the WebRequest and WebResponse classes. That's more like it.
- a C# implementation.
Posted by jones at 08:07 AM | Comments (0)
October 26, 2004
[] Persnickety details about ARM7TDMI
Taken from the Reference Manual
registers and interrupts
- words are 32 bits, halfwords are surprisingly 16 bits and bytes are 8 bits.
- 31 general purpose 32 bit registers.
- 6 status registers.
- r14 is the link register. which holds a copy of the pc value (r15) during a branch with link instruction.
- r15 holds the pc.
- r13 is, by convention, the stack pointer. 2-8
- each mode can treat some registers differently. fast interrupt mode (fiq) is the most different. Looks like the fiq mode just "reservers" (or banks in arm parlance) 8 registers to speed up data transfer.
- thumb mode has 8 regs (though you can access the higher regs directly in ASM)
- the CPSR is the CCR. Not sure what CPSR stands for. There are also 5 SPSR registers for exception handlers 2-13
Max interrupt latency in FIQ mode is 29 cycles. Min interrupt latency in FIQ or IRQ modes is 5 processor clock cycles 2-23.
Timing
page 6-29 has a nice summary of instruction timing. Its nice that there's so few opcodes. Instruction timing depends on the length of a N, S, I and C cycle. These are defining in bus cycle types on page 3-4, well really on page 3-5.Looks like the various kinds of cycles are how one might access memory. The timing models sort of assume that the DRAM will always give you back your data within a cycle but there's a way to stretch your bus cycles.
Timing of multiplication instructions depends on whether or not the operand contains all 0's or 1's in certain locations.
Don't forget to add in busy-wait loop time for non-instantaneous co-processor accesses.
Posted by jones at 08:45 AM | Comments (0)
October 25, 2004
[Research] ARM processor details
[ARM7TDMI] Looking at running some verifiaction experiments on a new platform.- ARM7TDMI seems to be a more entry level processor. 32 bit everywhere fully static, which I think means there's no pipelines, reordering or other fun stuff. We do have gdb support for this one. reference manual Simple three stage dlx-like pipeline. I think this would make a good first pipelined machine.
- ARM1156T2-S Has an 8 or 9 stage integer pipeline. Which is cool. No MMU, which is also good. But our gdb compiler doesn't support it.
- ARM1176 Also has the 8 stage integer pipeline.
- arm arm1020t reference manual. has an mmu and a well-documented 6 stage pipe.
-mcpu=name
This specifies the name of the target ARM processor. GCC uses this
name to determine what kind of instructions it can emit when gener-
ating assembly code. Permissible names are: arm2, arm250, arm3,
arm6, arm60, arm600, arm610, arm620, arm7, arm7m, arm7d, arm7dm,
arm7di, arm7dmi, arm70, arm700, arm700i, arm710, arm710c, arm7100,
arm7500, arm7500fe, arm7tdmi, arm8, strongarm, strongarm110, stron-
garm1100, arm8, arm810, arm9, arm9e, arm920, arm920t, arm940t,
arm9tdmi, arm10tdmi, arm1020t, xscale.
-mtune=name
This option is very similar to the -mcpu= option, except that
instead of specifying the actual target processor type, and hence
restricting which instructions can be used, it specifies that GCC
should tune the performance of the code as if the target were of
the type specified in this option, but still choosing the instruc-
tions that it will generate based on the cpu specified by a -mcpu=
option. For some ARM implementations better performance can be
obtained by using this option.
-march=name
This specifies the name of the target ARM architecture. GCC uses
this name to determine what kind of instructions it can emit when
generating assembly code. This option can be used in conjunction
with or instead of the -mcpu= option. Permissible names are:
armv2, armv2a, armv3, armv3m, armv4, armv4t, armv5, armv5t,
armv5te.
Posted by jones at 08:44 PM | Comments (0)
October 21, 2004
[Education] this is a test
Posted by jones at 08:59 AM | Comments (0)
October 11, 2004
[Misc.] School and scouting calendars
[Alpine School district calendar, Bridal Veils Falls Calendar
] Useful information for calendaring scouting stuff.
Posted by jones at 12:27 AM
[Tech Support] An FTP Library for .Net
[Enterprise Distributed Technologies - edtFTPnet Download] Just in case I need to write an ftp front end to a distributed database application.
Posted by jones at 12:27 AM
October 08, 2004
[Misc.] GIS Resources for a Mac
[GIS resources for Mac] Every now and then I get curious about turning DEM files into pretty pictures of my favorite landscapes using GIS software. Now is one of those times...
- Fruita DEM is 38111C2.exe
- Landserf appears to be the visualizer I've always wanted...
- DEMs for Utah (as exe's)
- DEMs for utah (as .tar.gz's)
Posted by jones at 08:53 AM | Comments (0)
October 07, 2004
[Tech Support] using bibtex.
How to use bibtex in a tex document
1. cvs checkout bib
2. edit bib/lal.bib
3. in your tex document add ...
\bibliography{../bib/lal}
\bibliographystyle{plain}
\end{document}
4. add this to your tex when you want to cite something...
Both Stern's~\cite{stern:cav97} and
\della's~\cite{della:charme03}
Save.
5. Final step
> latex
> bibtex
> latex
> latex
Eric's make will handle this.
Posted by jones at 02:13 PM | Comments (0)
October 06, 2004
[Misc.] Installing wonder baord
[Installing Tile Backer Cement Board] Getting ready to tile a bathroom. Let the good times roll...
Posted by jones at 08:53 PM | Comments (0)