Forum Discussion
Altera_Forum
Honored Contributor
8 years agoTricky,
I have not had the Luxury of trying it on a Formal Verification Tool. It simulates just fine. In other cases, this kind of technique certainly SPEEDS UP simulation by avoiding REDUNDANT THREADS in badly written very INEFFICIENT PROPERTIES when someone has dumped them on me & I don't have time to fix them. BUT in those cases I don't leave the aux code in the files, I just use it to investigate the problems. People who write INEFFICIENT PROPERTIES just don't care about how long we have to wait. Their attitude is that their properties do check & it is someone else's problem if the project is delayed. I would be very interested to know if JasperGold or VC Formal etc. can handle PSL_BOOL_PType properly. If there is anyone out there reading this & with access to Formal Verification Tools then please TRY IT OUT & let us all know. In THEORY, if those tools implement VHDL2008 PROPERLY then all should be well. Tricky, maybe you could try it with JasperGold. PSL_BOOL_PType is a very simple Protected Type & once created it can be used over & over again without much effort. Using aux code feels like a bit of a Kludge but we have to live in the real world. I could say the same thing about PSL & SVA. (Double Kludge) ANYWAY For the situation described in my previous post we really SHOULD NOT have to do this. There SHOULD have been a simple BUILT IN way of doing this in PSL & SVA BECAUSE As I said before First Match OR goto repetition [->] WILL NOT DO IT.