Fix HDL links

diff --git a/crypto_router_asic.mdwn b/crypto_router_asic.mdwn
index c91ffd490dc2605a18be9d086c6092fc3706e067..b752e2ecc3e59defb14f987bff0cf538f7dc9da0 100644 (file)
--- a/crypto_router_asic.mdwn
+++ b/crypto_router_asic.mdwn
@@ -35,22 +35,25 @@ The implementation is scattered within the simulator code, which is available at
 <https://git.libre-soc.org/?p=openpower-isa.git;a=tree;hb=HEAD>
 
 Unit tests are available at:
-[bigint](https://git.libre-soc.org/?p=openpower-isa.git;a=tree;f=src/openpower/test/bigint;h=38c2ffe30becb7f580053d0aa3a41beca1312567;hb=HEAD) and
-[bitmanip](https://git.libre-soc.org/?p=openpower-isa.git;a=tree;f=src/openpower/test/bitmanip;h=916950f9e62fd9dac0373b925eaf15199bc7c8ab;hb=HEAD)
 
-**3) Reference HDL implementation of some instructions**
-
-Code and tests are available at:
-
-* [Implementation of Galois Field instructions](https://git.libre-soc.org/?p=nmigen-gf.git;a=tree;f=src/nmigen_gf/hdl;hb=bc0c03b3df2fa19189aaa2b61a101cdc8ebf1beb)
-* [Test cases and formal tests for Galois Field instructions](https://git.libre-soc.org/?p=nmigen-gf.git;a=tree;f=src/nmigen_gf/hdl/test;hb=bc0c03b3df2fa19189aaa2b61a101cdc8ebf1beb)
-* [Ternlogi bitmanip implementation](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/shift_rot/main_stage.py;h=b8ec704199a800c6df652524612581e07d885bb2;hb=880bf8469c65dbb96c9853b32618d07a0c742cf0#l93)
-* [Grev bitmanip implementation](https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/grev.py;h=2b22fe1bf35ba3e5f2787b62bbf36c329a444787;hb=HEAD)
 * [Test cases for bitmanip instructions](https://git.libre-soc.org/?p=openpower-isa.git;a=blob;f=src/openpower/test/bitmanip/bitmanip_cases.py;h=93476025fc31dc5d42d4a86a27d4b826810436e2;hb=HEAD)
 * [Test cases for bigint instructions](https://git.libre-soc.org/?p=openpower-isa.git;a=blob;f=src/openpower/test/bigint/bigint_cases.py;h=2944ad431e586dca1b572f4be4c1a9c7a3e82e89;hb=HEAD)
 
+**3) Reference HDL implementation of some instructions**
+
 (full implemention was not possible within limited 2021-02-051 budget [[nlnet_2021_crypto_router]])
 
+Code and tests are available:
+
+* [HDL Implementation of Galois Field instructions](https://git.libre-soc.org/?p=nmigen-gf.git;a=tree;f=src/nmigen_gf/hdl;hb=bc0c03b3df2fa19189aaa2b61a101cdc8ebf1beb)
+* [Unit test and formal verification for the HDL implementation of Galois Field instructions](https://git.libre-soc.org/?p=nmigen-gf.git;a=tree;f=src/nmigen_gf/hdl/test;hb=bc0c03b3df2fa19189aaa2b61a101cdc8ebf1beb)
+* [HDL implementation of Ternlogi bitmanip instruction](https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/lut.py;h=755747ab2073dbf1a7620f9ac31e592b2bf63a44;hb=HEAD)
+* [HDL implementation of Grev bitmanip instruction](https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/grev.py;h=2b22fe1bf35ba3e5f2787b62bbf36c329a444787;hb=HEAD)
+* [Unit test for the HDL implementation of Ternlogi](https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/test/test_lut.py;h=e0a98099460ded8912299b05c513dc0f924005d7;hb=HEAD)
+* [Unit test for the HDL implementation of Grev](https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/test/test_grev.py;h=780239d8a13b2954a7953d5d2e312dd517a80347;hb=HEAD)
+* [Formal verification for the HDL implementation of Ternlogi](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/shift_rot/formal/proof_main_stage.py;h=379211d623a01259f77c90229cae0d57f40228a7;hb=HEAD#l311)
+* [Formal verification for the HDL implementation of Grev](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/shift_rot/formal/proof_main_stage.py;h=379211d623a01259f77c90229cae0d57f40228a7;hb=HEAD#l321)
+
 * additional specification of and simulation for concepts like a REMAP engine and element width
 overrides which, when implemented also in HDL, will allow hyper-efficient acceleration of many
 fundamental crypto algorithms. (implemented 100% in simulator, allowing 100% successful implementation of Simple-V-PowerISA assembler to be made, but limited budget of 2021-02-051 was insufficient to complete HDL implementation of REMAP and elwidths)