[Haskell-cafe] ANN: powerpc-0.0.1

[Tom Hawkins]

On Wed, Mar 10, 2010 at 8:07 AM, Warren Henning
<warren.henning at gmail.com> 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.

-Tom


>
> Warren
>
> On Tue, Mar 9, 2010 at 10:35 PM, Tom Hawkins <tomahawkins at gmail.com> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>