diff --git a/.gitignore b/.gitignore
index 71fa228..487adcc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,6 +29,7 @@
 /testbench.gtkw
 /testbench.vcd
 /testbench.trace
+/testbench_verilator*
 /check.smt2
 /check.vcd
 /synth.log
diff --git a/scripts/icestorm/Makefile b/scripts/icestorm/Makefile
index b86995f..7672b41 100644
--- a/scripts/icestorm/Makefile
+++ b/scripts/icestorm/Makefile
@@ -1,74 +1,104 @@
-
 TOOLCHAIN_PREFIX = riscv32-unknown-elf-
 
+ICE40_SIM_CELLS=$(shell yosys-config --datdir/ice40/cells_sim.v)
+
+# set to 4 for simulation
+FIRMWARE_COUNTER_BITS=18
+
 all: example.bin
 
+## -------------------
+## firmware generation
+
 firmware.elf: firmware.S firmware.c firmware.lds
-	$(TOOLCHAIN_PREFIX)gcc -Os -ffreestanding -nostdlib -o firmware.elf firmware.S firmware.c \
-			--std=gnu99 -Wl,-Bstatic,-T,firmware.lds,-Map,firmware.map,--strip-debug -lgcc
-	chmod -x firmware.elf
+	$(TOOLCHAIN_PREFIX)gcc \
+		-DSHIFT_COUNTER_BITS=$(FIRMWARE_COUNTER_BITS) \
+		-march=rv32i -Os -ffreestanding -nostdlib \
+		-o $@ firmware.S firmware.c \
+		--std=gnu99 -Wl,-Bstatic,-T,firmware.lds,-Map,firmware.map,--strip-debug
+	chmod -x $@
 
 firmware.bin: firmware.elf
-	$(TOOLCHAIN_PREFIX)objcopy -O binary firmware.elf firmware.bin
-	chmod -x firmware.bin
+	$(TOOLCHAIN_PREFIX)objcopy -O binary $< $@
+	chmod -x $@
 
 firmware.hex: firmware.bin
-	python3 ../../firmware/makehex.py firmware.bin 128 > firmware.hex
+	python3 ../../firmware/makehex.py $< 128 > $@
 
-synth.blif: example.v ../../picorv32.v firmware.hex
-	yosys -v3 -l synth.log -p 'synth_ice40 -top top -blif $@; write_verilog -attr2comment synth.v' $(filter %.v, $^)
+## ------------------------------
+## main flow: synth/p&r/bitstream
 
-example.asc: synth.blif
-	arachne-pnr -d 8k -o example.asc -p example.pcf synth.blif
+synth.json: example.v ../../picorv32.v firmware.hex
+	yosys -v3 -l synth.log -p 'synth_ice40 -top top -json $@; write_verilog -attr2comment synth.v' $(filter %.v, $^)
+
+example.asc: synth.json example.pcf
+	nextpnr-ice40 --hx8k --package ct256 --json $< --pcf example.pcf --asc $@
 
 example.bin: example.asc
-	icepack example.asc example.bin
+	icepack $< $@
 
-example_tb.vvp: example_tb.v example.v firmware.hex
-	iverilog -o example_tb.vvp -s testbench example.v example_tb.v ../../picorv32.v
-	chmod -x example_tb.vvp
+## -----------------
+## icarus simulation
+
+example_tb.vvp: example.v example_tb.v ../../picorv32.v firmware.hex
+	iverilog -o $@ -s testbench $(filter %.v, $^)
+	chmod -x $@
 
 example_sim: example_tb.vvp
-	vvp -N example_tb.vvp
+	vvp -N $<
 
 example_sim_vcd: example_tb.vvp
-	vvp -N example_tb.vvp +vcd
+	vvp -N $< +vcd
 
-synth_tb.vvp: example_tb.v synth.blif
-	iverilog -o synth_tb.vvp -s testbench synth.v example_tb.v `yosys-config --datdir/ice40/cells_sim.v`
-	chmod -x synth_tb.vvp
+## ---------------------
+## post-synth simulation
+
+synth_tb.vvp: example_tb.v synth.json
+	iverilog -o $@ -s testbench synth.v example_tb.v $(ICE40_SIM_CELLS)
+	chmod -x $@
 
 synth_sim: synth_tb.vvp
-	vvp -N synth_tb.vvp
+	vvp -N $<
 
 synth_sim_vcd: synth_tb.vvp
-	vvp -N synth_tb.vvp +vcd
+	vvp -N $< +vcd
 
-route.v: example.asc
-	icebox_vlog -L -n top -sp example.pcf example.asc > route.v
+## ---------------------
+## post-route simulation
 
