As part of the DFG project "Reinhart Koselleck PolyVer" I work on Polynomial Formal Verification (PFV) of complex circuits with a focus on RISC-V processors. The central question is whether certain architectures have polynomial time and space upper bounds and if available to determine these exactly.