Simulator compatibility

Note, the use of these declarations introduces a problem if we want to write synchronous verilog code that is compatible with verilog simulators and logic synthesis tools. For this reason, synchronous verilog provides ways of hiding ``decorations'' used by SMV from these tools. One is the syntax

  // smv ...code for smv only...

Any code between // smv and the end of a line is processed by synchronous verilog, and not treated as a comment. On the other hand, a simulator will ignore such code. This gives us a convenient way to introduce symmetry breaking declarations, for example:

  // smv breaking(foo)
    ...code breaking symmetry of type foo...
  // smv endbreaking

To introduce symmetric types it is more convenient to use a macro for the type. We can define the macro differently, depending on whether the code is interpreted for SMV, or for another tool. For example, to define the symmetric type foo, we could use the following code:

`ifdef __SMV__
  scalarset [3:0] foo;
  `define foo foo
`else
  `define foo [3:0]
`endif

The macro __SMV__ is predefined by SMV when processing synchronous verilog files. Thus, if SMV is processing the file, the macro `foo will stand for the scalarset type foo, otherwise, it will simply stand for text [3:0]. Thus, if we later declare a register as follows:

  reg `foo x;

then x will be a four bit quantity - a scalarset in SMV, but an ordinary bit vector in other tools.