Formal verification solutions based on Symbolic Computer Algebra (SCA) for complex arithmetic circuits. We also provide
GenMul a configurable (input size and architecture) generator for multipliers in Verilog.
RISC-V Virtual Prototype (VP) modeled in SystemC. The VP is open source, TLM2.0 compliant, and has great features like e.g. software debug via Eclipse by integrated GDB support, and runs FreeRTOS. See www.systemc-verification.org/riscv-vp for the github repositories.
ESL Verification tools & topics, in particular constrained-random library CRAVE
and formal TLM verification methods (SCIVER and SISSI), available at www.systemc-verification.org