This week I have been spending some time learning PSL assertion at work.? Assertion is a new verification methodology pushing very hard from the EDA venders.? It is a complement to the traditional verification flow, which you have no visibility inside the device.? Assertion allows you put extra checks right into the RTL logics.? Actually assertion exists for VHDL quite a long time.? The problem is the awkward syntax and limit functionality.? PSL is just another implemeent and syntax for assertion.? It seems the industry? somehow agree to support this one standard across different hardware languages.? One thing quite interesting is PSL assertion is inserted to the code as comments begins with the keyword psl.? Some of our old code breaks because we have a block happenes to call psl and we have this reserved keyword all over the code in comments.? Anyways, PSL assertion is quite handy to writing conditional or sequence checks.? Much easier than building a state machine to predict the result.? The more powerful feature of PSL assertion is that it support formal verification, which use mathematical alogirthm verify the code is equivalent to the specification. However, formalv verification is always a promise never comes true.? I guess if there are algorithms checking the specification against the implmentation, how hard would it be to let the algorithm simplily generate the code.? My first experience with PSL assertion is quite good, except that I manage to crash the simulator merely learning PSL for a day.? I guess I am just naturally attractive to bugs.<\/p>\n","protected":false},"excerpt":{"rendered":"