Skip to content

Commit

Permalink
WIP: Formal workaround
Browse files Browse the repository at this point in the history
  • Loading branch information
olofk committed Sep 13, 2023
1 parent d2738c6 commit 0eef880
Showing 1 changed file with 14 additions and 0 deletions.
14 changes: 14 additions & 0 deletions rtl/serv_decode.v
Original file line number Diff line number Diff line change
Expand Up @@ -146,6 +146,20 @@ module serv_decode
//and mret (!op21)
wire co_e_op = opcode[4] & opcode[2] & !op21 & !(|funct3);

`ifdef RISCV_FORMAL
/*
SERV makes no guarantees to handle illegal instructions
Instead of adding more complexity to the decoder, we add
these assumptions ensure that no illegal instructions
generated by riscv-formal
are identified as mret or e_op instructions.
*/
always @(posedge clk) begin
assume(co_ctrl_mret == 1'b0);
assume(co_e_op == 1'b0);
end
`endif

//opcode & funct3 & imm30

wire co_bufreg_sh_signed = imm30;
Expand Down

0 comments on commit 0eef880

Please sign in to comment.