search

GaloisInc / ivory

The Ivory EDSL
http://ivorylang.org
BSD 3-Clause "New" or "Revised" License
396 stars 28 forks source link

Question: Is ivory ready for other microcontrollers? #55

Closed schell closed 9 years ago

schell commented 9 years ago

Forgive my naivety, from the description at http://ivorylang.org/ivory-libs.html it seems that writing to registers in ivory only works for the STM32F4?

Memory bounds are defined statically in Ivory.HW.STM32F4 according to the STM32F4 microcontroller memory map

I'd like to use ivory for a project with the teensy++ (AT90USB1286). What work needs to be done before this is a possibility?

Hodapp87 commented 9 years ago

I've been using Ivory on Nordic nRF51 (ARM Cortex-M0) since January or February. I've had to write C wrapper functions for some of the hardware-specific stuff and Nordic-specific APIs; that's about it.

schell commented 9 years ago

Cool, thanks - @Hodapp87, is your project open source? I've done FFI before but I'm not quite sure where to start with ivory (besides the tutorial).

Hodapp87 commented 9 years ago

@schell https://github.com/GaloisInc/ivory/tree/master/ivory-examples/examples is where I started from.

My project is not open source, unfortunately, though I may try to open-source certain parts of it. However, you can find me in the Freenode channel #haskell-embedded if you want to ask questions... I'm not one of the Galois experts, just a user, but I have been using Ivory day-to-day in a fairly large build.

schell commented 9 years ago

Great! Thank you :) :+1:

pchickey commented 9 years ago

Welcome! We're glad to see more people interested in using Ivory. The short answer is, yes, you can use Ivory on any microcontroller that a reasonably complete C99 compiler exists for.

The long answer: unfortunately, much of the documentation at ivorylang.org has become out of date. That particular comment refers to some static checking we used to do in the ivory-hw library to ensure that memory mapped IO reads and writes were always performed on valid addresses for that particular chip family. However, we never found a satisfying way to make this check modular (allow users could select their own safety check for whatever chip they were using), and in a year or more of developing code with the check in place it had never caught any programmer errors. So, we got rid of the check entirely, and presently the ivory-hw primitives will allow you to write to any memory address. The only assumption it makes about your system is that pointers are 32 bits.

So, to get started with Ivory on an AT90 or any other microcontroller, you can write Ivory programs to link against existing C that takes care of low level drivers, or you can optionally write your drivers in Ivory as well, using ivory-hw as a wrapper around read/write operations to memory-mapped IO. Examples of the latter are found in ivory-tower-stm32.

(as a fun side note, most of the ivory-hw library and related bitdata infastructure, as well as lots of the STM32 BSP, was written by James Bielman, who was previously at Synapse. Small world!)

As far as more support goes - I wasn't aware of #haskell-embedded but none of us at Galois tend to hang out on IRC, sorry. We are definitely happy to take questions and feedback from you (and all users) in github issues or via email!

schell commented 9 years ago

Thanks for the explanation, I appreciate it.