One of the areas I am very well versed in is that of applying formal property verification, my bread and butter for the last eight years. And, living and working in the US, I am especially proficient in SystemVerilog assertions; my knowledge of PSL is rather rudimentary. And yet, as I was reminded the other day, there is always something new to learn.
In my experience, by far most SV assertions are concurrent as opposed to immediate. That is, they are typically standalone assertions of the form
prop_name: assert property (@(posedge clk) a |=> b);Whether explicit or implicit, they always include some clock or other edge-triggered sampling event - which is normally not a problem as by far most blocks are not combinatorial anyway and so there is always a clock to grab. And even when I'm dealing with a combinatorial design - an ECC checker, say - I can normally get away with writing simply
corr: assert property (ec |-> data_out == data_in);even if there is no implicit clock in the design, as I'm always using a formal property checker: Since the formal tools are always clock rather than event driven, they will typically just use their own internal clock as the implicit clock rather than error out. Effectively, this will sample the property all the time, that is, make it combinatorial which is exactly what I want.
This leaves the question of what to do if one wants to be strictly SV compliant (or just wants tool warnings to go away). I always figured that
always_comb corr: assert (!ec || data_out == data_in);was effectively equivalent to the concurrent version above. I always preferred the former because it allows the full SVA syntax, including implication, whereas the latter only allows SV boolean expressions. In other words, I can write concurrent assertions to be more readable.
Which brings me to other day, where I had finished one of the simple BCD-related exercises in the lab exercises for my FPGA board: Given two four bit inputs, A and B, show A on the left-most LED segment (HEX3), B on the next (HEX2), and their sum on the last two (HEX1 and HEX0) - all in decimal. Plus detection of illegal (>9) input values and some other connections that aren't relevant to the point I'm making. Following the scheme above, I wrote the property
always_comb hex3_p: assert (!err || decode(HEX3) == A);happily assuming it would capture my intent: Unless there's an input error, the value displayed on HEX3 will be equal to the value of A. Looking at the simulation trace, I'd gotten it right the first time, I just had a corner-case property problem at cycle 0 where the property was failing because all the signals were X. Reading up on always_comb, I saw that it was specifically activated at time 0 - unlike (by inference) always @*:
always @* hex3_p: assert (!err || decode(HEX3) == A);Now the property passed cleanly. Just to double-check the setup, I tried removing the "!err" disjunct, expecting a fail. It still passed.
After some debugging, my suspicion fell on the automatically-derived sensitivity lists of always_comb (which was also passing except for time 0) and always @*. A quick scan through IEEE 1800-2005 didn't turn up any mention of assertions in that context, so it would seem it unspecified whether variables from assertions should be added to the sensitivity list or not. ModelSim, which I'm using at home, doesn't include them, while I noticed at work that both NC-Verilog and VCS do. Fair enough. Using an explicit sensitivity list solved the problem:
always @ (error,HEX3) hex3_p: assert (!err || decode(HEX3) == A);Notice, as I initially didn't, the lack of A in the sensitivity list.
The check for HEX2 also went through just fine, but when I got to the sum output, I was stumped: The property was randomly failing yet all the outputs looked fine. Exposing myself as a complete newbie, I had introduced a race condition which I had inadvertently avoided in the first two properties. I conceptually had two actions in my code: The computation of HEX3 from A and the comparison of HEX3 and A in the property. When A changes (and A is in the sensitivity list), both action blocks are activated, but the order of their execution is not guaranteed: If the assignment of HEX3 is computed before the assertion, the latter won't fail. If, on the other hand, the assertion is checked before HEX3 has been updated, it will. By leaving out A in the sensitivity list of the procedure containing the assertion I had neatly avoided the race condition as the property wouldn't see the intermediary step of A updating. The property checking two LED segments could not be similarly fixed as the race condition was already between the updates of the two LED segments and the property.
In my defense, none of this makes any difference in formal tools: Sensitivity lists are ignored as they are for synthesis and race conditions do not exist as properties are checked only once a consistent state has been reached, that is, once all changes have propagated. That's my story and I'm sticking to it.
After all this, it was clear that writing stand-alone immediate combinatorial assertions was not the way forward. To avoid race conditions, it seemed prudent to explicitly do exactly what the formal tools do implicitly: Introduce a clock external to the design and make the testbench synchronous to that. As it happens, I can't use concurrent assertions with the free ModelSim version available from Altera's home page, so I simply used an intermediate assertion in a synchronous always block:
always @ (posedge clk) hex3_p: assert (!err || decode(HEX3) == A);I don't get the nice implication syntax, but at least I don't get any race conditions either and it behaves the same across all three simulators that I have access to. All I have to ensure is that the relevant signals are non-X by the time the first posedge of clk is seen.