-route_tb.vvp: example_tb.v route.v
-	iverilog -o route_tb.vvp -s testbench route.v example_tb.v `yosys-config --datdir/ice40/cells_sim.v`
-	chmod -x route_tb.vvp
+route.v: example.asc example.pcf
+	icebox_vlog -L -n top -sp example.pcf $< > $@
+
+route_tb.vvp: route.v example_tb.v
+	iverilog -o $@ -s testbench $^ $(ICE40_SIM_CELLS)
+	chmod -x $@
 
 route_sim: route_tb.vvp
-	vvp -N route_tb.vvp
+	vvp -N $<
 
 route_sim_vcd: route_tb.vvp
-	vvp -N route_tb.vvp +vcd
+	vvp -N $< +vcd
 
-prog_sram:
-	iceprog -S example.bin
+## ---------------------
+## miscellaneous targets
 
-view:
-	gtkwave example.vcd example.gtkw
+prog_sram: example.bin
+	iceprog -S $<
+
+timing: example.asc example.pcf
+	icetime -c 62 -tmd hx8k -P ct256 -p example.pcf -t $<
+
+view: example.vcd
+	gtkwave $< example.gtkw
+
+## ------
+## el fin
 
 clean:
 	rm -f firmware.elf firmware.map firmware.bin firmware.hex
-	rm -f synth.log synth.v synth.blif route.v example.asc example.bin
+	rm -f synth.log synth.v synth.json route.v example.asc example.bin
 	rm -f example_tb.vvp synth_tb.vvp route_tb.vvp example.vcd
 
 .PHONY: all prog_sram view clean
-.PHONY: example_sim synth_sim route_sim
+.PHONY: example_sim synth_sim route_sim timing
 .PHONY: example_sim_vcd synth_sim_vcd route_sim_vcd
-
diff --git a/scripts/icestorm/firmware.c b/scripts/icestorm/firmware.c
index a5e5236..80a4661 100644
--- a/scripts/icestorm/firmware.c
+++ b/scripts/icestorm/firmware.c
@@ -1,7 +1,8 @@
 #include <stdint.h>
 
