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