A lot of analog circuits as well as a few digital ones use thermometer coding. For years I have had the suspicion that there was a really simple way to write an assertion that checked a bit-vector for thermometer coding. It hasn’t been a priority, so I didn’t think too much about it, but today it hit me: A bit vector is a thermometer code if the code plus 1 is a one-hot signal or power of two number. I feel stupid. This is simply the reverse of the bit-twiddling hack to check for a power of two number. So without further ado, the thermometer code checking assertion:

a_is_therm_code: assert property (
  @(posedge clk) disable iff (!rst_n)
  $onehot0(code+1)
);

And the reverse version if the msbs are ones (bit inversion plus one is negation):

a_is_rev_therm_code: assert property (
  @(posedge clk) disable iff (!rst_n)
  $onehot0(-code)
);