I recommend downloading and installing the free Yosys software and the free solvers on Ubuntu, and then follow the tutorials from Symbiotic EDA and try it out hands-on to gain experience with formal verification, because that's what I did. The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand language to specify properties that can even span infinite cycles.

In the end, it's not magic, and it has its limitations like any other technology. But it is a powerful technique that leverages research done in mathematics, computer science and formal logic.

I recommend downloading and installing the free Yosys software and the free solvers on Ubuntu, and then follow the tutorials from Symbiotic EDA and try it out hands-on to gain experience with formal verification, because that's what I did as a senior year engineering undergraduate. The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand language to specify properties that can even span infinite cycles. Note that the open-source version of Symbiotic EDA does not support most SVA constructs.

In the end, it's not magic, and it has its limitations like any other technology. But it is a powerful technique that leverages cutting-edge research done in mathematics, computer science and formal logic.

I recommend downloading and installing the free Yosys software and the free solvers on Ubuntu, and then follow the tutorials from Symbiotic EDA and try it out hands-on to gain experience with formal verification, because that's what I did.

The other answer has mentioned formal equivalence checking, which is a kind of formal verification that checks 2 designs which may or may not be at the same abstraction level for logical / functional equivalency. For example, you can do RTL versus RTL formal equivalence checking or RTL versus gate-level netlist formal equivalence checking. Equivalence checking is one of the most common formal verification based techniques used in the semiconductor industry. Low-power formal verification and property checking are other kinds of formal verification. I have worked with property checking, so I can write a little about it.

SAT, as we know, is NP Complete i.e. no known polynomial time algorithm to solve this problem exists. So one might expect formal verification to be slow. Yes, formal verification can be slow for large designs and the tool can "choke" when the complexity of the proofs is high, due to the system running out of memory. The good news is there are clever techniques like blackboxes, cut-points and abstractions that can be applied by the one doing formal verification to speeden the verification process and reduce memory consumption. Adding a sufficient number of assumptions restricts the solver to check a smaller search space, and increases the probability of converging to a solution.

For a large design, it is recommended to break the problem of verifying the design into smaller, provable properties that verify the entire design. This enables the tool to use a Divide-and-Conquer approach to generate the proofs. For example, RISC-V Formal uses a set of simple properties to prove ISA compliance of RISC-V processors.

Formal verification is a somewhat challenging field, but the effort is worth it. Some bugs like the Pentium Floating point division bug will most likely escape random testing, since the probability of the occurences leading to the detection of some bugs in random testing is extremely small. You can't verify that your design does not hang (enter a deadlock) at some point of time using constrained random, since there are only so many cycles you can run the simulation for. Formal verification proves the entire design is bug-free, provided one writes the right properties. Formal verification using the Induction technique proves the correctness of designs for infinite cycles. It's not magic, it's the power of mathematics and formal logic.

The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand language to specify properties that can even span infinite cycles.

How to learn practical Formal Verification

I recommend downloading and installing the free Yosys software and the free solvers on Ubuntu, and then follow the tutorials from Symbiotic EDA and try it out hands-on to gain experience with formal verification, because that's what I did. The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand language to specify properties that can even span infinite cycles.

Equivalence Checking Vs. Formal Verification

The other answer has mentioned formal equivalence checking, which is a kind of formal verification that checks 2 designs which may or may not be at the same abstraction level for logical / functional equivalency. For example, you can do RTL versus RTL formal equivalence checking or RTL versus gate-level netlist formal equivalence checking. Equivalence checking is one of the most common formal verification based techniques used in the semiconductor industry. Low-power formal verification and property checking are other kinds of formal verification. I have worked with property checking, so I can write a little about it.

Property Checking

Limitations of Property Checking

1. SAT is NP Complete i.e. no known polynomial time algorithm to solve this problem exists. So one might expect formal verification to be slow. Yes, formal verification can be slow for large designs and the tool can "choke" when the complexity of the proofs is high, due to the system running out of memory. The good news is there are clever techniques like blackboxes, cut-points and abstractions that can be applied by the one doing formal verification to speeden the verification process and reduce memory consumption. Adding a sufficient number of assumptions restricts the solver to check a smaller search space, and increases the probability of converging to a solution.
2. The Incompleteness Theorem: The conclusion that has to be drawn from this theorem is that it is not possible to build a formal system that can be guaranteed to verify the correctness of any specifications. Tools that can solve most problems found in the real world do exist and are useful.
3. Correctness and completeness of properties: The onus of the correctness and completeness of properties specified is on the one writing the properties. Writing correct properties is not very easy and it takes time to learn to write assertions.

Suggestions for property checking

1. For a large design, it is recommended to break the problem of verifying the design into smaller, provable properties that verify the entire design. This enables the tool to use a Divide-and-Conquer approach to generate the proofs. For example, RISC-V Formal uses a set of simple properties to prove ISA compliance of RISC-V processors.
2. It is also recommended to start with Bounded model checking and then try Induction proofs. This is because bounded model checking is easier to run and debug.

Is formal verification worth it?

1. Formal verification is a somewhat challenging field, but the effort is worth it because some bugs like the Pentium Floating point division bug will most likely escape random testing, since the probability of the occurences leading to the detection of some bugs in random testing is extremely small.
2. You can't verify that your design does not hang (enter a deadlock) at some point of time using constrained random, since there are only so many cycles you can run the simulation for. Formal verification can potentially prove the correctness of the logic design at the Register Transfer Level and gate level for infinite cycles.

