Home / Resources
Projects
Here are listed my current/past projects which gave birth to useful resources. These might be software tools, tutorials, design/verification examples, etc.
- openCarac is an automated verification solution to characterize electronic designs using your favourite Spice simulator. It provides output files in HTML, LaTeX and GNU Octave scripts. Also, it comes with an API which unlocks extension and fitness to a particular purpose.
Proofs of Concepts
Here are some resources which I have written and which I like to use as a reminder when I work. These are mostly proofs of concepts, tested under Debian GNU/Linux.
Coq
- Examples of simple theorems based on
LTL_Coq
library - Definition of PSL operators as syntactic sugar for LTL
NuSMV
- Verify LTL properties on Verilog models with Verilog2SMV
- Walk the AST and access names of specifications with pyNUSMV
Python 3
- Instrumentation of firefox web browser with the marionette
- GUI script and image recognition with sikuliX
Spice
- Hardware/software co-simulation between C and Spice with swig and TCLSpice
- How to observe crosstalk between systems through simulation
TCL
Verilog
- Manipulation of icarus simulator with Verilog Programming Interface (VPI)
- Empower simulation with C++ and SystemC using Verilator
VHDL
- Hardware/software co-simulation between VHDL and C with ghdl and gcc
- Dynamic verification of PSL properties with ghdl
Xilinx Zynq-7000
- Interfacing software running on an ARM Cortex-A9 with FPGA Artix-7 using GPIO
- Fetch and execute software from an AXI slave with ARM Cortex-A9
no cookie, no javascript, no external resource, KISS!