Verification of a DLX pipeline

Following the CAV 98 paper by Srivas and others we tested the performance of the uninterpreted decision procedures by verifying the correctness of a DLX pipeline in a brute force manner. The transcribed PVS specification with running times of the validity checker follows below.



(* @(#)test15.spec  1.1 05/23/98 *)
SPEC %spec

type word
type reg_addr
type instruction
type alu_op
type imem_type 
type regfile_type = array reg_addr of word
type dmem_type = array word of word
type state_A = {pc : word,
          regfile : regfile_type,
    dmem : dmem_type,
    imem : imem_type  
         }
type inputs_type = {stall : bool}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Select part of the instruction register

value rf1_of,rf2_of,rf3_of : instruction --> reg_addr

type instr_classes = {j, beqz, load, store, alu_immed, alu_reg}

type opcode 
value opcode_of:   instruction --> opcode
value instr_class : opcode --> instr_classes
value alu_op_of:   opcode --> alu_op

  
value short_immed_of : instruction --> word
value long_immed_of  : instruction --> word

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Operations on register file and memory

value zero_reg: reg_addr
value zero_word: word
value four_word: word

value add : word * word --> word
value alu : alu_op * word *word --> word
value read_imem : imem_type *  word --> instruction


macro read_reg(RF:regfile_type, Raddr:reg_addr):word = RF[Raddr]
macro write_reg(RF:regfile_type, Raddr:reg_addr, val:word):regfile_type =
  update(RF,val,Raddr)

variable R1, R2: reg_addr
variable W : word
variable RF : regfile_type


macro read_dmem(DM:dmem_type, Daddr:word):word = DM[Daddr]
macro write_dmem(DM:dmem_type, Daddr:word, val:word):dmem_type =
  update(DM,val,Daddr)

variable M1, M2: word
variable DM: dmem_type

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

variable as : state_A

macro inst(as: state_A) : instruction =
  read_imem(#imem(as), #pc(as))

macro rf1data(as: state_A) : word =
  if rf1_of(inst(as))=zero_reg
    then zero_word
    else read_reg(#regfile(as),rf1_of(inst(as)))
  

macro rf2data(as: state_A) : word = 
  if rf2_of(inst(as))=zero_reg
    then zero_word
  else read_reg(#regfile(as),rf2_of(inst(as)))
  


macro new_pcA(as: state_A) : word =
  if instr_class(opcode_of(inst(as)))=j
    then add(long_immed_of(inst(as)),add(four_word,#pc(as)))
  else if (instr_class(opcode_of(inst(as)))= beqz) /\ rf1data(as)=zero_word
    then add(short_immed_of(inst(as)),add(four_word,#pc(as)))
    else add(four_word,#pc(as))
  


macro new_regfileA(as: state_A) : regfile_type =
  if instr_class(opcode_of(inst(as)))=load
     /\ !(rf2_of(inst(as))=zero_reg)
         then write_reg(#regfile(as), rf2_of(inst(as)),
          read_dmem(#dmem(as), add(rf1data(as),short_immed_of(inst(as)))))
  else if instr_class(opcode_of(inst(as)))=alu_immed
         /\ !(rf2_of(inst(as))=zero_reg)
    then write_reg(#regfile(as), rf2_of(inst(as)), 
         alu(alu_op_of(opcode_of(inst(as))),
             rf1data(as), short_immed_of(inst(as))))
  else if instr_class(opcode_of(inst(as)))=alu_reg
    /\ !(rf3_of(inst(as))=zero_reg)
    then write_reg(#regfile(as), rf3_of(inst(as)),
         alu(alu_op_of(opcode_of(inst(as))),
             rf1data(as), rf2data(as)))
    else #regfile(as)
  

macro new_dmemA(as: state_A) : dmem_type =
  if instr_class(opcode_of(inst(as)))=store
  then write_dmem(#dmem(as), add(rf1data(as),short_immed_of(inst(as))),
         rf2data(as))
  else #dmem(as)
  

macro new_imemA(as:state_A) : imem_type = #imem(as)

macro A_step(as: state_A,inp:inputs_type) : state_A =
  if #stall(inp)
    then as
  else
    { pc = new_pcA(as);
      regfile = new_regfileA(as);
      dmem = new_dmemA(as);
      imem = new_imemA(as)
    }
        

type state_I = {
    regfile: regfile_type,
    dmem: dmem_type,
    imem: imem_type,
    dest_wb: reg_addr,
    result_wb: word,
    dest_mem: reg_addr,
    result_mem: word,
    mar: word,
    load_flag: bool,
    store_flag: bool,
    bubble_ex: bool,
    offset_ex: word,
    dest_ex: reg_addr,
    opcode_ex: opcode,
    operand_a : word,
    operand_b: word,
    bubble_id: bool,
    inst_id: instruction,
    pc: word
    }

value inp: inputs_type

% WB stage

macro new_regfileI(is:state_I) : regfile_type =
  if !(#dest_wb(is)=zero_reg)
  then write_reg(#regfile(is), #dest_wb(is), #result_wb(is))
  else #regfile(is)
  

% MEM stage

macro new_dest_wb(is:state_I) : reg_addr = #dest_mem(is)


macro new_result_wb(is:state_I) : word =
  if #load_flag(is)
  then read_dmem(#dmem(is),#mar(is))
  else #result_mem(is)
  

macro new_dmemI(is:state_I) : dmem_type =
  if #store_flag(is)
  then write_dmem(#dmem(is),#mar(is),#result_mem(is))
  else #dmem(is)
  

% EX stage

macro new_dest_mem(is:state_I) : reg_addr = #dest_ex(is)

macro new_load_flag(is:state_I) : bool = !(#bubble_ex(is)) /\
         (instr_class(#opcode_ex(is)) = load)

macro new_store_flag(is:state_I) : bool = !(#bubble_ex(is)) /\
          (instr_class(#opcode_ex(is)) = store)

macro alu_result(is:state_I) : word =
  if (instr_class(#opcode_ex(is)) = load) \/
     (instr_class(#opcode_ex(is)) = store)
  then add(#operand_a(is), #offset_ex(is))
  else alu(alu_op_of(#opcode_ex(is)),#operand_a(is),#operand_b(is))
  

macro new_result_mem(is) : word =
  if (instr_class(#opcode_ex(is)) = load) \/
     (instr_class(#opcode_ex(is)) = store)
  then #operand_b(is)
  else alu_result(is)
  

macro new_mar(is:state_I) : word = alu_result(is)
  

% ID stage

macro new_operand_a(is:state_I) : word =
  if rf1_of(#inst_id(is)) = zero_reg
    then zero_word
  else if rf1_of(#inst_id(is)) = #dest_ex(is)
    then new_result_mem(is) 
  else if rf1_of(#inst_id(is)) = #dest_mem(is)
    then new_result_wb(is) 
  else read_reg(new_regfileI(is),rf1_of(#inst_id(is))) 
  

macro new_operand_b(is:state_I) : word =
  if instr_class(opcode_of(#inst_id(is))) = alu_immed
    then short_immed_of(#inst_id(is))
  else if rf2_of(#inst_id(is)) = zero_reg
    then zero_word
  else if rf2_of(#inst_id(is)) = #dest_ex(is)
    then new_result_mem(is) 
  else if rf2_of(#inst_id(is)) = #dest_mem(is)
    then new_result_wb(is) 
  else read_reg(new_regfileI(is),rf2_of(#inst_id(is))) 
  

macro stall_issue(is:state_I) : bool =
  !(#bubble_ex(is)) /\ instr_class(#opcode_ex(is))=load /\
  !(#bubble_id(is)) /\ (rf1_of(#inst_id(is)) = #dest_ex(is) \/
        rf2_of(#inst_id(is)) = #dest_ex(is))

macro JTA(is:state_I) :  word = add(long_immed_of(#inst_id(is)), #pc(is))

macro BTA(is:state_I) :  word = add(short_immed_of(#inst_id(is)), #pc(is))

macro TA(is:state_I) : word = if instr_class(opcode_of(#inst_id(is)))=j
     then JTA(is) else BTA(is) 

macro branch_taken(is:state_I) : bool =
  !(#bubble_id(is)) /\ (instr_class(opcode_of(#inst_id(is)))=j \/
              (instr_class(opcode_of(#inst_id(is)))=beqz /\
         new_operand_a(is)=zero_word))

macro new_bubble_ex(is:state_I) :  bool =
  stall_issue(is) \/ #bubble_id(is) \/
  instr_class(opcode_of(#inst_id(is)))=j \/
  instr_class(opcode_of(#inst_id(is)))=beqz      

macro new_offset_ex(is:state_I) : word = short_immed_of(#inst_id(is))

macro new_dest_ex(is:state_I) : reg_addr =
  if new_bubble_ex(is) \/ instr_class(opcode_of(#inst_id(is)))=store  
  then zero_reg
  else if instr_class(opcode_of(#inst_id(is)))=load \/
        instr_class(opcode_of(#inst_id(is)))=alu_immed
  then rf2_of(#inst_id(is))
  else rf3_of(#inst_id(is))
  

macro new_opcode_ex(is:state_I) : opcode = opcode_of(#inst_id(is))

% IF stage

macro new_bubble_id(is:state_I,inp: inputs_type) : bool =
  if stall_issue(is) then #bubble_id(is)
  else if #stall(inp) then true
  else branch_taken(is)
  

macro new_inst_id(is:state_I,inp: inputs_type) : instruction =
  if stall_issue(is) then #inst_id(is)
  else if #stall(inp) then #inst_id(is)
  else read_imem(#imem(is),#pc(is))
  

macro new_pcI(is:state_I,inp: inputs_type) : word =
  if stall_issue(is) then #pc(is)
  else if #stall(inp) then
     if branch_taken(is) then TA(is) else #pc(is) 
  else if branch_taken(is) then TA(is) else add(four_word,#pc(is)) 
  

macro new_imemI(is:state_I) : imem_type = #imem(is)

macro I_step(is:state_I,inp: inputs_type) : state_I = {
    regfile= new_regfileI(is);
    dmem= new_dmemI(is);
    imem= new_imemI(is);
    dest_wb= new_dest_wb(is);
    result_wb= new_result_wb(is);
    dest_mem= new_dest_mem(is);
    result_mem= new_result_mem(is);
    mar= new_mar(is);
    load_flag= new_load_flag(is);
    store_flag= new_store_flag(is);
    bubble_ex= new_bubble_ex(is);
    offset_ex= new_offset_ex(is);
    dest_ex= new_dest_ex(is);
    opcode_ex= new_opcode_ex(is);
    operand_a= new_operand_a(is);
    operand_b= new_operand_b(is);
    bubble_id= new_bubble_id(is,inp);
    inst_id= new_inst_id(is,inp);
    pc= new_pcI(is,inp)
    }

value is: state_I

% Complete the instruction in the MEM/WB pipeline registers.
macro Complete_MEM_WB(is : state_I) : state_I =
  (is) with [ regfile := if !(dest_wb(is)=zero_reg) then
          write_reg(regfile(is),dest_wb(is),result_wb(is))
             else regfile(is)  ]


% Complete the instruction in the EX/MEM pipeline registers.
macro Complete_EX_MEM(is : state_I) : state_I =
  is with [ dmem := if store_flag(is) then
             write_dmem(dmem(is),mar(is),result_mem(is))
          else dmem(is) ,

      regfile := if !(dest_mem(is)=zero_reg) then
          write_reg(regfile(is),dest_mem(is),
            if load_flag(is) then
               read_dmem(dmem(is),mar(is))
            else result_mem(is) )
              else regfile(is)  ]


% Complete the instruction in the ID/EX pipeline registers.
macro Complete_ID_EX(is : state_I) : state_I =
  is with [ dmem := if (instr_class(opcode_ex(is)) = store) /\ !(bubble_ex(is)) then
             write_dmem(dmem(is),add(operand_a(is),offset_ex(is)),operand_b(is))
          else dmem(is) ,
      regfile := if ! (dest_ex(is)=zero_reg) /\ !(bubble_ex(is)) /\
          (instr_class(opcode_ex(is)) = load) then
                write_reg(regfile(is),dest_ex(is),read_dmem(dmem(is),
              add(operand_a(is),offset_ex(is))))
             else if ! (dest_ex(is)=zero_reg) /\ ! (bubble_ex(is)) /\ 
          ((instr_class(opcode_ex(is)) = alu_reg) \/
            (instr_class(opcode_ex(is)) = alu_immed)) then
          write_reg(regfile(is),dest_ex(is),alu(alu_op_of(opcode_ex(is)),
                operand_a(is),operand_b(is)))
             else regfile(is)  ]


macro val_a(is1 : state_I) : word =
  if rf1_of(inst_id(is1)) = zero_reg then zero_word
  else read_reg(regfile(is1),rf1_of(inst_id(is1))) 

macro val_b(is1 : state_I) : word = 
  if instr_class(opcode_of(inst_id(is1))) = alu_immed then
    short_immed_of(inst_id(is1))
  else if rf2_of(inst_id(is1)) = zero_reg then
    zero_word
  else read_reg(regfile(is1),rf2_of(inst_id(is1))) 

macro branch_taken_test(is1 : state_I) : bool =
  instr_class(opcode_of(inst_id(is1))) = j \/ 
    (instr_class(opcode_of(inst_id(is1))) = beqz /\
      val_a(is1) = zero_word)

macro instr_kind(is1 : state_I) : instr_classes =
  instr_class(opcode_of(inst_id(is1)))

macro mem_addr(is1 : state_I) : word =
  add(val_a(is1),short_immed_of(inst_id(is1)))

% Complete the instruction in the IF/ID pipeline registers.
macro Complete_IF_ID(is : state_I) : state_I =
  if bubble_id(is) then
     is
  else 
         is with [ pc := if branch_taken_test(is) then TA(is) 
           else pc(is) ,
         dmem := if instr_kind(is) = store then
         write_dmem(dmem(is),mem_addr(is),val_b(is))
                else dmem(is) ,
         regfile := if (instr_kind(is) = load) /\ 
          ! (rf2_of(inst_id(is)) = zero_reg) then
              write_reg(regfile(is),rf2_of(inst_id(is)),
              read_dmem(dmem(is),mem_addr(is)))
          else if (instr_kind(is) = alu_immed) /\
            ! (rf2_of(inst_id(is)) = zero_reg) then
            write_reg(regfile(is),rf2_of(inst_id(is)),
            alu(alu_op_of(opcode_of(inst_id(is))),val_a(is),val_b(is)))
          else if (instr_kind(is) = alu_reg) /\
            ! (rf3_of(inst_id(is)) = zero_reg) then
            write_reg(regfile(is),rf3_of(inst_id(is)),
            alu(alu_op_of(opcode_of(inst_id(is))),val_a(is),val_b(is)))
          else regfile(is)  ]
  

%========================================================================

macro proj_state(is:state_I) : state_A = 
  {  pc = pc(is);
    regfile = regfile(is);
    dmem = dmem(is);
    imem = imem(is)
  }

macro ABS(is:state_I) : state_A = 
  proj_state(Complete_IF_ID(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is)))))


macro Inv_predicate(is : state_I) : bool =
  (bubble_ex(is) \/ (instr_class(opcode_ex(is)) = store) \/ (instr_class(opcode_ex(is)) = beqz)
    \/ (instr_class(opcode_ex(is)) = j)) --> (dest_ex(is) = zero_reg)


AXIOM Inv1: 
  (*Forall is : state_I .*) Inv_predicate(is)




%-----------
%VC1_r
CONJECTURE lemma1_regfile: 
  regfile(I_step(is,inp)) = regfile(Complete_MEM_WB(is))        

%VC1_d
CONJECTURE lemma1_dmem: 
  dmem(Complete_MEM_WB(is)) = dmem(is)

%------------
%VC2_r
CONJECTURE lemma2_regfile: 
  regfile(Complete_MEM_WB(I_step(is,inp))) = regfile(Complete_EX_MEM(Complete_MEM_WB(is)))        


%VC2_d
CONJECTURE lemma2_dmem: 
  dmem(Complete_MEM_WB(I_step(is,inp))) = dmem(Complete_EX_MEM(Complete_MEM_WB(is)))


%-------------
%VC3_r
CONJECTURE lemma3_regfile: 
  regfile(Complete_EX_MEM(Complete_MEM_WB(I_step(is,inp)))) = 
  regfile(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is))))

%VC3_d
CONJECTURE lemma3_dmem: 
  dmem(Complete_EX_MEM(Complete_MEM_WB(I_step(is,inp)))) = 
  dmem(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is))))        

%-------------
% Asserting the correctness of the feedback logic.
CONJECTURE lemma_new_operand_a: 
  ! stall_issue(is) /\ ! bubble_id(is) --> 
    new_operand_a(is) = val_a(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is))))

CONJECTURE lemma_new_operand_b: 
  ! stall_issue(is) /\ ! bubble_id(is) -->
    new_operand_b(is) = val_b(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is))))

%--------------
%VC4_r
CONJECTURE lemma4_regfile1: 
  ! stall_issue(is) --> 
    regfile(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(I_step(is,inp))))) = 
      regfile(Complete_IF_ID(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is)))))
        

%VC4_d
CONJECTURE lemma4_dmem1: 
  ! stall_issue(is) --> 
    dmem(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(I_step(is,inp))))) = 
      dmem(Complete_IF_ID(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is)))))  
      

%VC5_r
CONJECTURE lemma4_regfile2: 
  stall_issue(is) --> 
    regfile(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(I_step(is,inp))))) = 
      regfile(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is))))        

%VC5_d
CONJECTURE lemma4_dmem2: 
  stall_issue(is) --> 
    dmem(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(I_step(is,inp))))) = 
      dmem(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is))))        

%-------------------------------------------------------------------------------------------------
%VC1_i
CONJECTURE lemma_imem: 
  imem(Complete_IF_ID(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is))))) = imem(is)

%VC1_p
CONJECTURE lemma_pc1: 
  pc(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is)))) = pc(is)

%VC2_p
CONJECTURE lemma_pc2: 
  ! stall_issue(is) /\ ! branch_taken(is) -->
    pc(Complete_IF_ID(Complete_ID_EX(Complete_EX_MEM(Complete_MEM_WB(is))))) = pc(is)


%-----------------------------------------------------------------------------------
%VC6_r

CONJECTURE commutes_regfile: 
  regfile(ABS(I_step(is,inp))) =
  regfile(A_step(ABS(is),{ stall = stall(inp) \/ stall_issue(is) \/ branch_taken(is) }))
(** 
 requires 500.000 branches in 2700.0 seconds 
 **)

(**
With all previous background properties active:
verified by examining 366304 branches
dp:
        calls:  1
        usr  :  3213.3200
        sys  :  44.6600
        gc   :  16.4800
**)

%VC6_d
CONJECTURE commutes_dmem: 
  dmem(ABS(I_step(is,inp))) =
  dmem(A_step(ABS(is),{ stall = stall(inp) \/ stall_issue(is) \/ branch_taken(is) }))
(**
verified by examining 895639 branches
dp:
  calls:  1
  usr  :  2890.5700
  sys  :  118.9000
  gc   :  14.7200

With all previous background properties active:
verified by examining 253732 branches
dp:
        calls:  1
        usr  :  2144.7900
        sys  :  31.2900
        gc   :  9.0100

**)

%VC3_p
CONJECTURE commutes_pc: 
  pc(ABS(I_step(is,inp))) =
  pc(A_step(ABS(is),{ stall = stall(inp) \/ stall_issue(is) \/ branch_taken(is) }))

(**
verified by examining 69383 branches
dp:
        calls:  1
        usr  :  691.7500
        sys  :  299.6200
        gc   :  2.6100

With all previous background properties active:
verified by examining 50040 branches
dp:
        calls:  1
        usr  :  521.5100
        sys  :  6.9600
        gc   :  2.6400


 **)
%VC2_i
CONJECTURE commutes_imem: 
  imem(ABS(I_step(is,inp))) =
  imem(A_step(ABS(is),{ stall = stall(inp) \/ stall_issue(is) \/ branch_taken(is) }))

(**
verified by examining 208 branches
dp:
        calls:  1
        usr  :  6.9400
        sys  :  0.3800
        gc   :  0.0300

verified by examining 156 branches
dp:
        calls:  1
        usr  :  5.7700
        sys  :  0.0100
        gc   :  0.0400

**)
%----------------------------------------------------------------------------



CONJECTURE commutes_dlx: 
  ABS(I_step(is,inp)) =
        A_step(ABS(is),{ stall = stall(inp) \/ stall_issue(is) \/ branch_taken(is) })


(***
By using all previously proven properties as axioms:

verified by examining 927152 branches
dp:
        calls:  1
        usr  :  8962.1000
        sys  :  95.5400
        gc   :  26.9400

***)
%END verif_diag




Last modified: Sat Aug 8 18:25:09 PDT 1998