gEDA is a suite of electronic design automation (EDA) tools. Currently, the project offers a mature suite of free software applications for electronics design, including schematic capture, attribute management, bill of materials (BOM) generation, netlisting into over 20 netlist formats, analog and digital simulation, and printed circuit board (PCB) layout.
TkGate is an event-driven digital circuit simulator with a TCL/Tk-based graphical editor. It supports a wide range of primitive circuit elements and user-defined modules for hierarchical design. The distribution comes with a number of tutorial and example circuits which can be loaded through the "Help" menu, and the example circuits include a simple CPU, programmed to run the Animals game. TkGate has multi-lingual support for English, Japanese, French, German, Spanish, Welsh, and Catalan.
Piklab is an integrated development environment for applications based on PIC and dsPIC microcontrollers. Supported compilers are: the Small Device C Compiler, the GNU PIC Utilities, PICC compilers, the PIC30 toolchain, the C18 compiler, the JAL and JALV2 compilers, the CSC compiler, and the Boost compilers. Supported programmers: ICD2, PICkit, PICkit2, PicStart+, and most direct programmers. Supported debuggers: ICD2 and GPSim. A commandline programmer/debugger is also provided.
ACL2 is a mathematical logic, programming language, and mechanical theorem prover based on the applicative subset of Common Lisp. It is an "industrial-strength" version of the NQTHM or Boyer/Moore theorem prover, and has been used for the formal verification of commercial microprocessors, the Java Virtual Machine, interesting algorithms, and so forth.