Open-Source EDA Tools

my-dma-ip/
├── rtl/                  # Synthesisable RTL source
│   ├── axi4_dma_top.sv
│   ├── axi4_dma_engine.sv
│   └── axi4_dma_irq.sv
├── tb/                   # Testbenches (not shipped to customer)
│   ├── tb_top.sv
│   └── test_m2m.sv
├── cocotb/               # Python testbenches
│   ├── Makefile
│   └── test_dma.py
├── formal/               # SymbiYosys property files
│   └── dma_props.sby
├── synth/                # Synthesis scripts
│   └── synth.tcl
├── docs/                 # Datasheet, app notes
│   └── datasheet.pdf
├── .gitignore
└── README.md

# Initialise a new IP repo
git init my-dma-ip && cd my-dma-ip
git remote add origin https://github.com/yourname/my-dma-ip.git

# Daily workflow
git status                        # see what changed
git diff rtl/axi4_dma_engine.sv  # see exact line changes
git add rtl/axi4_dma_engine.sv   # stage specific file (not git add .)
git commit -m "fix: AXI burst length calculation for 128-bit mode"
git push

# Feature branch — never work directly on main
git checkout -b feature/scatter-gather
# ... make changes, test ...
git checkout main
git merge feature/scatter-gather

# Tag a release for customer delivery
git tag -a v1.2.0 -m "AXI4-DMA v1.2.0 — adds scatter-gather, 128-bit support"
git push origin v1.2.0

# .gitignore — exclude simulation artifacts
echo "*.vcd
*.fst
*.log
obj_dir/
__pycache__/
*.pyc" > .gitignore