-// use SHIFT_COUNTER_BITS=4 for simulation
-#define SHIFT_COUNTER_BITS 18
+#ifndef SHIFT_COUNTER_BITS
+#error SHIFT_COUNTER_BITS must be defined as 4 (for simulation) or 18 (for hardware bitstreams)!
+#endif
 
 void output(uint8_t c)
 {
diff --git a/scripts/icestorm/readme.md b/scripts/icestorm/readme.md
new file mode 100644
index 0000000..101391f
--- /dev/null
+++ b/scripts/icestorm/readme.md
@@ -0,0 +1,12 @@
+To build the example LED-blinking firmware for an HX8K Breakout Board and get
+a timing report (checked against the default 12MHz oscillator):
+
+    $ make clean example.bin timing
+
+To run all the simulation tests:
+
+    $ make clean example_sim synth_sim route_sim FIRMWARE_COUNTER_BITS=4
+
+(You must run the `clean` target to rebuild the firmware with the updated
+`FIRMWARE_COUNTER_BITS` parameter; the firmware source must be recompiled for
+simulation vs hardware, but this is not tracked as a Makefile dependency.)
diff --git a/shell.nix b/shell.nix
new file mode 100644
index 0000000..92ec1ff
--- /dev/null
+++ b/shell.nix
@@ -0,0 +1,139 @@
+# nix.shell: PicoRV32 Development Environment
+#
+# This file allows you to use the Nix Package Manager (https://nixos.org/nix)
+# in order to download, install, and prepare a working environment for doing
+# PicoRV32/PicoSoC development on _any_ existing Linux distribution, provided
+# the Nix package manager is installed.
+#
+# Current included tools:
+#
+#   - Synthesis: Recent Yosys and SymbiYosys
+#   - Place and Route: arachne-pnr and nextpnr (ICE40, ECP5, Python, no GUI)
+#   - Packing: Project IceStorm (Trellis tools may be included later?)
+#   - SMT Solvers: Z3 4.7.x, Yices 2.6.x, and Boolector 3.0.x
+#   - Verification: Recent Verilator, Recent (unreleased) Icarus Verilog
+#   - A bare-metal RISC-V cross compiler toolchain, based on GCC 8.2.x
+#
+# With these tools, you can immediately begin development, simulation, firmware
+# hacking, etc with almost no need to fiddle with recent tools yourself. Almost
+# all of the tools will be downloaded on-demand (except the GCC toolchain)
+# meaning you don't have to compile any recent tools yourself. Due to the
+# "hermetic" nature of Nix, these packages should also work on practically any
+# Linux distribution, as well.
+#
+# (This environment should also be suitable for running riscv-formal test
+# harnesses on PicoRV32, as well. In fact it is probably useful for almost
+# _any_ RTL implementation of the RV32I core.)
+#
+# Usage
+# -----
+#
+# At the top-level of the picorv32 directory, simply run the 'nix-shell' command,
+# which will then drop you into a bash prompt:
+#
+#
+#     $ nix-shell
+#     ...
+#     [nix-shell:~/src/picorv32]$
+#
+#
+# When you run 'nix-shell', you will automatically begin downloading all of the
+# various tools you need from an upstream "cache", so most of this will execute
+# very quickly. However, this may take a while, as you will at least have to
+# build a cross-compiled RISC-V toolchain, which may take some time. (These
+# binaries are not available from the cache, so they must be built by you.) Once
+# you have done this once, you do not need to do it again.
+#
+# At this point, once you are inside the shell, you can begin running tests
+# like normal. For example, to run the Verilator tests with the included test
+# firmware, which is substantially faster than Icarus:
+#
+#     [nix-shell:~/src/picorv32]$ make test_verilator TOOLCHAIN_PREFIX=riscv32-unknown-elf-
+#     ...
+#
+#
+# Note that you must override TOOLCHAIN_PREFIX (in the top-level Makefile, it
+# looks in /opt by default).
+#
+# This will work immediately with no extra fiddling necessary. You can also run
+# formal verification tests using a provided SMT solver, for example, yices and
+# boolector (Z3 is not used since it does not complete in a reasonable amount
+# of time for these examples):
+#
+#     [nix-shell:~/src/picorv32]$ make check-yices check-boolector
+#     ...
+#
+# You can also run the PicoSoC tests and build bitstreams. To run the
+# simulation tests and then build bitstreams for the HX8K and IceBreaker
+# boards:
+#
+#     [nix-shell:~/src/picorv32]$ cd picosoc/
+#     [nix-shell:~/src/picorv32/picosoc]$ make hx8ksynsim icebsynsim
+#     ...
+#     [nix-shell:~/src/picorv32/picosoc]$ make hx8kdemo.bin icebreaker.bin
+#     ...
+#
+# The HX8K simulation and IceBreaker simulation will be synthesized with Yosys
+# and then run with Icarus Verilog. The bitstreams for HX8K and IceBreaker will
+# be P&R'd with arachne-pnr and nextpnr, respectively.
+#
+
+{ architecture ? "rv32imc"
+}:
+
+# TODO FIXME: fix this to a specific version of nixpkgs.
+# ALSO: maybe use cachix to make it easier for contributors(?)
+with import <nixpkgs> {};
+
+let
+  # risc-v toolchain source code. TODO FIXME: this should be replaced with
+  # upstream versions of GCC. in the future we could also include LLVM (the
+  # upstream nixpkgs LLVM expression should be built with it in time)
+  riscv-toolchain-ver = "8.2.0";
+  riscv-src = pkgs.fetchFromGitHub {
+    owner  = "riscv";
+    repo   = "riscv-gnu-toolchain";
+    rev    = "c3ad5556197e374c25bc475ffc9285b831f869f8";
+    sha256 = "1j9y3ai42xzzph9rm116sxfzhdlrjrk4z0v4yrk197j72isqyxbc";
+    fetchSubmodules = true;
+  };
+
+  # given an architecture like 'rv32i', this will generate the given
+  # toolchain derivation based on the above source code.
+  make-riscv-toolchain = arch:
+    stdenv.mkDerivation rec {
+      name    = "riscv-${arch}-toolchain-${version}";
+      version = "${riscv-toolchain-ver}-${builtins.substring 0 7 src.rev}";
+      src     = riscv-src;
+
+      configureFlags   = [ "--with-arch=${arch}" ];
+      installPhase     = ":"; # 'make' installs on its own
+      hardeningDisable = [ "all" ];
+      enableParallelBuilding = true;
+
+      # Stripping/fixups break the resulting libgcc.a archives, somehow.
+      # Maybe something in stdenv that does this...
+      dontStrip = true;
+      dontFixup = true;
+
+      nativeBuildInputs = with pkgs; [ curl gawk texinfo bison flex gperf ];
+      buildInputs = with pkgs; [ libmpc mpfr gmp expat ];
+    };
+
+  riscv-toolchain = make-riscv-toolchain architecture;
+
+  # These are all the packages that will be available inside the nix-shell
+  # environment.
+  buildInputs = with pkgs;
+    # these are generally useful packages for tests, verification, synthesis
+    # and deployment, etc
+    [ python3 gcc
+      yosys symbiyosys nextpnr arachne-pnr icestorm
+      z3 boolector yices
+      verilog verilator
+      # also include the RISC-V toolchain
+      riscv-toolchain
+    ];
+
+# Export a usable shell environment
+in runCommand "picorv32-shell" { inherit buildInputs; } ""