verification info
diff --git a/INFO.md b/INFO.md
index 9abbc17..af6c510 100644
--- a/INFO.md
+++ b/INFO.md
@@ -69,70 +69,14 @@
 
     make user_project_wrapper
 
-## Simulations
+To build the GDS and run the simulations, you will need to install the Sky130 PDK and OpenLane tool.
+It takes about 5 minutes and needs about 3GB of disk space.
 
-### Scan controller
+    export PDK_ROOT=<some dir>/pdk
+    export OPENLANE_ROOT=<some dir>/openlane
+    cd <the root of this repo>
+    make setup 
 
-There are some testbenches that you can use to check the scan chain and controller is working.
-The default of 498 projects takes a very long time to simulate, so I advise overriding the configuration first:
+## Verification
 
-    # fetch the test projects
-    ./configure.py --test --update-projects
-    # rebuild config with only 20 projects
-    ./configure.py --test --update-caravel --limit 20
-
-Then run the test:
-
-    cd verilog/dv/scan_controller
-    # you will also need to set your PDK_ROOT environment variable
-    make test_scan_controller
-
-The Gate Level simulation requires scan_controller and user_project_wrapper to be re-hardened to get the correct gate level netlists: 
-
-* Edit openlane/scan_controller/config.tcl and change NUM_DESIGNS=498 to NUM_DESIGNS=20.
-* Then from the top level directory:
-
-    make scan_controller
-    make user_project_wrapper
-
-* Then run the GL test
-
-    cd verilog/dv/scan_controller
-    make test_scan_controller_gl
-
-### Top level test: internal control
-
-Uses the scan controller.
-
-    cd verilog/dv/scan_controller_int
-    make coco_test
-
-### Top level test: external control
-
-Uses external signals to control the scan chain.
-
-    cd verilog/dv/scan_controller_ext
-    make coco_test
-
-### Top level test: logic analyser control
-
-Uses the RISCV co-processor to drive the scanchain with firmware.
-
-    cd verilog/dv/scan_controller_la
-    make coco_test
-
-## Dev notes
-
-* PDN hang issues https://github.com/The-OpenROAD-Project/OpenLane/issues/1173
-* Also discovered PDN hangs if extra lefs/defs are not deduplicated
-* with PDN set so dense, tapeout job fails with density checks
-* with unused PDN straps turned off, precheck fails
-* copied the erased version (just power rings) and deleted the first digital power rings, copy pasted that over final gds
-* precheck fails with missing power ports
-* manually added missing power ports to gl verilog of user_project_wrapper
-* precheck passes. Will try tapeout job
-* tapeout job failed with DRC, was because outer power ring was too thin. I think due to configuration rather than being cutoff for precheck
-* updated missing_power_rings with correct rings and repeated, this time tapeout passes
-* Tim suggests doing this as a module/cell to make it easier to reproduce
-* Maximo suggests editing pdn_cfg.tcl and using the -nets option with add_pdn_stripe to force only 1st voltage domain
-* This worked, see the new openlane/user_project_wrapper/pdn_cfg.tcl config
+See the separate [verification](verification.md) doc.
diff --git a/README.md b/README.md
index e8fb6d6..be25ba2 100644
--- a/README.md
+++ b/README.md
@@ -11,154 +11,6 @@
 
 # Project Index
 
