Verifying instruction execution against a golden instruction set architecture (ISA) simulator is becoming a common practice to verify processors. Despite many potential applications, existing verification frameworks require an extensive test set to cover most of the processor states. In this paper, we demonstrate a verification scheme combining two different domains, functional and formal, converging to exclusive error detection. By combining these two, we present a reliable way to perform more accurate instruction verification to detect different kinds of errors. The proposal detected a RISC-V ISA specification gap revealing the ambiguity from the verification perspectives.