// 8-bit up counter with synchronous reset
module counter #(
  parameter int WIDTH = 8
)(
  input  logic             clk,
  input  logic             rst_n,    // active-low reset
  input  logic             en,       // count enable
  output logic [WIDTH-1:0] count,
  output logic             overflow  // pulses for 1 cycle on wrap
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      count    <= '0;
      overflow <= 1'b0;
    end else if (en) begin
      {overflow, count} <= count + 1'b1;
    end else begin
      overflow <= 1'b0;
    end
  end
endmodule

`timescale 1ns/1ps

module tb_counter;
  // DUT signals
  logic       clk = 0;
  logic       rst_n, en;
  logic [7:0] count;
  logic       overflow;

  // Clock: 10ns period (100 MHz)
  always #5 clk = ~clk;

  // Instantiate DUT
  counter #(.WIDTH(8)) dut (
    .clk(clk), .rst_n(rst_n), .en(en),
    .count(count), .overflow(overflow)
  );

  // VCD dump — opens in GTKWave
  initial begin
    $dumpfile("waves/counter.vcd");
    $dumpvars(0, tb_counter);
  end

  // Stimulus
  initial begin
    rst_n = 0; en = 0;
    repeat(3) @(posedge clk);  // hold reset for 3 cycles
    rst_n = 1;

    // Count up from 0
    en = 1;
    repeat(300) @(posedge clk);   // watch overflow at 255→0

    // Pause counting
    en = 0;
    repeat(10) @(posedge clk);

    // Resume
    en = 1;
    repeat(50) @(posedge clk);

    $display("SIMULATION DONE — open waves/counter.vcd in GTKWave");
    $finish;
  end

  // Self-check: catch X state on count
  always @(posedge clk) begin
    if (rst_n && ^count === 1'bx)
      $error("X-state detected on count at time %0t", $time);
  end
endmodule

# Create output directory
mkdir -p waves

# Compile RTL + TB into a simulation binary
iverilog -g2012 -o sim.out rtl/counter.sv tb/tb_counter.v

# Run the simulation
vvp sim.out

# Output:
# SIMULATION DONE — open waves/counter.vcd in GTKWave

# Common flags:
#  -g2012    : enable SystemVerilog-2012 features (always_ff, logic, etc.)
#  -Wall     : enable all warnings
#  -I rtl/   : add include path for `include files
#  -D VERBOSE: define a preprocessor macro

# With multiple RTL files:
iverilog -g2012 -o sim.out \
  rtl/counter.sv \
  rtl/another_module.sv \
  tb/tb_counter.v

# Open the VCD file directly
gtkwave waves/counter.vcd

# Or open with a saved signal layout (.gtkw file):
gtkwave waves/counter.vcd --rcvar "do_initial_zoom_fit yes"

// In your testbench — use FST for 5–10× smaller files
initial begin
  $dumpfile("waves/counter.fst");
  $dumpvars(0, tb_counter);
end

// Then compile with: iverilog -g2012 -DFST -o sim.out rtl/counter.sv tb/tb_counter.v
// gtkwave handles both .vcd and .fst natively

# Run Verilator as a linter — catches mistakes before simulation
verilator --lint-only -Wall rtl/counter.sv

# Common lint warnings to fix immediately:
#   UNUSED     — declared but never used signal (often a typo)
#   UNDRIVEN   — signal never assigned (bug — will be X in sim)
#   WIDTH      — mismatched bus widths in assignment
#   CASEINCOMPLETE — case statement missing values (FSM holes)
#   LATCH      — unintended latch inferred from combinational block

# Suppress a specific warning when intentional:
verilator --lint-only -Wall -Wno-UNUSED rtl/counter.sv

#include "Vcounter.h"        // Verilator auto-generates this
#include "verilated.h"
#include "verilated_vcd_c.h"

int main(int argc, char **argv) {
    Verilated::commandArgs(argc, argv);
    Vcounter *dut = new Vcounter;

    // VCD tracing
    Verilated::traceEverOn(true);
    VerilatedVcdC *tfp = new VerilatedVcdC;
    dut->trace(tfp, 99);
    tfp->open("waves/counter.vcd");

    // Reset
    dut->rst_n = 0; dut->en = 0; dut->clk = 0;
    for (int i = 0; i < 6; i++) {
        dut->clk = !dut->clk;
        dut->eval();
        tfp->dump(i * 5);
    }
    dut->rst_n = 1;

    // Run for 1000 clock cycles
    uint64_t t = 30;
    dut->en = 1;
    for (int i = 0; i < 2000; i++) {
        dut->clk = !dut->clk;
        dut->eval();
        tfp->dump(t);
        t += 5;
        // Simple self-check
        if (dut->clk && dut->overflow)
            printf("Overflow at cycle %d, count=%d\n", i/2, dut->count);
    }

    tfp->close();
    delete dut;
    printf("Simulation done. Open waves/counter.vcd in GTKWave.\n");
    return 0;
}

mkdir -p waves

# Step 1: Verilator builds C++ from the RTL
verilator --cc --trace -Wall rtl/counter.sv --exe tb/sim_main.cpp

# Step 2: Compile the generated C++ to a fast binary
make -C obj_dir -f Vcounter.mk Vcounter -j$(nproc)

# Step 3: Run
./obj_dir/Vcounter
# Output: Overflow at cycle 127, count=0
#         Overflow at cycle 383, count=0  (etc.)
#         Simulation done. Open waves/counter.vcd in GTKWave.

import cocotb
from cocotb.clock import Clock
from cocotb.triggers import RisingEdge, Timer, FallingEdge
from cocotb.result import TestFailure

@cocotb.test()
async def test_reset_clears_count(dut):
    """Count must be 0 after reset, regardless of any prior state."""
    clock = Clock(dut.clk, 10, units="ns")  # 100 MHz
    cocotb.start_soon(clock.start())

    dut.rst_n.value = 0
    dut.en.value = 0
    await Timer(50, units="ns")
    await RisingEdge(dut.clk)

    assert dut.count.value == 0, f"Expected 0 after reset, got {dut.count.value}"
    dut._log.info("PASS: reset test")

@cocotb.test()
async def test_count_increments(dut):
    """Counter increments by 1 each enabled clock cycle."""
    clock = Clock(dut.clk, 10, units="ns")
    cocotb.start_soon(clock.start())

    dut.rst_n.value = 0
    await Timer(30, units="ns")
    dut.rst_n.value = 1
    dut.en.value = 1

    for expected in range(1, 20):
        await RisingEdge(dut.clk)
        await FallingEdge(dut.clk)  # sample after clock edge settles
        actual = int(dut.count.value)
        assert actual == expected, f"Cycle {expected}: expected {expected} got {actual}"

    dut._log.info("PASS: increment test (20 cycles)")

@cocotb.test()
async def test_overflow_flag(dut):
    """Overflow must pulse exactly at 255→0 wrap."""
    clock = Clock(dut.clk, 10, units="ns")
    cocotb.start_soon(clock.start())

    dut.rst_n.value = 0
    await Timer(30, units="ns")
    dut.rst_n.value = 1
    dut.en.value = 1

    # Fast-forward to just before overflow
    for _ in range(254):
        await RisingEdge(dut.clk)

    await RisingEdge(dut.clk)  # cycle 255 → overflow
    await FallingEdge(dut.clk)
    assert dut.overflow.value == 1, "Expected overflow=1 at wrap"

    await RisingEdge(dut.clk)  # next cycle — overflow should clear
    await FallingEdge(dut.clk)
    assert dut.overflow.value == 0, "Expected overflow=0 after wrap cycle"

    dut._log.info("PASS: overflow flag test")

@cocotb.test()
async def test_enable_holds_count(dut):
    """Count must not change when en=0."""
    clock = Clock(dut.clk, 10, units="ns")
    cocotb.start_soon(clock.start())

    dut.rst_n.value = 0
    await Timer(30, units="ns")
    dut.rst_n.value = 1
    dut.en.value = 1

    # Count up to 50
    for _ in range(50):
        await RisingEdge(dut.clk)

    # Pause
    dut.en.value = 0
    frozen_count = int(dut.count.value)
    for _ in range(20):
        await RisingEdge(dut.clk)
        assert int(dut.count.value) == frozen_count, "Count changed while en=0!"

    dut._log.info(f"PASS: enable hold test (count frozen at {frozen_count})")

SIM       ?= icarus          # or: verilator, vcs, xcelium
TOPLEVEL_LANG ?= verilog

VERILOG_SOURCES  = $(PWD)/../rtl/counter.sv
TOPLEVEL         = counter
MODULE           = test_counter

include $(shell cocotb-config --makefiles)/Makefile.sim

cd cocotb

# Run all tests with Icarus Verilog backend
make SIM=icarus

# Run with Verilator (faster for large designs)
make SIM=verilator

# Run a specific test only
make SIM=icarus TESTCASE=test_overflow_flag

# Output (all passing):
# test_reset_clears_count           PASS
# test_count_increments             PASS
# test_overflow_flag                PASS
# test_enable_holds_count           PASS
# --- 4 passed in 0.82s ---

# Launch yosys interactive shell
yosys

# Inside yosys shell:
read_verilog -sv rtl/counter.sv    # read the RTL
hierarchy -check -top counter      # set top module, check hierarchy
proc                               # convert always blocks to netlists
opt                                # basic optimisation pass
stat                               # print gate count
show                               # open a graphical view (requires xdot)
exit

# Full synthesis script for the counter
yosys -import

# 1. Read RTL
read_verilog -sv ../rtl/counter.sv

# 2. Set top module and check
hierarchy -check -top counter

# 3. Run full synthesis (generic cells)
synth -top counter

# 4. Print statistics — gate count, flip-flop count, memory
stat

# 5. Write output netlist
write_verilog -noattr synth_out/counter_netlist.v

# To target Sky130 standard cells:
# read_liberty -lib /path/to/sky130_fd_sc_hd__tt_025C_1v80.lib
# abc -liberty  /path/to/sky130_fd_sc_hd__tt_025C_1v80.lib
# write_verilog -noattr synth_out/counter_sky130.v

mkdir -p synth_out

# Run the script
yosys synth/synth_counter.tcl

# Expected stat output (generic cells):
# === counter ===
#    Number of wires:              12
#    Number of cells:              11
#      $_DFF_PP0_                   9    ← 9 flip-flops (8-bit count + overflow)
#      $_NOT_                       1
#      $_XOR_                       1
#    Number of cells (excluding ...): 11

// Formal properties — compiled only during formal flow, not synthesis
`ifdef FORMAL

  // 1. After reset, count must be zero
  prop_reset_zero: assert property (
    @(posedge clk) !rst_n |=> (count == '0)
  );

  // 2. When disabled, count must never change
  prop_no_count_when_disabled: assert property (
    @(posedge clk) disable iff (!rst_n)
    !en |=> $stable(count)
  );

  // 3. Overflow must only pulse when count wraps 255→0
  prop_overflow_only_on_wrap: assert property (
    @(posedge clk) disable iff (!rst_n)
    overflow |-> ($past(count) == 8'hFF && en)
  );

  // 4. Count must never be X while out of reset
  prop_no_x: assert property (
    @(posedge clk) rst_n |-> !$isunknown(count)
  );

  // Cover: make sure count actually reaches 255 (reachability)
  cov_max_count: cover property (
    @(posedge clk) count == 8'hFF
  );

`endif

[options]
mode prove         # prove assertions hold for all time (unbounded)
# mode bmc         # bounded model check: try to find bug within N cycles
# depth 30         # number of steps for bmc mode

[engines]
smtbmc boolector   # use Boolector SMT solver (fast for bit-vector problems)
# smtbmc z3       # Z3 solver — more powerful but slower
# aiger avy       # for sequential miter checks

[script]
read -formal rtl/counter.sv
read -formal rtl/counter_props.sv
prep -top counter

[files]
rtl/counter.sv
rtl/counter_props.sv

# Run formal proof
sby -f formal/counter.sby

# Successful output:
# [prop_reset_zero]             PROVED (depth 2)
# [prop_no_count_when_disabled] PROVED (depth 5)
# [prop_overflow_only_on_wrap]  PROVED (depth 258)
# [prop_no_x]                   PROVED (depth 1)
# [cov_max_count]               COVERED (in 256 steps)
# SBY ... DONE (PASS)

# If a property FAILS, sby creates a counterexample VCD:
# gtkwave formal/counter/engine_0/trace.vcd

name: RTL Verification CI

on:
  push:
    branches: [main, develop]
  pull_request:
    branches: [main]

jobs:
  lint:
    name: Verilator Lint
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install Verilator
        run: sudo apt-get install -y verilator
      - name: Lint RTL
        run: verilator --lint-only -Wall rtl/counter.sv

  simulate-iverilog:
    name: iverilog Simulation
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install iverilog
        run: sudo apt-get install -y iverilog
      - name: Compile and simulate
        run: |
          mkdir -p waves
          iverilog -g2012 -o sim.out rtl/counter.sv tb/tb_counter.v
          vvp sim.out

  cocotb-tests:
    name: cocotb Regression
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: actions/setup-python@v5
        with:
          python-version: '3.11'
      - name: Install deps
        run: pip install cocotb iverilog
      - name: Install iverilog (system)
        run: sudo apt-get install -y iverilog
      - name: Run cocotb tests
        run: make SIM=icarus
        working-directory: cocotb

  synthesise:
    name: Yosys Synthesis (Gate Count)
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install Yosys
        run: sudo apt-get install -y yosys
      - name: Synthesise
        run: |
          mkdir -p synth_out
          yosys synth/synth_counter.tcl

  formal-verify:
    name: SymbiYosys Formal Proof
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - name: Install OSS CAD Suite
        run: |
          curl -L https://github.com/YosysHQ/oss-cad-suite-build/releases/latest/download/oss-cad-suite-linux-x64-latest.tgz | tar xz -C $HOME
          echo "$HOME/oss-cad-suite/bin" >> $GITHUB_PATH
      - name: Run formal verification
        run: sby -f formal/counter.sby