-* [339501025136214612](https://wokwi.com/projects/339501025136214612) https://github.com/mattvenn/wokwi_filler
-* [339688086163161683](https://wokwi.com/projects/339688086163161683) https://github.com/mattvenn/tinytapeout_m_segments
-* [340218629792465491](https://wokwi.com/projects/340218629792465491) https://github.com/gregdavill/tinytapeout_spin0
-* [340318610245288530](https://wokwi.com/projects/340318610245288530) https://github.com/mole99/wokwi-1bit-alu
-* [340285391309374034](https://wokwi.com/projects/340285391309374034) https://github.com/ericsmi/tinytapeout_popcnt.git
-* [340661930553246290](https://wokwi.com/projects/340661930553246290) https://github.com/krasin/wokwi-guess-my-number
-* [341136771628663380](https://wokwi.com/projects/341136771628663380) https://github.com/johshoff/barrelshifter-wokwi-gds
-* [339800239192932947](https://wokwi.com/projects/339800239192932947) https://github.com/pretentious7/tinytapeout
-* [341154161238213203](https://wokwi.com/projects/341154161238213203) https://github.com/GuzTech/wokwi-ripple-carry-adder
-* [341159915403870803](https://wokwi.com/projects/341159915403870803) https://github.com/kbeckmann/tinytapeout_kbeckmann1
-* [341154068332282450](https://wokwi.com/projects/341154068332282450) https://github.com/H-S-S-11/tinytapeout-verilog-test
-* [341160201697624660](https://wokwi.com/projects/341160201697624660) https://github.com/skerr92/tinytapeout_frequency_div
-* [341163800289870419](https://wokwi.com/projects/341163800289870419) https://github.com/argunda/tinytapeout_dualedgedetector
-* [341160271679586899](https://wokwi.com/projects/341160271679586899) https://github.com/libokuohai/tinytapeout-2022-08
-* [341161378978988626](https://wokwi.com/projects/341161378978988626) https://github.com/jglim/tinytapeout_bcd-dec
-* [341152580068442706](https://wokwi.com/projects/341152580068442706) https://github.com/jglim/tinytapeout_bcd-7seg
-* [341155178824598098](https://wokwi.com/projects/341155178824598098) https://github.com/tkuester/wokwi-directghost
-* [341167691532337747](https://wokwi.com/projects/341167691532337747) https://github.com/shahzaibk23/tinytapeout-barrel-shifter
-* [341178154799333971](https://wokwi.com/projects/341178154799333971) https://github.com/tcptomato/tinytapeout
-* [341178481588044372](https://wokwi.com/projects/341178481588044372) https://github.com/DaveyPocket/chaser
-* [341176884318437971](https://wokwi.com/projects/341176884318437971) https://github.com/GuzTech/tinytapeout-4x4-multiplier
-* [341182944314917460](https://wokwi.com/projects/341182944314917460) https://github.com/derhexenmeister/tinytapeout_nco
-* [341188777753969234](https://wokwi.com/projects/341188777753969234) https://github.com/mbalestrini/tinytapeout_rgb_lut_test
-* [341194143598379604](https://wokwi.com/projects/341194143598379604) https://github.com/derhexenmeister/tinytapeout_updwnbcd
-* [341205508016833108](https://wokwi.com/projects/341205508016833108) https://github.com/bradysalz/pll_tiny_tapeout_demo
-* [341162950004834900](https://wokwi.com/projects/341162950004834900) https://github.com/pramitpal/tinytapeout_pramit
-* [341202178192441940](https://wokwi.com/projects/341202178192441940) https://github.com/gregdavill/tinytapeout-verilog-fifo
-* [341191836498395731](https://wokwi.com/projects/341191836498395731) https://github.com/gregdavill/tinytapeout-wokwi-74x1G00
-* [341192113929585235](https://wokwi.com/projects/341192113929585235) https://github.com/gregdavill/tinytapeout-wokwi-74x1G02
-* [341192621088047698](https://wokwi.com/projects/341192621088047698) https://github.com/gregdavill/tinytapeout-wokwi-74xG198
-* [340579111348994642](https://wokwi.com/projects/340579111348994642) https://github.com/gregdavill/tinytapeout-verilog-7seg-clock
-* [341224613878956628](https://wokwi.com/projects/341224613878956628) https://github.com/alanvgreen/tinytapeout4bitadder
-* [341235973870322258](https://wokwi.com/projects/341235973870322258) https://github.com/benlaurie/twistedringcounter
-* [341235575572922964](https://wokwi.com/projects/341235575572922964) https://github.com/sureshsugumar/tinytapeout_counter
-* [341164910646919762](https://wokwi.com/projects/341164910646919762) https://github.com/daniestevez/tinytapeout-verilog
-* [341233739099013714](https://wokwi.com/projects/341233739099013714) https://github.com/pkuligowski/tinytapeout_tmr
-* [341240110454407762](https://wokwi.com/projects/341240110454407762) https://github.com/chiplet/tinytapeout-snake
-* [341264068701586004](https://wokwi.com/projects/341264068701586004) https://github.com/derhexenmeister/tinytapeout_pwm
-* [341164228775772755](https://wokwi.com/projects/341164228775772755) https://github.com/raha96/tinycharacters-locked
-* [341262321634509394](https://wokwi.com/projects/341262321634509394) https://github.com/nathancheek/tinytapeout-loop
-* [341174563322724948](https://wokwi.com/projects/341174563322724948) https://github.com/andars/universal-turing-machine-w5s8
-* [341271902949474898](https://wokwi.com/projects/341271902949474898) https://github.com/vmunoz82/tinytapeout_euler1
-* [bc4d7220e4fdbf20a574d56ea112a8e1](https://wokwi.com/projects/bc4d7220e4fdbf20a574d56ea112a8e1) https://github.com/mikenet213/mikenet213-tt1-verilog
-* [341178296293130834](https://wokwi.com/projects/341178296293130834) https://github.com/veremenko-y/tinytapeout-ue14500
-* [1f985e14df1ed789231bb6e0189d6e39](https://wokwi.com/projects/1f985e14df1ed789231bb6e0189d6e39) https://github.com/mikenet213/mikenet213-tt2-verilog
-* [341277789473735250](https://wokwi.com/projects/341277789473735250) https://github.com/aiunderstand/tinytapeout_asyncbinterconvcomp.git
-* [341263346544149074](https://wokwi.com/projects/341263346544149074) https://github.com/smunaut/tinytapeout-fifo
-* [341296149788885588](https://wokwi.com/projects/341296149788885588) https://github.com/nwtechguy/tinytapeout_BCD_counter
-* [341332847867462227](https://wokwi.com/projects/341332847867462227) https://github.com/kambadur/bcd_to_7seg
-* [341337976625693266](https://wokwi.com/projects/341337976625693266) https://github.com/bieganski/tinytapeout_bieganski
-* [341339883600609876](https://wokwi.com/projects/341339883600609876) https://github.com/TomKeddie/tinytapeout-2022-1
-* [341344337258349139](https://wokwi.com/projects/341344337258349139) https://github.com/r-a-hoggarth/tinytapeGaloisLFSR
-* [341342096033055316](https://wokwi.com/projects/341342096033055316) https://github.com/adamgreig/tinytapeout-prn
-* [341259651269001812](https://wokwi.com/projects/341259651269001812) https://github.com/ianloic/tinytapeout-1
-* [341353928049295956](https://wokwi.com/projects/341353928049295956) https://github.com/sad-electronics/tinytapeout-clock-divider-asic
-* [341353780122485332](https://wokwi.com/projects/341353780122485332) https://github.com/gatecat/tinytapeout-lutram-test
-* [341193419111006803](https://wokwi.com/projects/341193419111006803) https://github.com/tommythorn/tinytapeout-4-bit-cpu
-* [341266732010177108](https://wokwi.com/projects/341266732010177108) https://github.com/wokwi/tt-game-of-life-cell-popcnt
-* [341353777861755476](https://wokwi.com/projects/341353777861755476) https://github.com/gatecat/tinytapeout-srlut-test
-* [341359404107432531](https://wokwi.com/projects/341359404107432531) https://github.com/AdDraw/tinytapeout_demo
-* [341315210433266259](https://wokwi.com/projects/341315210433266259) https://github.com/cpldcpu/tinydice
-* [341364381657858642](https://wokwi.com/projects/341364381657858642) https://github.com/cpldcpu/tinytapeout_mcpu6bit
-* [341279123277087315](https://wokwi.com/projects/341279123277087315) https://github.com/azzeloof/tinytapeout-counter
-* [341802655228625490](https://wokwi.com/projects/341802655228625490) https://github.com/mattvenn/tinytapeout-341802655228625490
-* [341382703379120723](https://wokwi.com/projects/341382703379120723) https://github.com/mwelling/led-blaster
-* [341389786199622227](https://wokwi.com/projects/341389786199622227) https://github.com/mwelling/figure-8
-* [341404507891040852](https://wokwi.com/projects/341404507891040852) https://github.com/gatecat/tinytapeout-fpga-test
-* [341410909669818963](https://wokwi.com/projects/341410909669818963) https://github.com/cfib/trafficlight-fsm
-* [341063825089364563](https://wokwi.com/projects/341063825089364563) https://github.com/clj/tinytapeout-verilog-7seg-figure-eight
-* [341174480471589458](https://wokwi.com/projects/341174480471589458) https://github.com/smunaut/tinytapeout-misc-1
-* [341419328215712339](https://wokwi.com/projects/341419328215712339) https://github.com/regymm/tinytapeout-funnyblinky
-* [341431339142087251](https://wokwi.com/projects/341431339142087251) https://github.com/Sirawit7205/tinytapeout-2G57-2G58
-* [341432030163108435](https://wokwi.com/projects/341432030163108435) https://github.com/Sirawit7205/tinytapeout-2G97-2G98
-* [341440114308678227](https://wokwi.com/projects/341440114308678227) https://github.com/hosein-mokarian/tinytapeout_counter_3to8_decoder
-* [341496918381167187](https://wokwi.com/projects/341496918381167187) https://github.com/burtyb/srld
-* [341440781874102868](https://wokwi.com/projects/341440781874102868) https://github.com/Mahnoor-ismail01/tinytapeout-chromatic-3-to-8-Decoder
-* [341444501414347346](https://wokwi.com/projects/341444501414347346) https://github.com/Shahzaib2028/tinytapeout-4to2Encoder-2to4Decoder
-* [019235602376235615](https://wokwi.com/projects/019235602376235615) https://github.com/sfmth/tinytapeout-tinycordic
-* [341450853309219412](https://wokwi.com/projects/341450853309219412) https://github.com/mm21/tinytapeout-led-matrix
-* [341438392303616596](https://wokwi.com/projects/341438392303616596) https://github.com/jeanthom/tinytapout-lock
-* [341432284947153491](https://wokwi.com/projects/341432284947153491) https://github.com/AidanMedcalf/tinytapeout-tinyio
-* [341457971277988435](https://wokwi.com/projects/341457971277988435) https://github.com/ElectricPotato/tinytapeout-hello-world-uart
-* [341399568412312147](https://wokwi.com/projects/341399568412312147) https://github.com/abdullahkhalids/TinyTapeout-hamming-code
-* [341464767397888596](https://wokwi.com/projects/341464767397888596) https://github.com/hossein1387/tinytapeout-verilog-test
-* [341476989274686036](https://wokwi.com/projects/341476989274686036) https://github.com/ChrisPVille/tinytapeout-FROG4bitCPU
-* [341482086419399252](https://wokwi.com/projects/341482086419399252) https://github.com/Talha-Ahmed-1/tinytapeout_flop_regfile
-* [341452019534398035](https://wokwi.com/projects/341452019534398035) https://github.com/skylersaleh/tinytapeout-hello
-* [341497971083313748](https://wokwi.com/projects/341497971083313748) https://github.com/proppy/tinytapeout-xls-popcount
-* [341497964482527828](https://wokwi.com/projects/341497964482527828) https://github.com/proppy/tinytapeout-xls-popcount-bithacks
-* [341497938559631956](https://wokwi.com/projects/341497938559631956) https://github.com/proppy/tinytapeout-xls-inverter
-* [341499976001520211](https://wokwi.com/projects/341499976001520211) https://github.com/mark64/tinytapeout
-* [341500800901579348](https://wokwi.com/projects/341500800901579348) https://github.com/dave-roo/ddcomparatorandro
-* [341493393195532884](https://wokwi.com/projects/341493393195532884) https://github.com/splinedrive/tinytapeout-verilog-4x4-multiplier
-* [341506274933867090](https://wokwi.com/projects/341506274933867090) https://github.com/ThorKn/tinytapeout_shiftregister_8bit
-* [341449297858921043](https://wokwi.com/projects/341449297858921043) https://github.com/UDXS/tinytapeout-sqrt
-* [341710255833481812](https://wokwi.com/projects/341710255833481812) https://github.com/coralmw/tinytapeout-css-feedback
-* [340067262721426004](https://wokwi.com/projects/340067262721426004) https://github.com/ericsmi/tinytapeout-verilog-div3
-* [341462925422101075](https://wokwi.com/projects/341462925422101075) https://github.com/fluxfocus/jdtt-logic1.git
-* [341520747710120530](https://wokwi.com/projects/341520747710120530) https://github.com/anm/nyasic
-* [341423712597181012](https://wokwi.com/projects/341423712597181012) https://github.com/aiunderstand/tinytapeout_bintristateloadablecounter
-* [341516949939814994](https://wokwi.com/projects/341516949939814994) https://github.com/ThorKn/tinytapeout_shiftregister_challenge
-* [341521390605697619](https://wokwi.com/projects/341521390605697619) https://github.com/regymm/tinytapeout-mcpi
-* [341243232292700755](https://wokwi.com/projects/341243232292700755) https://github.com/todd1251/tinytapeout-figure8
-* [341519170869920338](https://wokwi.com/projects/341519170869920338) https://github.com/CyberGai/tinytapeout-bcd-counter
-* [341446083683025490](https://wokwi.com/projects/341446083683025490) https://github.com/georgeyhere/tinytapeout-dice-roller
-* [341524192738411090](https://wokwi.com/projects/341524192738411090) https://github.com/nayanesh-reddy/2-Bit_Add_Mul_Comp
-* [341533740987581011](https://wokwi.com/projects/341533740987581011) https://github.com/ryancor/half_addr_asic
-* [341431502448362067](https://wokwi.com/projects/341431502448362067) https://github.com/hovind/tinytapeout-verilog-test
-* [341473139924927058](https://wokwi.com/projects/341473139924927058) https://github.com/siriusm46/tinytapeout_bcd_decimal
-* [341528610027340372](https://wokwi.com/projects/341528610027340372) https://github.com/cpldcpu/tinytapeout_mcpu5
-* [341424636358034002](https://wokwi.com/projects/341424636358034002) https://github.com/goran-mahovlic/tinytapeout-verilog-piano
-* [341717091617866324](https://wokwi.com/projects/341717091617866324) https://github.com/andars/universal-turing-machine-aw7s8
-* [hamming74](https://wokwi.com/projects/hamming74) https://github.com/marcusmueller/hamming74-tapeout
-* [341541108650607187](https://wokwi.com/projects/341541108650607187) https://github.com/13arn/tinytapeout_counter_steamdeck
-* [341360223723717202](https://wokwi.com/projects/341360223723717202) https://github.com/johshoff/tinytapeout-verilog
-* [341546888233747026](https://wokwi.com/projects/341546888233747026) https://github.com/cy384/seven-segment-with-adder
-* [340979268609638995](https://wokwi.com/projects/340979268609638995) https://github.com/georgerennie/tinytapeout-wokwi-cd4518
-* [341542971476279892](https://wokwi.com/projects/341542971476279892) https://github.com/ElectricPotato/tinytapeout-picture-printer-b
-* [341556236196512338](https://wokwi.com/projects/341556236196512338) https://github.com/theFestest/tinytapeout-simple-invert8
-* [341558189536313940](https://wokwi.com/projects/341558189536313940) https://github.com/ArsenioDev/CustomSiliconTest
-* [341538994733974098](https://wokwi.com/projects/341538994733974098) https://github.com/mgargano/tinytapeout_alu_with_4bit_7segmetdisplay_decoder
-* [341557831870186068](https://wokwi.com/projects/341557831870186068) https://github.com/theFestest/tinytapeout-4x4-ram
-* [341569483755749970](https://wokwi.com/projects/341569483755749970) https://github.com/michael-christen/wokwi-verilog-asic-experiment
-* [341573751072096850](https://wokwi.com/projects/341573751072096850) https://github.com/craigcc-frii/tinytapeout_craig
-* [341571228858843732](https://wokwi.com/projects/341571228858843732) https://github.com/youngpines/r2rdac_tinytapeout_demo
-* [341490465660469844](https://wokwi.com/projects/341490465660469844) https://github.com/toybuilder/learn-tinytapeout
-* [341581732833657427](https://wokwi.com/projects/341581732833657427) https://github.com/eggsactly/tinytapeout_demo
-* [341457494561784402](https://wokwi.com/projects/341457494561784402) https://github.com/gsegura96/tinytapeout-chisel
-* [341590933015364178](https://wokwi.com/projects/341590933015364178) https://github.com/abf149/fbna_like_verilog_abf149
-* [341589685194195540](https://wokwi.com/projects/341589685194195540) https://github.com/MC-SecPat/tinytapeout_chi2shares
-* [341608574336631379](https://wokwi.com/projects/341608574336631379) https://github.com/MC-SecPat/tinytapeout_chi3shares
-* [341608297106768466](https://wokwi.com/projects/341608297106768466) https://github.com/Adil8442/tiny_tapeout_test
-* [341802448429515346](https://wokwi.com/projects/341802448429515346) https://github.com/mattvenn/tinytapeout-341802448429515346
-* [341609034095264340](https://wokwi.com/projects/341609034095264340) https://github.com/r4d10n/tinytapeout-HELLo-3orLd-7seg
-* [341617722294010450](https://wokwi.com/projects/341617722294010450) https://github.com/proppy/tinytapeout-xls-graydec
-* [341613097060926036](https://wokwi.com/projects/341613097060926036) https://github.com/prabaldutta/tinytapeout_adi
-* [341614346808328788](https://wokwi.com/projects/341614346808328788) https://github.com/maehw/wokwi-verilog-gds-wolf-goat-cabbage
-* [341620484740219475](https://wokwi.com/projects/341620484740219475) https://github.com/ThorKn/tinytapeout_pattern_player
-* [341624400621077076](https://wokwi.com/projects/341624400621077076) https://github.com/rigobertoruiz98/cts_fsm
-* [341614536664547922](https://wokwi.com/projects/341614536664547922) https://github.com/rajarshiroy/tinytapout0_rajarshi
-* [341567111632519764](https://wokwi.com/projects/341567111632519764) https://github.com/BarsMonster/MicroASIC
-* [341631485498884690](https://wokwi.com/projects/341631485498884690) https://github.com/cpldcpu/TinyTapeout_TrainLED
-* [341632596577354323](https://wokwi.com/projects/341632596577354323) https://github.com/malkam03/tinytapeout-game-of-life
-* [341628725785264722](https://wokwi.com/projects/341628725785264722) https://github.com/BarsMonster/MicroAsicV
-* [341631511790879314](https://wokwi.com/projects/341631511790879314) https://github.com/maehw/wokwi-verilog-gds-lowspeed-tiny-uart
-* [341426151397261906](https://wokwi.com/projects/341426151397261906) https://github.com/smunaut/tinytapeout-smolram
-* [341629415144292948](https://wokwi.com/projects/341629415144292948) https://github.com/sirejdua/6bit-cellular-automata-tinytapeout
-* [341637831098106450](https://wokwi.com/projects/341637831098106450) https://github.com/DuaneSand/TinyTapeout-Hello
-* [341631644820570706](https://wokwi.com/projects/341631644820570706) https://github.com/tzachari/tinytapeout-lab11
-* [340596276030603858](https://wokwi.com/projects/340596276030603858) https://github.com/mattvenn/tinytapeout-marc
-* [341678527574180436](https://wokwi.com/projects/341678527574180436) https://github.com/mattvenn/tinytapeout-laura
+* [339501025136214612](https://wokwi.com/projects/339501025136214612) https://github.com/mattvenn/tinytapeout-test-straight
+* [340805072482992722](https://wokwi.com/projects/340805072482992722) https://github.com/mattvenn/tinytapeout-7seg-seconds-counter
+* [341535056611770964](https://wokwi.com/projects/341535056611770964) https://github.com/mattvenn/tinytapeout-test-invert
diff --git a/verification.md b/verification.md
new file mode 100644
index 0000000..ed1756d
--- /dev/null
+++ b/verification.md
@@ -0,0 +1,77 @@
+# Verification
+
+* Simulation of some test projects at RTL and GL level. 
+* Simulation of the whole chip with scan controller, external controller, logic analyser.
+* Formal verification that each small project's scan chain is correct.
+* Formal verification that the correct signals are passed through for the 3 different scan chain control modes.
+
+# Timing constraints
+
+* [Each small project has a negedge flop flop at the end of the shift register to reclock the data](https://github.com/mattvenn/wokwi-verilog-gds-test/blob/17f106db36f022536d013b960316bcc7f02c572c/template/scan_wrapper.v#L67). This gives more hold margin.
+* [Each small project has SDC timing constraints](https://github.com/mattvenn/wokwi-verilog-gds-test/blob/main/src/base.sdc)
+* [Scan controller](https://github.com/mattvenn/tinytapeout-mpw7/blob/aacae16304f4a4878943a49fd479d8a284736e32/verilog/rtl/scan_controller/scan_controller.v#L334) uses a shift register clocked with the end of the chain to ensure correct data is captured.
+* [Scan controller has its own SDC timing constraints](openlane/scan_controller/base.sdc)
+
+## Simulations
+
+There are some testbenches that you can use to check the scan chain and controller is working.
+The default of 498 projects takes a very long time to simulate, so I advise overriding the configuration first:
+
+    # fetch the test projects
+    ./configure.py --test --update-projects
+    # rebuild config with only 20 projects
+    ./configure.py --test --update-caravel --limit 20
+
+### Scan controller
+
+This test only instantiates user_project_wrapper (which contains all the small projects). It doesn't simulate the rest of the ASIC.
+
+    cd verilog/dv/scan_controller
+    make test_scan_controller
+
+The Gate Level simulation requires scan_controller and user_project_wrapper to be re-hardened to get the correct gate level netlists: 
+
+* Edit openlane/scan_controller/config.tcl and change NUM_DESIGNS=498 to NUM_DESIGNS=20.
+* Then from the top level directory:
+
+    make scan_controller
+    make user_project_wrapper
+
+* Then run the GL test
+
+    cd verilog/dv/scan_controller
+    make test_scan_controller_gl
+
+### Top level test: internal control
+
+Uses the scan controller.
+
+    cd verilog/dv/scan_controller_int
+    make coco_test
+
+### Top level test: external control
+
+Uses external signals to control the scan chain.
+
+    cd verilog/dv/scan_controller_ext
+    make coco_test
+
+### Top level test: logic analyser control
+
+Uses the RISCV co-processor to drive the scanchain with firmware.
+
+    cd verilog/dv/scan_controller_la
+    make coco_test
+
+## Formal Verification
+
+## Scan chain
+
+Each GL netlist for each small project is proven to be equivalent to the reference scan chain implementation.
+The verification is done on the GL netlist, so an RTL version of the cells used needed to be created.
+See [here for more info](tinytapeout_scan/README.md).
+
+## Scan controller MUX
+
+In case the internal scan controller doesn't work, we also have ability to control the chain from external pins or the Caravel Logic Analyser.
+We implement a simple MUX to achieve this and [formally prove it is correct](verilog/rtl/scan_controller/properties.v).