diff --git a/.gitmodules b/.gitmodules
index 58c58a9..4ff4afd 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -10,3 +10,6 @@
 [submodule "test/formal/riscv-formal"]
 	path = test/formal/riscv-formal/riscv-formal
 	url = https://github.com/Wren6991/riscv-formal.git
+[submodule "example_soc/libfpga"]
+	path = example_soc/libfpga
+	url = https://github.com/Wren6991/libfpga.git
diff --git a/example_soc/fpga/fpga_icebreaker.f b/example_soc/fpga/fpga_icebreaker.f
new file mode 100644
index 0000000..823be01
--- /dev/null
+++ b/example_soc/fpga/fpga_icebreaker.f
@@ -0,0 +1,5 @@
+file fpga_icebreaker.v
+list ../soc/soc.f
+
+file ../libfpga/common/reset_sync.v
+file ../libfpga/common/fpga_reset.v
diff --git a/example_soc/fpga/fpga_icebreaker.v b/example_soc/fpga/fpga_icebreaker.v
new file mode 100644
index 0000000..0b840be
--- /dev/null
+++ b/example_soc/fpga/fpga_icebreaker.v
@@ -0,0 +1,68 @@
+/**********************************************************************
+ * DO WHAT THE FUCK YOU WANT TO AND DON'T BLAME US PUBLIC LICENSE     *
+ *                    Version 3, April 2008                           *
+ *                                                                    *
+ * Copyright (C) 2021 Luke Wren                                       *
+ *                                                                    *
+ * Everyone is permitted to copy and distribute verbatim or modified  *
+ * copies of this license document and accompanying software, and     *
+ * changing either is allowed.                                        *
+ *                                                                    *
+ *   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION  *
+ *                                                                    *
+ * 0. You just DO WHAT THE FUCK YOU WANT TO.                          *
+ * 1. We're NOT RESPONSIBLE WHEN IT DOESN'T FUCKING WORK.             *
+ *                                                                    *
+ *********************************************************************/
+
+// FPGA toplevel for ../soc/example_soc.v on an iCEBreaker dev board
+
+`default_nettype none
+
+module fpga_icebreaker (
+	input wire        clk_osc,
+
+	// No external trst_n as iCEBreaker can't easily drive it from FTDI, so we
+	// generate a pulse internally from FPGA PoR.
+    input  wire       tck,
+    input  wire       tms,
+    input  wire       tdi,
+    output wire       tdo,
+
+	output wire       uart_tx,
+	input  wire       uart_rx
+);
+
+wire clk_sys = clk_osc;
+wire rst_n_sys;
+wire trst_n;
+
+fpga_reset #(
+	.SHIFT (3)
+) rstgen (
+	.clk         (clk_sys),
+	.force_rst_n (1'b1),
+	.rst_n       (rst_n_sys)
+);
+
+reset_sync trst_sync_u (
+	.clk       (tck),
+	.rst_n_in  (rst_n_sys),
+	.rst_n_out (trst_n)
+);
+
+example_soc soc_u (
+	.clk     (clk_sys),
+	.rst_n   (rst_n_sys),
+
+	.tck     (tck),
+	.trst_n  (trst_n),
+	.tms     (tms),
+	.tdi     (tdi),
+	.tdo     (tdo),
+
+	.uart_tx (uart_tx),
+	.uart_rx (uart_rx)
+);
+
+endmodule
diff --git a/example_soc/libfpga b/example_soc/libfpga
new file mode 160000
index 0000000..dd4920f
--- /dev/null
+++ b/example_soc/libfpga
@@ -0,0 +1 @@
+Subproject commit dd4920f522ff9658ddfc49e9d0b8e3764ccc315f
diff --git a/example_soc/soc/example_soc.v b/example_soc/soc/example_soc.v
new file mode 100644
index 0000000..5a1199b
--- /dev/null
+++ b/example_soc/soc/example_soc.v
@@ -0,0 +1,412 @@
+/**********************************************************************
+ * DO WHAT THE FUCK YOU WANT TO AND DON'T BLAME US PUBLIC LICENSE     *
+ *                    Version 3, April 2008                           *
+ *                                                                    *
+ * Copyright (C) 2021 Luke Wren                                       *
+ *                                                                    *
+ * Everyone is permitted to copy and distribute verbatim or modified  *
+ * copies of this license document and accompanying software, and     *
+ * changing either is allowed.                                        *
+ *                                                                    *
+ *   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION  *
+ *                                                                    *
+ * 0. You just DO WHAT THE FUCK YOU WANT TO.                          *
+ * 1. We're NOT RESPONSIBLE WHEN IT DOESN'T FUCKING WORK.             *
+ *                                                                    *
+ *********************************************************************/
+
+// Example file integrating a Hazard3 processor, processor JTAG + debug
+// components, some memory and a UART.
+
+`default_nettype none
+
+module example_soc (
+	// System clock + reset
+	input wire               clk,
+	input wire               rst_n,
+
+	// JTAG port to RISC-V JTAG-DTM
+    input  wire              tck,
+    input  wire              trst_n,
+    input  wire              tms,
+    input  wire              tdi,
+    output wire              tdo,
+
+    // IO
+    output wire              uart_tx,
+    input  wire              uart_rx
+);
+
+localparam W_ADDR = 32;
+localparam W_DATA = 32;
+
+// ----------------------------------------------------------------------------
+// Processor debug
+
+// JTAG-DTM IDCODE, selected after TAP reset, would normally be a
+// JEP106-compliant ID
+localparam IDCODE = 32'hdeadbeef;
+
+wire              dmi_psel;
+wire              dmi_penable;
+wire              dmi_pwrite;
+wire [7:0]        dmi_paddr;
+wire [31:0]       dmi_pwdata;
+reg  [31:0]       dmi_prdata;
+wire              dmi_pready;
+wire              dmi_pslverr;
+
+
+// TCK-domain DTM logic can force a hard reset of the 
+wire dmihardreset_req;
+wire assert_dmi_reset = !rst_n || dmihardreset_req;
+wire rst_n_dmi;
+
+reset_sync dmi_reset_sync_u (
+	.clk       (clk),
+	.rst_n_in  (!assert_dmi_reset),
+	.rst_n_out (rst_n_dmi)
+);
+
+hazard3_jtag_dtm #(
+	.IDCODE (IDCODE)
+) inst_hazard3_jtag_dtm (
+	.tck              (tck),
+	.trst_n           (trst_n),
+	.tms              (tms),
+	.tdi              (tdi),
+	.tdo              (tdo),
+
+	.dmihardreset_req (dmihardreset_req),
+
+	.clk_dmi          (clk),
+	.rst_n_dmi        (rst_n_dmi),
+
+	.dmi_psel         (dmi_psel),
+	.dmi_penable      (dmi_penable),
+	.dmi_pwrite       (dmi_pwrite),
+	.dmi_paddr        (dmi_paddr),
+	.dmi_pwdata       (dmi_pwdata),
+	.dmi_prdata       (dmi_prdata),
+	.dmi_pready       (dmi_pready),
+	.dmi_pslverr      (dmi_pslverr)
+);
+
+localparam N_HARTS = 1;
+localparam XLEN = 32;
+
+wire                      sys_reset_req;
+wire                      sys_reset_done;
+wire [N_HARTS-1:0]        hart_reset_req;
+wire [N_HARTS-1:0]        hart_reset_done;
+
+wire [N_HARTS-1:0]        hart_req_halt;
+wire [N_HARTS-1:0]        hart_req_halt_on_reset;
+wire [N_HARTS-1:0]        hart_req_resume;
+wire [N_HARTS-1:0]        hart_halted;
+wire [N_HARTS-1:0]        hart_running;
+
+wire [N_HARTS*XLEN-1:0]   hart_data0_rdata;
+wire [N_HARTS*XLEN-1:0]   hart_data0_wdata;
+wire [N_HARTS-1:0]        hart_data0_wen;
+
+wire [N_HARTS*XLEN-1:0]   hart_instr_data;
+wire [N_HARTS-1:0]        hart_instr_data_vld;
+wire [N_HARTS-1:0]        hart_instr_data_rdy;
+wire [N_HARTS-1:0]        hart_instr_caught_exception;
+wire [N_HARTS-1:0]        hart_instr_caught_ebreak;
+
+hazard3_dm #(
+	.N_HARTS      (N_HARTS),
+	.NEXT_DM_ADDR (0)
+) dm (
+	.clk                         (clk),
+	.rst_n                       (rst_n),
+
+	.dmi_psel                    (dmi_psel),
+	.dmi_penable                 (dmi_penable),
+	.dmi_pwrite                  (dmi_pwrite),
+	.dmi_paddr                   (dmi_paddr),
+	.dmi_pwdata                  (dmi_pwdata),
+	.dmi_prdata                  (dmi_prdata),
+	.dmi_pready                  (dmi_pready),
+	.dmi_pslverr                 (dmi_pslverr),
+
+	.sys_reset_req               (sys_reset_req),
+	.sys_reset_done              (sys_reset_done),
+	.hart_reset_req              (hart_reset_req),
+	.hart_reset_done             (hart_reset_done),
+
+	.hart_req_halt               (hart_req_halt),
+	.hart_req_halt_on_reset      (hart_req_halt_on_reset),
+	.hart_req_resume             (hart_req_resume),
+	.hart_halted                 (hart_halted),
+	.hart_running                (hart_running),
+
+	.hart_data0_rdata            (hart_data0_rdata),
+	.hart_data0_wdata            (hart_data0_wdata),
+	.hart_data0_wen              (hart_data0_wen),
+
+	.hart_instr_data             (hart_instr_data),
+	.hart_instr_data_vld         (hart_instr_data_vld),
+	.hart_instr_data_rdy         (hart_instr_data_rdy),
+	.hart_instr_caught_exception (hart_instr_caught_exception),
+	.hart_instr_caught_ebreak    (hart_instr_caught_ebreak)
+);
+
+
+// Generate resynchronised reset for CPU based on upstream system reset and on
+// system/hart reset requests from DM.
+
+wire assert_cpu_reset = !rst_n || sys_reset_req || hart_reset_req[0];
+wire rst_n_cpu;
+
+reset_sync cpu_reset_sync (
+	.clk       (clk),
+	.rst_n_in  (!assert_cpu_reset),
+	.rst_n_out (rst_n_cpu)
+);
+
+// Still some work to be done on the reset handshake -- this ought to be
+// resynchronised to DM's reset domain here, and the DM should wait for a
+// rising edge after it has asserted the reset pulse, to make sure the tail
+// of the previous "done" is not passed on.
+assign sys_reset_done = rst_n_cpu;
+assign hart_reset_done = rst_n_cpu;
+
+// ----------------------------------------------------------------------------
+// Processor
+
+wire [W_ADDR-1:0] proc_haddr;
+wire              proc_hwrite;
+wire [1:0]        proc_htrans;
+wire [2:0]        proc_hsize;
+wire [2:0]        proc_hburst;
+wire [3:0]        proc_hprot;
+wire              proc_hmastlock;
+wire              proc_hready;
+wire              proc_hresp;
+wire [W_DATA-1:0] proc_hwdata;
+wire [W_DATA-1:0] proc_hrdata;
+
+wire uart_irq;
+
+// Processor instantiation. Parameters can be set here or by modifying
+// hazard3_config.vh. Turn on all the ISA support but ignore performance
+// options like faster multiply/divide.
+
+hazard3_cpu_1port #(
+	.RESET_VECTOR    (32'h2000_00c0),
+	.MTVEC_INIT      (32'h2000_0000),
+
+	.EXTENSION_C     (0),
+	.EXTENSION_M     (0),
+	.CSR_M_MANDATORY (1),
+	.CSR_M_TRAP      (1),
+	.CSR_COUNTER     (0), // also no counters cause they're whack
+	.DEBUG_SUPPORT   (1),
+
+	.NUM_IRQ         (1),
+
+	.MVENDORID_VAL   (32'h0),
+	.MARCHID_VAL     (32'h0),
+	.MIMPID_VAL      (32'h0),
+	.MHARTID_VAL     (32'h0)
+) cpu (
+	.clk                        (clk),
+	.rst_n                      (rst_n_cpu),
+
+	.ahblm_haddr                (proc_haddr),
+	.ahblm_hwrite               (proc_hwrite),
+	.ahblm_htrans               (proc_htrans),
+	.ahblm_hsize                (proc_hsize),
+	.ahblm_hburst               (proc_hburst),
+	.ahblm_hprot                (proc_hprot),
+	.ahblm_hmastlock            (proc_hmastlock),
+	.ahblm_hready               (proc_hready),
+	.ahblm_hresp                (proc_hresp),
+	.ahblm_hwdata               (proc_hwdata),
+	.ahblm_hrdata               (proc_hrdata),
+
+	.dbg_req_halt               (hart_req_halt),
+	.dbg_req_halt_on_reset      (hart_req_halt_on_reset),
+	.dbg_req_resume             (hart_req_resume),
+	.dbg_halted                 (hart_halted),
+	.dbg_running                (hart_running),
+
+	.dbg_data0_rdata            (hart_data0_rdata),
+	.dbg_data0_wdata            (hart_data0_wdata),
+	.dbg_data0_wen              (hart_data0_wen),
+
+	.dbg_instr_data             (hart_instr_data),
+	.dbg_instr_data_vld         (hart_instr_data_vld),
+	.dbg_instr_data_rdy         (hart_instr_data_rdy),
+	.dbg_instr_caught_exception (hart_instr_caught_exception),
+	.dbg_instr_caught_ebreak    (hart_instr_caught_ebreak),
+
+	.irq                        (uart_irq),
+
+	// Should provide timer and software-controllable IRQ at system level --
+	// not implemented in this basic SoC.
+	.soft_irq                   (1'b0),
+	.timer_irq                  (1'b0)
+);
+
+
+// ----------------------------------------------------------------------------
+// Bus fabric
+
+// - 128 kB SRAM (using SPRAMs) at 0x2000_0000
+// - UART at 0x4000_0000
+
+// AHBL layer
+
+wire               sram0_hready_resp;
+wire               sram0_hready;
+wire               sram0_hresp;
+wire [W_ADDR-1:0]  sram0_haddr;
+wire               sram0_hwrite;
+wire [1:0]         sram0_htrans;
+wire [2:0]         sram0_hsize;
+wire [2:0]         sram0_hburst;
+wire [3:0]         sram0_hprot;
+wire               sram0_hmastlock;
+wire [W_DATA-1:0]  sram0_hwdata;
+wire [W_DATA-1:0]  sram0_hrdata;
+
+wire               bridge_hready_resp;
+wire               bridge_hready;
+wire               bridge_hresp;
+wire [W_ADDR-1:0]  bridge_haddr;
+wire               bridge_hwrite;
+wire [1:0]         bridge_htrans;
+wire [2:0]         bridge_hsize;
+wire [2:0]         bridge_hburst;
+wire [3:0]         bridge_hprot;
+wire               bridge_hmastlock;
+wire [W_DATA-1:0]  bridge_hwdata;
+wire [W_DATA-1:0]  bridge_hrdata;
+
+
+ahbl_splitter #(
+	.N_PORTS     (2),
+	.ADDR_MAP    (64'h40000000_20000000),
+	.ADDR_MASK   (64'he0000000_e0000000)
+) splitter_u (
+	.clk (clk),
+	.rst_n (rst_n),
+
+	.src_hready_resp (proc_hready   ),
+	.src_hready      (proc_hready   ),
+	.src_hresp       (proc_hresp    ),
+	.src_haddr       (proc_haddr    ),
+	.src_hwrite      (proc_hwrite   ),
+	.src_htrans      (proc_htrans   ),
+	.src_hsize       (proc_hsize    ),
+	.src_hburst      (proc_hburst   ),
+	.src_hprot       (proc_hprot    ),
+	.src_hmastlock   (proc_hmastlock),
+	.src_hwdata      (proc_hwdata   ),
+	.src_hrdata      (proc_hrdata   ),
+
+	.dst_hready_resp ({bridge_hready_resp , sram0_hready_resp}),
+	.dst_hready      ({bridge_hready      , sram0_hready     }),
+	.dst_hresp       ({bridge_hresp       , sram0_hresp      }),
+	.dst_haddr       ({bridge_haddr       , sram0_haddr      }),
+	.dst_hwrite      ({bridge_hwrite      , sram0_hwrite     }),
+	.dst_htrans      ({bridge_htrans      , sram0_htrans     }),
+	.dst_hsize       ({bridge_hsize       , sram0_hsize      }),
+	.dst_hburst      ({bridge_hburst      , sram0_hburst     }),
+	.dst_hprot       ({bridge_hprot       , sram0_hprot      }),
+	.dst_hmastlock   ({bridge_hmastlock   , sram0_hmastlock  }),
+	.dst_hwdata      ({bridge_hwdata      , sram0_hwdata     }),
+	.dst_hrdata      ({bridge_hrdata      , sram0_hrdata     })
+);
+
+// APB layer
+
+wire        uart_psel;
+wire        uart_penable;
+wire        uart_pwrite;
+wire [15:0] uart_paddr;
+wire [31:0] uart_pwdata;
+wire [31:0] uart_prdata;
+wire        uart_pready;
+wire        uart_pslverr;
+
+ahbl_to_apb apb_bridge_u (
+	.clk               (clk),
+	.rst_n             (rst_n),
+
+	.ahbls_hready      (bridge_hready),
+	.ahbls_hready_resp (bridge_hready_resp),
+	.ahbls_hresp       (bridge_hresp),
+	.ahbls_haddr       (bridge_haddr),
+	.ahbls_hwrite      (bridge_hwrite),
+	.ahbls_htrans      (bridge_htrans),
+	.ahbls_hsize       (bridge_hsize),
+	.ahbls_hburst      (bridge_hburst),
+	.ahbls_hprot       (bridge_hprot),
+	.ahbls_hmastlock   (bridge_hmastlock),
+	.ahbls_hwdata      (bridge_hwdata),
+	.ahbls_hrdata      (bridge_hrdata),
+
+	.apbm_paddr        (uart_paddr),
+	.apbm_psel         (uart_psel),
+	.apbm_penable      (uart_penable),
+	.apbm_pwrite       (uart_pwrite),
+	.apbm_pwdata       (uart_pwdata),
+	.apbm_pready       (uart_pready),
+	.apbm_prdata       (uart_prdata),
+	.apbm_pslverr      (uart_pslverr)
+);
+
+// ----------------------------------------------------------------------------
+// Memory and peripherals
+
+// No preloaded bootloader -- just use the debugger! (the processor will
+// actually enter an infinite crash loop after reset if memory is
+// zero-initialised so don't leave the little guy hanging too long)
+
+ahb_sync_sram #(
+	.DEPTH (1 << 15) // 32k x 32 = 128 kB
+) sram0 (
+	.clk               (clk),
+	.rst_n             (rst_n),
+
+	.ahbls_hready_resp (sram0_hready_resp),
+	.ahbls_hready      (sram0_hready),
+	.ahbls_hresp       (sram0_hresp),
+	.ahbls_haddr       (sram0_haddr),
+	.ahbls_hwrite      (sram0_hwrite),
+	.ahbls_htrans      (sram0_htrans),
+	.ahbls_hsize       (sram0_hsize),
+	.ahbls_hburst      (sram0_hburst),
+	.ahbls_hprot       (sram0_hprot),
+	.ahbls_hmastlock   (sram0_hmastlock),
+	.ahbls_hwdata      (sram0_hwdata),
+	.ahbls_hrdata      (sram0_hrdata)
+);
+
+uart_mini uart_u (
+	.clk          (clk),
+	.rst_n        (rst_n),
+
+	.apbs_psel    (uart_psel),
+	.apbs_penable (uart_penable),
+	.apbs_pwrite  (uart_pwrite),
+	.apbs_paddr   (uart_paddr),
+	.apbs_pwdata  (uart_pwdata),
+	.apbs_prdata  (uart_prdata),
+	.apbs_pready  (uart_pready),
+	.apbs_pslverr (uart_pslverr),
+
+	.rx           (uart_rx),
+	.tx           (uart_tx),
+	.cts          (1'b0),
+	.rts          (/* unused */),
+	.irq          (uart_irq),
+	.dreq         (/* unused */)
+);
+
+endmodule
diff --git a/example_soc/soc/soc.f b/example_soc/soc/soc.f
new file mode 100644
index 0000000..e9343de
--- /dev/null
+++ b/example_soc/soc/soc.f
@@ -0,0 +1,14 @@
+# SoC integration file
+file example_soc.v
+
+# CPU + debug components
+list $HDL/hazard3.f
+list $HDL/debug/dtm/hazard3_jtag_dtm.f
+list $HDL/debug/dm/hazard3_dm.f
+
+# Generic SoC components from libfpga
+file ../libfpga/common/reset_sync.v
+list ../libfpga/peris/uart/uart.f
+list ../libfpga/mem/ahb_sync_sram.f
+list ../libfpga/busfabric/ahbl_crossbar.f
+file ../libfpga/busfabric/ahbl_to_apb.v
diff --git a/example_soc/synth/.gitignore b/example_soc/synth/.gitignore
new file mode 100644
index 0000000..df5a45d
--- /dev/null
+++ b/example_soc/synth/.gitignore
@@ -0,0 +1,10 @@
+srcs.mk
+*.blif
+*.asc
+*.hex
+*.bin
+*.json
+*.log
+*.config
+*.svf
+*.bit
diff --git a/example_soc/synth/Makefile b/example_soc/synth/Makefile
new file mode 100644
index 0000000..0320b99
--- /dev/null
+++ b/example_soc/synth/Makefile
@@ -0,0 +1,11 @@
+CHIPNAME=fpga_icebreaker
+DOTF=../fpga/fpga_icebreaker.f
+SYNTH_OPT=-retime
+
+DEVICE=up5k
+PACKAGE=sg48
+
+include $(SCRIPTS)/synth_ice40.mk
+
+prog: bit
+	iceprog $(CHIPNAME).bin
diff --git a/example_soc/synth/fpga_icebreaker.pcf b/example_soc/synth/fpga_icebreaker.pcf
new file mode 100644
index 0000000..83bcafa
--- /dev/null
+++ b/example_soc/synth/fpga_icebreaker.pcf
@@ -0,0 +1,35 @@
+# 12 MHz oscillator
+set_io clk_osc 35
+
+# JTAG is on FTDI B channel so it doesn't inadvertently assert flash CS pin
+# (usually UART would be on the B channel)
+set_io tck  6 # FTDI BDBUS0
+set_io tdi  9 # FTDI BDBUS1
+set_io tdo 18 # FTDI BDBUS2
+set_io tms 19 # FTDI BDBUS3
+
+# UART is moved over to FTDI A channel -- this means flash is inaccessible
+# (and stays in a quiescent state since CSn is disconnected and pulled high)
+set_io uart_rx 15 # FTDI ADBUS0, flash SCK, iCE SCK
+set_io uart_tx 14 # FTDI ADBUS1, flash MOSI, iCE SO (if jumper J15 connected)
+
+# SPI flash
+# set_io flash_mosi 14
+# set_io flash_miso 17
+# set_io flash_sclk 15
+# set_io flash_cs 16
+
+# # Buttons
+# set_io dpad_u 20 # Snapoff top
+# set_io dpad_d 18 # Snapoff bottom
+# set_io dpad_l 10 # Main board
+# set_io dpad_r 19 # Snapoff middle
+
+# # LEDs
+# set_io led[0] 37 # Green on main board
+# set_io led[1] 11 # Red on main board
+# set_io led[2] 26 # Middle on snapoff (L1)
+# set_io led[3] 27 # Left on snapoff   (L2)
+# set_io led[4] 25 # Right on snapoff  (L3)
+# set_io led[5] 23 # Top on snapoff    (L4)
+# set_io led[6] 21 # Bottom on snapoff (L5)
diff --git a/hdl/hazard3_cpu_1port.v b/hdl/hazard3_cpu_1port.v
index 005d261..6143e21 100644
--- a/hdl/hazard3_cpu_1port.v
+++ b/hdl/hazard3_cpu_1port.v
@@ -61,9 +61,9 @@ module hazard3_cpu_1port #(
 	output wire              dbg_instr_caught_ebreak,
 
 	// Level-sensitive interrupt sources
-	input wire [NUM_IRQ-1:0] irq,          // -> mip.meip
-	input wire               irq_software, // -> mip.msip
-	input wire               irq_timer     // -> mip.mtip
+	input wire [NUM_IRQ-1:0] irq,       // -> mip.meip
+	input wire               soft_irq,  // -> mip.msip
+	input wire               timer_irq  // -> mip.mtip
 );
 
 // ----------------------------------------------------------------------------