* [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)
-* a flexible HDL platform (ls2) for implementing a System-on-Chip on an FPGA or ASIC
+**4) Additional specification of and simulation for concepts like a REMAP engine
+and element width overrides**
+
+These, when implemented also in HDL, will allow hyper-efficient acceleration of
+many fundamental crypto algorithms.
+
+* [REMAP documentation](https://libre-soc.org/openpower/sv/remap/)
+* [Element width overrides documentation](https://libre-soc.org/openpower/sv/overview/#elwidths)
+
+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.)
+
+**5) A flexible self-contained HDL platform (ls2) for implementing a System-on-Chip
+on an FPGA or ASIC**
+
+* [Documentation](/HDL_workflow/ls2/)
+* [Code](https://git.libre-soc.org/?p=ls2.git;a=blob;f=src/ls2.py;h=48f6cca7e06ac16ec42e76c361945e3943dca4b2;hb=HEAD)
One catastrophic mistake made by many cryptographic instruction implementations
is to create over-specific instructions. "multiply by 2 then subtract 5" for example