In the end, it's not magic, and it has its limitations like any other technology. But it is a powerful technique that leverages research done in mathematics, computer science and formal logic.

As an undergraduate myself, I can say that Formal verification is within the reach of an engineering undergraduate. I recommend downloading and installing the free Yosys software and the free solvers on Ubuntu, and then follow the YouTube videos from Symbiotic EDA and try it out hands-on to gain experience with formal verification, because that's what I did.

The other answer has mentioned formal equivalence checking, which is a kind of formal verification that checks 2 designs which may or may not be at the same abstraction level for logical / functional equivalency. For example, you can do RTL versus RTL formal equivalence checking or RTL versus gate-level netlist formal equivalence checking. Equivalence checking is one of the most common formal verification based techniques used in the semiconductor industry. Low-power formal verification and property checking are other kinds of formal verification. I have worked with property checking, so I can write a little about it.

Property checking is a technique where you specify properties, and the solver proves these properties are held true, either for all time i.e. induction, or for a certain number of cycles i.e. bounded model checking. 2 kinds of properties are specified: assumptions and assertions. Assumptions are properties which the solver assumes and assertions are the properties the solver needs to prove. So the problem of proving properties is represented as a SAT (Satisfiability, i.e. Boolean Satisfiability) problem, which is then solved by SAT solvers.

SAT, as we know, is NP Complete i.e. no known polynomial time algorithm to solve this problem exists. So one might expect formal verification to be slow. Yes, formal verification can be slow for large designs and the tool can "choke" when the complexity of the proofs is high, due to the system running out of memory. The good news is there are clever techniques like blackboxes, cut-points and abstractions that can be applied by the one doing formal verification to speeden the verification process and reduce memory consumption. Adding a sufficient number of assumptions restricts the solver to check a smaller search space, and increases the probability of converging to a solution.

For a large design, it is recommended to break the problem of verifying the design into smaller, provable properties that verify the entire design. This enables the tool to use a Divide-and-Conquer approach to generate the proofs. For example, RISC-V Formal uses a set of simple properties to prove ISA compliance of RISC-V processors.

Formal verification is a somewhat challenging field, but the effort is worth it. Some bugs like the Pentium Floating point division bug will most likely escape random testing, since the probability of the occurences leading to the detection of some bugs in random testing is extremely small. You can't verify that your design does not hang (enter a deadlock) at some point of time using constrained random, since there are only so many cycles you can run the simulation for. Formal verification proves the entire design is bug-free, provided one writes the right properties. Formal verification using the Induction technique proves the correctness of designs for infinite cycles. It's not magic, it's the power of mathematics and formal logic.

The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand language to specify properties that can even span infinite cycles.

I recommend downloading and installing the free Yosys software and the free solvers on Ubuntu, and then follow the tutorials from Symbiotic EDA and try it out hands-on to gain experience with formal verification, because that's what I did.

The other answer has mentioned formal equivalence checking, which is a kind of formal verification that checks 2 designs which may or may not be at the same abstraction level for logical / functional equivalency. For example, you can do RTL versus RTL formal equivalence checking or RTL versus gate-level netlist formal equivalence checking. Equivalence checking is one of the most common formal verification based techniques used in the semiconductor industry. Low-power formal verification and property checking are other kinds of formal verification. I have worked with property checking, so I can write a little about it.

Property checking is a technique where you specify properties, and the solver proves these properties are held true, either for all time i.e. induction, or for a certain number of cycles i.e. bounded model checking. 2 kinds of properties are specified: assumptions and assertions. Assumptions are properties which the solver assumes and assertions are the properties the solver needs to prove. So the problem of proving properties is represented as a SAT (Satisfiability, i.e. Boolean Satisfiability) problem, which is then solved by SAT solvers.

SAT, as we know, is NP Complete i.e. no known polynomial time algorithm to solve this problem exists. So one might expect formal verification to be slow. Yes, formal verification can be slow for large designs and the tool can "choke" when the complexity of the proofs is high, due to the system running out of memory. The good news is there are clever techniques like blackboxes, cut-points and abstractions that can be applied by the one doing formal verification to speeden the verification process and reduce memory consumption. Adding a sufficient number of assumptions restricts the solver to check a smaller search space, and increases the probability of converging to a solution.

For a large design, it is recommended to break the problem of verifying the design into smaller, provable properties that verify the entire design. This enables the tool to use a Divide-and-Conquer approach to generate the proofs. For example, RISC-V Formal uses a set of simple properties to prove ISA compliance of RISC-V processors.

Formal verification is a somewhat challenging field, but the effort is worth it. Some bugs like the Pentium Floating point division bug will most likely escape random testing, since the probability of the occurences leading to the detection of some bugs in random testing is extremely small. You can't verify that your design does not hang (enter a deadlock) at some point of time using constrained random, since there are only so many cycles you can run the simulation for. Formal verification proves the entire design is bug-free, provided one writes the right properties. Formal verification using the Induction technique proves the correctness of designs for infinite cycles. It's not magic, it's the power of mathematics and formal logic.

The properties are written in a property specification language, like PSL and SystemVerilog Assertions. I have worked with SystemVerilog Assertions (SVA). SVA gives us a compact, easy-to-understand language to specify properties that can even span infinite cycles.