IFV and IUS, what's the difference?

Well, the short answer is that you can use both tools, since they tackle different verification problems.

Formal analysis is really good at finding nasty corner-case bugs with low effort from the engineer. However, formal is best applied to certain types of design if you want to get the best value from it. Good examples are control logic such as arbiters, state machines, FIFO control logic. Formal is not so good when the state space is big (wide busses, memories, big counters).
Simulation is still important for verifying the integration of all your modules once the design gets too big to handle in formal verification.

Designers use SVA or PSL to specify the legal input behaviour (assumptions) and the legal output behaviour (assertions), and the formal tool uses these as the modelling constraints and checks.

Designers can get very quick turn-around when writing or bug-fixing their code - the formal tool will quickly show them any errors they added without writing and running loads of simulations. Once the RTL module is well verified in IFV, the designers can integrate it into the bigger system where simulation is more useful. The module has already been exhaustively verified, so the only thing left to do (in simulation) is check that the connections into the module are legal and that the overall system design is good.
The really good thing now is that the assumptions written for IFV are treated as assertions in IUS, so that you're checking that what's driving your "perfectly" verified module is now checked for the correct input protocol, using the same properties.
This really boosts your confidence, and also helps isolate bugs when you're simulating at the system level, because you've already put loads of assertions all over your design!

If you haven't done so already, take a look at the Formal Analysis forum on CDNUsers.

Steve.

Well, the short answer is that you can use both tools, since they tackle different verification problems.

Formal analysis is really good at finding nasty corner-case bugs with low effort from the engineer. However, formal is best applied to certain types of design if you want to get the best value from it. Good examples are control logic such as arbiters, state machines, FIFO control logic. Formal is not so good when the state space is big (wide busses, memories, big counters).
Simulation is still important for verifying the integration of all your modules once the design gets too big to handle in formal verification.

Designers use SVA or PSL to specify the legal input behaviour (assumptions) and the legal output behaviour (assertions), and the formal tool uses these as the modelling constraints and checks.

Designers can get very quick turn-around when writing or bug-fixing their code - the formal tool will quickly show them any errors they added without writing and running loads of simulations. Once the RTL module is well verified in IFV, the designers can integrate it into the bigger system where simulation is more useful. The module has already been exhaustively verified, so the only thing left to do (in simulation) is check that the connections into the module are legal and that the overall system design is good.
The really good thing now is that the assumptions written for IFV are treated as assertions in IUS, so that you're checking that what's driving your "perfectly" verified module is now checked for the correct input protocol, using the same properties.
This really boosts your confidence, and also helps isolate bugs when you're simulating at the system level, because you've already put loads of assertions all over your design!

If you haven't done so already, take a look at the Formal Analysis forum on CDNUsers.

Steve.