Platform Independent Petri Net Editor (PIPE) creates and analyses Petri Nets quickly, efficiently, and effectively. A key design feature is the modular approach adopted for analysis, enabling new modules to be written easily and powerfully, using built-in data layer methods for standard calculations. Six analysis modules are provided, including Invariant Analysis, State-Space Analysis (deadlock, etc.), and Simulation Analysis and Classification. PIPE adheres to the XML Petri net standard (PNML). The file format for saving and loading Petri Nets is extensible through the use of XSLT, the default being PNML.
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.
Covered is a Verilog code coverage utility that reads in a Verilog design and a generated VCD/LXT/FST dumpfile from that design and generates a coverage file that can be merged with other coverage files or used to create a coverage report. Covered also contains the GUI coverage report utility that reads in a coverage file to allow interactive coverage discovery. Areas of coverage measured by Covered are: line, toggle, memory, combinational logic, FSM state/state-transition and assertion coverage.
JSDAI is a toolkit around STEP or ISO 10303, the STandard for the Exchange of Product model data. It supports the Express data modelling language as defined in ISO 10303-11 and provides data exchange capabilities according to ISO 10303-21 STEP-file and ISO 10303-28 STEP-XML. JSDAI Runtime is an API according ISO 10303-22, the Standard Data Access Interface (SDAI) for the Java programming language, ISO 10303-27. JSDAI Developer is for the development of Express data models, including Express-G diagrams.
The Distributed Real-time Embedded Analysis Method (DREAM) is a tool and method for the real-time verification and performance estimation of distributed real-time embedded (DRE) systems. It focuses on the practical application of formal verification and timing analysis to real-time middleware.
The CBOLD framework is a set of C++ classes and related source code for capturing board-level electronic designs. It allows the designer to capture and process an electronic board-level design using a text editor (or IDE) and a C++ compiler. It provides a concise, intuitive notation for schematicless capture of board-level designs. Instead of entering a schematic into an EDA tool, the designer creates a C++ program that describes the design and the desired outputs. When the program is compiled and run, it verifies the legality of the design and writes output files (CAD layout netlist, bill of materials, FPGA constraint files, etc.) to disk. Code primarily consists of definitions of modules, which are analogous to pages of a schematic design.