There are several different niches, and HW formal is likely using different tools and methods than SW formal, though there is overlap. Anyways there is room for a wide range of experience/skills/background in a variety of different areas.
Also, the main conference in the area is FMCAD, you can find a lot of related work there. More recently the conference has moved more towards software, but if you look at some of the older proceedings you can find a lot of hardware related stuff.
There is decent amount of overlap between formal for hardware and software, so if you study one you will likely have enough background to get started in the other.
Not at apple: The following is about 10 years out of date, would be interesting to know what's changed:
10 years ago formal had just started to be viable in run of the mill semiconductor verification (as opposed to throwing a bunch of specialist PhD grads at the problem); Jasper Gold was the first tool I heard of that worked well enough. pre-formal, the approach was to write a bunch of tests with input stimulators and validity checkers and/or assertions, and then work on the stimulators until you reached 100%coverage (signing off the cases that couldn't happen). That's not just line coverage, but each branch of an if, each component of a boolean expression must toggle, each bit of a signal must toggle, etc.
Reaching 100% coverage was a tedious exercise so the first use of formal was as a sumplement, to find the last,most difficult test cases that completed your coverage (or prove that the cases were impossible). The next use was to try and prove directly that assertions or test failures could not occur, or provide a counterexample. this is all based on the tool being able to read low level verilog or systemC code.
What it couldn't do at the time, which would be interesting to know if it can now, is as follows: Often, you actually have a higher level model of the behavior of your system. The RTL code is written to have the same behavior (manually, because it takes expertise to choose RTL code that will work efficiently). Ideally, provers would simply prove that your RTL has the same behavior.
rsrsrs86|2 years ago
ta1748|2 years ago
https://jobs.apple.com/en-us/search?search=formal&sort=relev...
There are several different niches, and HW formal is likely using different tools and methods than SW formal, though there is overlap. Anyways there is room for a wide range of experience/skills/background in a variety of different areas.
jderick|2 years ago
Here is a course taught at UT with some slides from guest lecturers from industry that looks like a decent overview:
https://www.cerc.utexas.edu/~jaa/verification/
Also, the main conference in the area is FMCAD, you can find a lot of related work there. More recently the conference has moved more towards software, but if you look at some of the older proceedings you can find a lot of hardware related stuff.
https://www.fmcad.org/
There is decent amount of overlap between formal for hardware and software, so if you study one you will likely have enough background to get started in the other.
ajb|2 years ago
10 years ago formal had just started to be viable in run of the mill semiconductor verification (as opposed to throwing a bunch of specialist PhD grads at the problem); Jasper Gold was the first tool I heard of that worked well enough. pre-formal, the approach was to write a bunch of tests with input stimulators and validity checkers and/or assertions, and then work on the stimulators until you reached 100%coverage (signing off the cases that couldn't happen). That's not just line coverage, but each branch of an if, each component of a boolean expression must toggle, each bit of a signal must toggle, etc.
Reaching 100% coverage was a tedious exercise so the first use of formal was as a sumplement, to find the last,most difficult test cases that completed your coverage (or prove that the cases were impossible). The next use was to try and prove directly that assertions or test failures could not occur, or provide a counterexample. this is all based on the tool being able to read low level verilog or systemC code.
What it couldn't do at the time, which would be interesting to know if it can now, is as follows: Often, you actually have a higher level model of the behavior of your system. The RTL code is written to have the same behavior (manually, because it takes expertise to choose RTL code that will work efficiently). Ideally, provers would simply prove that your RTL has the same behavior.