An example

As an example of this, let us return to the read-only memory example from section 4.11. This is a ROM whose addresses are 24 bits, but the address is multiplexed into the ROM in two 12-bit hunks. At a high level, we would like to model this as a lookup in an array, such that addresses are treated in a completely symmetric way. However, at the implementation level, we need to be able to refer to the individual bits of address.

We will divide the code into two parts. The implementation is written in synchronous verilog, while the specification model and the proof are written in the SMV language. Note, it is usually more convenient to write abstract models in SMV, since SMV has a richer type structure. Further, at present, the proof declarations such as subcase and using..prove can only be written in SMV.

Let us begin with the SMV part. The first thing we do is to include the implementation code with the following declaration:

#include "ROM.v"

We assume this file will contain declarations for the types we need such as WORD and ADDR.

The high level model is quite straightforward:

  module main(){

    /* the abstract model */

    ROM : array ADDR of WORD;

    stall : boolean;
    addr_inp : ADDR;
    data_out : WORD;

    next(ROM) := ROM;   /* ROM stays constant over time */

    layer L1: {
      if(~stall)
        data_out  := ROM[addr_inp];
    }

    /* assume the address input is held while we stall */
    if(stall)
      next(addr_inp) := addr_inp;
    else next(addr_inp) := undefined;

We will return to the remainder of the SMV file shortly. Meanwhile, the synchronous verilog file (ROM.v) contains just the type declarations and the implementation module. We declare addresses (type ADDR) to be 24-bit scalarsets, and data words (type WORD) to be non-symmetric 32-bit vectors (symmetry of data words won't be used in the proof). Finally, we declare an enumerated type STATE for the state of a state machine in the implementation. Since verilog doesn't have enumerated types, we make STATE an ordinary boolean in the non-SMV case, and encode its two symbol values using macro definitions. Here is the code for the type declarations:

`ifdef __SMV__

  scalarset [23:0] ADDR;
  typedef [31:0] WORD;
  typedef enum {tx_low, tx_high} STATE;

  `define ADDR ADDR
  `define WORD WORD
  `define STATE STATE
  `define tx_low tx_low
  `define tx_high tx_high

`else

  `define ADDR [23:0]
  `define WORD [31:0]
  `define STATE
  `define `tx_low 0
  `define `tx_high 1

`endif

Now, in the implementation module ROM_impl, we'll use the macros defined above for the corresponding types:

module ROM_impl(clk,addr_inp, data_out, stall); 
   input  clk;
   input  `ADDR addr_inp;
   output `WORD data_out;
   output stall;

We'll use a two-state finite state machine to determine whether the high word or low word of the address is being clocked into the ROM. We stall the abstract model when in the low word state:

   reg `STATE state;
   initial state = `tx_low;
   always @(posedge clk)
      if(state == `tx_low)
         state = `tx_high;
      else state = `tx_low;
   
   assign stall = (state == `tx_low);

We'll also need a 12 bit register to save the low word of the address while the high word is being transmitted:

   reg [11:0] low_reg;
   // smv breaking(ADDR)
     always @(posedge clk)
        if(state == `tx_low)
           low_reg = addr_inp[11:0];
   // smv endbreaking

Note that in order to extract the low order 12 bits of the address, we have to declare that we're breaking the symmetry of type ADDR. Otherwise SMV will report an error. However, to hide this declaration from other tools, we use the //smv syntax. Now, we reassemble the address from the high and low order parts, and look up in the array:

   wire `ADDR impl_addr;
   // smv breaking(ADDR)
      assign impl_addr = {addr_inp[23:12],low_reg};
   // smv endbreaking
   
   /* an instance of a ROM */
   ROM24x32 ROM(impl_addr,data_out);
   
endmodule // ROM_impl

The ROM itself is a call to a library cell ROM24x32. This we can model in the SMV file as follows:

  module ROM24x32(addr,data){
    input addr : ADDR;
    output data : WORD;

    r : array ADDR of WORD;

    next(r) := r;
    data := r[addr];
  }

That's the end of the implementation file. Now, of course, we want to show that the value of data_out produced by this implementation actually satisfies the specification in layer L1. Thus, we return to the main module, and create an instance of module ROM_impl to provide the implementation:

    /* the implementation */

    clk : boolean;
    impl : ROM_impl(clk,addr_inp,data_out,stall);

Note that clk is a dummy signal here. In simulation it would be driven by a ``test bench''. However, in synchronous verilog, the registers are updated at every time unit, and clk is simply ignored.

Now, to prove that we have correctly implemented our specification (i.e., that we have correctly refined signal data_out), we need to be able to handle the lookup in the ROM array. Since this is a very large array, we must rely on the symmetry of type ADDR (we cannot possibly check $2^{24}$ cases separately). However, the lookup in the ROM array depends on impl_addr, which breaks the symmetry of type ADDR. Therefore, we will write a refinement map for impl_addr, breaking the problem into two parts, one which breaks the symmetry of ADDR, and one which does not:

    layer L2:
      if(state=tx_high)
        impl.impl_addr := addr_inp;

That is, we rely on the fact that the address reassembled from the high and low parts must equal the original address. Further, we must specify that the initial contents of the ROM in the specification model are equal to the initial contents of the ROM in the implementation (a witness function):

    init(ROM) := impl.ROM.r;

Now, to prove the data output correctness, we do the usual trick of splitting cases on the address:

   forall(a in ADDR) subcase L1[a] of data_out//L1 for addr_inp = a;

To verify the refinement relation for impl_addr, however, we simply break the symmetry of addresses:

   breaking(ADDR) prove impl.impl_addr//L2;
 }

This will cause SMV to treat impl_addr as a 24-bit vector when proving this property. As a result, we will have to verify each bit if impl_addr separately. This is not a problem, however, since the verification problem for each bit is trivial.

Now, copy the main SMV file ROM_main.smv and the verilog implementation file ROM.v into a directory, and run vw on the main file.²Observe the ``Cone'' pane. You'll notice that there are 32 instances of the data output correctness property data_out//L1, one for each bit in the data path. However, only one representative address case was chosen because we are exploiting the symmetry of addresses. Similarly, there are 24 instance of the refinement relation impl_addr//L2, one for each address bit. This is because we are breaking the symmetry of addresses to prove this property, hence addresses appear as bit vectors and not scalars. If you select ``Verify all'', you'll find that the model checking goes very quickly, because all 32 data cases are isomorphic, as are all 12 cases for each of the low and high halves of the address word. Thus, all but three instances hit in SMV's hash table.

Thus, we have been able to verify a property involving a 24-bit address space, by exploiting symmetry of the bit vector type ADDR to deal with the large memory array, but breaking the symmetry when verifying the bit-level multiplexing if the address. Further, the implementation file remains compatible with existing verilog tools.