关于综合库，后仿库，还有验证库的区别？

新人，不懂，又来了。
综合时用的工艺库：.lib和.db有什么不同?
之后的后仿用的：.db又有什么区别?我只知道可以由综合库转化而来。
最后的形式验证又用到共享工艺库：.db，又是什么?
不是说：验证摆脱了工艺的约束和仿真test bench的不完全性。
可是工艺影响延时，延时影响时序。没有工艺的话，只比较RTL和网表文件，不是不知道时序影响。
那就必须后仿时序仿真了额?
不是很懂形式验证，和时序仿真的定位?
求教大大们~

同求，最近也在弄综合，求教大神解答