A barebones 64-bit RISC-V micro-controller class CPU, implementing the I(nteger), M(ul/div), C(ompressed) and K(ryptography) extensions.
Assertion-Based Formal Verification of an AHB2APB bridge, featuring SystemVerilog assertions, RTL designs, and detailed documentation including a final report and project progression presentation.
Formal AXI verification properties from the eXpect framework for secure SoC validation
Firmware-driven dual-die RV32 chiplet SoC with GCC/ISS co-verification, DMA/AES offload, UPF 4.0 low-power intent, async CDC, real UVM, formal, and open-source coverage.
Various IPs implemented in Verilog
Logic Analyzer IP Core
This project is a final project in my master studies and it's done in a team of 2 people, Petar Stamenkovic and myself.
Formal Verification of RVECC Error Correcting Code Hardware
Parameterized NxN systolic-array NPU for signed matrix multiplication, implemented in SystemVerilog RTL and verified using UVM, SVA, directed testing, formal verification, functional coverage, and multi-configuration regression.
This repository provides a verification IP for conducting exhaustive security verification for CHERI processors.
Uninterpreted functions examples
Deterministic, formally verified tick-to-trade engine in FPGA fabric — 5-cycle latency, zero CPU, proven fail-closed. SystemVerilog on Arty A7.
Formal (VC Formal FPV) and UVM verification of an 8-lane mixed-precision INT8/BF16/NVFP4 dot-product core, with a shared SystemVerilog golden reference across assertions and scoreboards.
A 5-stage pipelined RV32IM core with caches and branch prediction, verified with RISC-V Formal and Spike lockstep co-simulation, booting FreeRTOS and running CoreMark on a Nexys Video FPGA.
Formally verified vendor-neutral PCIe Gen5 / CXL Type-3 memory-expansion datapath. Unbounded k-induction safety proofs, two-clock CDC, and mutation-checked non-vacuity.
This is where I am putting first RISC-V RV32I single-cycle processor (in development)
8 SystemVerilog FIFO designs formally verified (SymbiYosys BMC + k-induction), mutation-tested, FPGA-characterized — green CI
To associate your repository with the formal-verification topic, visit your repo's landing page and select "manage topics."