Chisel is an open-source high-level hardware construction language embedded in Scala to facilitate parameterizable, reusable circuit design generators. It is becoming increasingly popular and has been used to design many RISC-V processor variants. Formal verification has been adapted to check the (functional) correctness of RISC-V processor designs. However, the RISC-V instructions therein are specified in the low-level hardware languages Verilog/SystemVerilog, which are challenging to develop, maintain, and extend. This considerably lowers the advantage of RISC-V for designing highly customizable processors. In this work, we present the first end-to-end approach for formally verifying the correctness of RISC-V processor designs, fully at the Chisel high-level. Specifically, by utilizing the object-oriented and functional programming constructs offered by Chisel, we develop a high-level reference model of RISC-V instructions in Chisel. This reference model is a succinct, modular, and parameterized RISC-V processor design generator, thus can produce customized RISC-V processor variants. We then devise a novel queue-based synchronization mechanism between the RISC-V processor Chisel design and the reference model by which the correctness verification of the RISC-V processor design is reduced to the model-checking problem and off-the-shelf model-checkers can be harnessed. We implement our approach in an open-source tool and demonstrate its efficacy on two representative open-source RISC-V processor designs in Chisel (i.e., riscv-mini and NutShell). The experiment results confirm the efficacy of our approach, capable of discovering 7 real-world unknown non-conformance bugs and all the 10 manually injected bugs. It is also three-orders-of-magnitude more efficient than the state-of-the-art symbolic-execution based approach.