Every digital device has Control and Status Registers (CSRs) described by a Register Map: it is a fundamental element for the correct operation of any function in an IC. For this reason, there is a strong need to guarantee the absence of malfunctions inside the CSRs. In order to achieve this, the available methods to verify CSRs behavior exhaustively were explored. Starting from a Register Map already verified with Universal Verification Methodology (UVM), formal verification was applied: the main objective was to compare how formal performance and results differed from the UVM approach. The first aspect analyzed was the capability in finding bugs of formal, with particular attention to bugs that can be very hard to detect, or debug, through an UVM run.