Howdy! Here are a few of my projects. I hope you find them enjoyable!
Noah was born on July 24th, 2007. He loves to sing songs, read books, play games, and go to the park.
... and a ton of other pictures.
ImProve is an imperative programming language embedded in Haskell. The intent of ImProve is to provide a restrictive language that can be easily verified with formal methods for safety critical and other high assurance applications.
Atom is a Haskell DSL for designing hard real-time embedded software. At Eaton, we use it for automotive control systems. Based on guarded atomic actions, and similar to software transactional memory, Atom enables highly concurrent programming without the need for mutex locking. In addition, Atom performs compile-time task scheduling and generates code with deterministic execution time and constant memory use, simplifying the process of timing verification and memory consumption in hard realtime applications. Without mutex locking and run-time task scheduling, Atom can eliminate the need and overhead of RTOSs for many embedded applications.
Atom's Formal Verifier (AFV) is model checker that can verify assertions of an iterative C program without test stimulus or simulation. Based on the Yices SMT solver, AFV can reason about programs with both floating point and integral types.
Mecha is a solid modeling language embedded in Haskell. Mecha has few features at this point, but the goal is a CAD tool for machine design.
A symbol library to diagram hydraulic systems with gschem schematic capture.
A Haskell library for instruction set simulation (ISS) and static analysis on PowerPC machine code.
A Makefile and collection of patches to build a GCC cross compiler (C, C++, Ada) for bare metal embedded PowerPC targets.
A Haskell library to parse and generate VCD files. Though intended for Verilog simulation, we found VCD great for logging and viewing live vehicle data transmitted over a CAN bus.
HTZAAR is an implementation of TZAAR, a 2-player abstract strategy game designed by Kris Burm for the GIPF series of games. HTZAAR currently has a very weak AI, but provides a reasonable interface for creating new AI strategies. HTZAAR can also pit AI versus AI.
Confluence is a functional hardware description language.
HDCaml is an HDL embedded in Objective Caml.