
Here is a new library for analyzing PowerPC programs [1]. At this point it does instruction set simulation on machine code -- and not all instructions are implemented yet, BTW. To run a simulation, the user defines an instance of the Memory class [2] to represent both instruction and data memory. The Memory class declares functions for memory loads and stores, instruction fetches, and reading and writing special purpose registers. In our test bench, we set up the 'fetch' method to dump out register values so we can see the state of the processor at every step. A neat feature of the library is the instruction behavior is captured by a little DSL [3]. This makes it easy to add new instructions because the translation from the instruction RTL spec [4] to the DSL is nearly one-to-one. And with instruction behavior captured symbolically, this opens the door to other types of analysis besides just simulation. I hope a few folks find it useful. -Tom [1] http://hackage.haskell.org/package/powerpc [2] http://hackage.haskell.org/packages/archive/powerpc/0.0.1/doc/html/Language-... [3] http://hackage.haskell.org/packages/archive/powerpc/0.0.1/doc/html/Language-... [4] http://www.ibm.com/developerworks/systems/library/es-archguide-v2.html

Wow. Quite ambitious.
Was this inspired by work at your current employer like with Atom and
some of the other stuff you've released?
Warren
On Tue, Mar 9, 2010 at 10:35 PM, Tom Hawkins
Here is a new library for analyzing PowerPC programs [1]. At this point it does instruction set simulation on machine code -- and not all instructions are implemented yet, BTW.
To run a simulation, the user defines an instance of the Memory class [2] to represent both instruction and data memory. The Memory class declares functions for memory loads and stores, instruction fetches, and reading and writing special purpose registers. In our test bench, we set up the 'fetch' method to dump out register values so we can see the state of the processor at every step.
A neat feature of the library is the instruction behavior is captured by a little DSL [3]. This makes it easy to add new instructions because the translation from the instruction RTL spec [4] to the DSL is nearly one-to-one. And with instruction behavior captured symbolically, this opens the door to other types of analysis besides just simulation.
I hope a few folks find it useful.
-Tom

On Wed, Mar 10, 2010 at 8:07 AM, Warren Henning
Wow. Quite ambitious.
Was this inspired by work at your current employer like with Atom and some of the other stuff you've released?
Yes, we had an immediate need to debug some machine code. I looked around, but all the emulators I found (PSIM, et al.) were too complicated. I'm also intrigued by the emphasis on software verification at the object code level for aerospace (DO-178). I figure better tools in this area may open the door to using advanced design methods like Atom for avionics. Of course it's unlikely this project will reach that level of maturity, but you never know. -Tom
Warren
On Tue, Mar 9, 2010 at 10:35 PM, Tom Hawkins
wrote: Here is a new library for analyzing PowerPC programs [1]. At this point it does instruction set simulation on machine code -- and not all instructions are implemented yet, BTW.
To run a simulation, the user defines an instance of the Memory class [2] to represent both instruction and data memory. The Memory class declares functions for memory loads and stores, instruction fetches, and reading and writing special purpose registers. In our test bench, we set up the 'fetch' method to dump out register values so we can see the state of the processor at every step.
A neat feature of the library is the instruction behavior is captured by a little DSL [3]. This makes it easy to add new instructions because the translation from the instruction RTL spec [4] to the DSL is nearly one-to-one. And with instruction behavior captured symbolically, this opens the door to other types of analysis besides just simulation.
I hope a few folks find it useful.
-Tom
Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

2010/3/10 Tom Hawkins
On Wed, Mar 10, 2010 at 8:07 AM, Warren Henning
wrote: Wow. Quite ambitious.
Was this inspired by work at your current employer like with Atom and some of the other stuff you've released?
Yes, we had an immediate need to debug some machine code. I looked around, but all the emulators I found (PSIM, et al.) were too complicated.
I'm also intrigued by the emphasis on software verification at the object code level for aerospace (DO-178). I figure better tools in this area may open the door to using advanced design methods like Atom for avionics. Of course it's unlikely this project will reach that level of maturity, but you never know.
We wrote the debugger and simulator for AVR line of microcontroller cores. We used a DSEL to describe inner workings of commands and now try to apply it to ARM ISA. The Haskell code is heavy on the use of type-level computations and, especially, assiciated types.

Serguey,
I'm working on a similar project. What's the chance you have your source
code in the open?
/jve
On Thu, Mar 11, 2010 at 7:30 AM, Serguey Zefirov
2010/3/10 Tom Hawkins
: On Wed, Mar 10, 2010 at 8:07 AM, Warren Henning
wrote: Wow. Quite ambitious.
Was this inspired by work at your current employer like with Atom and some of the other stuff you've released?
Yes, we had an immediate need to debug some machine code. I looked around, but all the emulators I found (PSIM, et al.) were too complicated.
I'm also intrigued by the emphasis on software verification at the object code level for aerospace (DO-178). I figure better tools in this area may open the door to using advanced design methods like Atom for avionics. Of course it's unlikely this project will reach that level of maturity, but you never know.
We wrote the debugger and simulator for AVR line of microcontroller cores.
We used a DSEL to describe inner workings of commands and now try to apply it to ARM ISA.
The Haskell code is heavy on the use of type-level computations and, especially, assiciated types. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

2010/3/11 John Van Enk
Serguey, I'm working on a similar project. What's the chance you have your source code in the open? /jve
I'll ask. But chances are pretty small. I'll think about reimplementing command description from scratch.
On Thu, Mar 11, 2010 at 7:30 AM, Serguey Zefirov
wrote: 2010/3/10 Tom Hawkins
: On Wed, Mar 10, 2010 at 8:07 AM, Warren Henning
wrote: Wow. Quite ambitious.
Was this inspired by work at your current employer like with Atom and some of the other stuff you've released?
Yes, we had an immediate need to debug some machine code. I looked around, but all the emulators I found (PSIM, et al.) were too complicated.
I'm also intrigued by the emphasis on software verification at the object code level for aerospace (DO-178). I figure better tools in this area may open the door to using advanced design methods like Atom for avionics. Of course it's unlikely this project will reach that level of maturity, but you never know.
We wrote the debugger and simulator for AVR line of microcontroller cores.
We used a DSEL to describe inner workings of commands and now try to apply it to ARM ISA.
The Haskell code is heavy on the use of type-level computations and, especially, assiciated types. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Serguey,
The system I'm writing has a type in place for the AVR instruction set. I'm
working on writing an assembler/disassembler for it as well. It might make
sense, if your employer deems it worthwhile to release the code, to
collaborate.
/jve
On Thu, Mar 11, 2010 at 11:35 AM, Serguey Zefirov
2010/3/11 John Van Enk
: Serguey, I'm working on a similar project. What's the chance you have your source code in the open? /jve
I'll ask.
But chances are pretty small.
I'll think about reimplementing command description from scratch.
On Thu, Mar 11, 2010 at 7:30 AM, Serguey Zefirov
wrote: 2010/3/10 Tom Hawkins
: On Wed, Mar 10, 2010 at 8:07 AM, Warren Henning
wrote: Wow. Quite ambitious.
Was this inspired by work at your current employer like with Atom and some of the other stuff you've released?
Yes, we had an immediate need to debug some machine code. I looked around, but all the emulators I found (PSIM, et al.) were too complicated.
I'm also intrigued by the emphasis on software verification at the object code level for aerospace (DO-178). I figure better tools in this area may open the door to using advanced design methods like Atom for avionics. Of course it's unlikely this project will reach that level of maturity, but you never know.
We wrote the debugger and simulator for AVR line of microcontroller
cores.
We used a DSEL to describe inner workings of commands and now try to apply it to ARM ISA.
The Haskell code is heavy on the use of type-level computations and, especially, assiciated types. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

2010/3/11 John Van Enk
Serguey, The system I'm writing has a type in place for the AVR instruction set. I'm working on writing an assembler/disassembler for it as well. It might make sense, if your employer deems it worthwhile to release the code, to collaborate. /jve
Our work is concerned with semantics of operations. So we build a list of Commands: data Command cpu = Command { cmdName :: String -- right now it's just a string, but it could be a pretty printer -- with calculations for disasm. ,cmdFormat :: [Match cpu] -- when we decode a command in a simulation, -- we set some CPU variables. -- that's what Match encode. ,cmdStatements :: [Stat cpu] -- the semantics of command. } And then we use that list to generate code for our simulation package. Lately we found that we could use those command descriptions for other purposes, like automatic code generator generators, etc, but we didn't explored all that yet. So we don't have a specific type of AVR commands. We have general description of (almost) arbitrary CPU commands which we successfully applied to AVR line of microcontroller cores. Statements contains assignments (Variable cpu size := Expression cpu size), conditionals and various CPU- and bus-specific function invocation (like read from memory or write to it).
On Thu, Mar 11, 2010 at 11:35 AM, Serguey Zefirov
wrote: 2010/3/11 John Van Enk
: Serguey, I'm working on a similar project. What's the chance you have your source code in the open? /jve
I'll ask.
But chances are pretty small.
I'll think about reimplementing command description from scratch.
On Thu, Mar 11, 2010 at 7:30 AM, Serguey Zefirov
wrote: 2010/3/10 Tom Hawkins
: On Wed, Mar 10, 2010 at 8:07 AM, Warren Henning
wrote: Wow. Quite ambitious.
Was this inspired by work at your current employer like with Atom and some of the other stuff you've released?
Yes, we had an immediate need to debug some machine code. I looked around, but all the emulators I found (PSIM, et al.) were too complicated.
I'm also intrigued by the emphasis on software verification at the object code level for aerospace (DO-178). I figure better tools in this area may open the door to using advanced design methods like Atom for avionics. Of course it's unlikely this project will reach that level of maturity, but you never know.
We wrote the debugger and simulator for AVR line of microcontroller cores.
We used a DSEL to describe inner workings of commands and now try to apply it to ARM ISA.
The Haskell code is heavy on the use of type-level computations and, especially, assiciated types. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (4)
-
John Van Enk
-
Serguey Zefirov
-
Tom Hawkins
-
Warren Henning