Loading files
This file is pinned to the selected release. Download the original to open it in your design tool.
// Copyright 2024 Dolphin Design
// SPDX-License-Identifier: Apache-2.0 WITH SHL-2.1
//
// Licensed under the Solderpad Hardware License v 2.1 (the "License");
// you may not use this file except in compliance with the License, or,
// at your option, the Apache License version 2.0.
// You may obtain a copy of the License at
//
// https://solderpad.org/licenses/SHL-2.1/
//
// Unless required by applicable law or agreed to in writing, any work
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
////////////////////////////////////////////////////////////////////////////////////
// //
// Contributors: Yoann Pruvost, Dolphin Design <yoann.pruvost@dolphin.fr> //
// //
// Description: OBI protocol emulation for CV32E40P instruction interface //
// //
////////////////////////////////////////////////////////////////////////////////////
module insn_assert (
input logic clk_i,
input logic rst_ni,
// Instruction memory interface
input logic instr_req_o,
input logic instr_gnt_i,
input logic instr_rvalid_i,
input logic [31:0] instr_addr_o,
input logic [31:0] instr_rdata_i
);
import cv32e40p_pkg::*;
import cv32e40p_tracer_pkg::*;
/*****************
* Helpers logic *
*****************/
int s_outstanding_cnt;
always_ff @(posedge clk_i or negedge rst_ni) begin
if(!rst_ni) begin
s_outstanding_cnt <= 0;
end else if (instr_req_o & instr_gnt_i & instr_rvalid_i) begin
s_outstanding_cnt <= s_outstanding_cnt;
end else if (instr_req_o & instr_gnt_i) begin
s_outstanding_cnt <= s_outstanding_cnt + 1;
end else if (instr_rvalid_i) begin
s_outstanding_cnt <= s_outstanding_cnt - 1;
end
end
logic [31:0] s_prev_insn;
always_ff @(posedge clk_i or negedge rst_ni) begin
if(!rst_ni) begin
s_prev_insn <= '0;
end else if (instr_rvalid_i) begin
s_prev_insn <= instr_rdata_i;
end
end
/**********
* Assume *
**********/
// Concerning lint_grnt
property no_grnt_when_no_req;
@(posedge clk_i) disable iff(!rst_ni)
!instr_req_o |-> !instr_gnt_i;
endproperty
property no_rvalid_if_no_pending_req;
@(posedge clk_i) disable iff(!rst_ni)
s_outstanding_cnt < 1 |-> !instr_rvalid_i;
endproperty
property no_compressed;
@(posedge clk_i) disable iff(!rst_ni)
instr_rdata_i[1:0] == 2'b11;
endproperty
property no_jump;
@(posedge clk_i) disable iff(!rst_ni)
(instr_rdata_i[6:0] != OPCODE_JAL) & (instr_rdata_i[6:0] != OPCODE_JALR);
endproperty
property no_branch;
@(posedge clk_i) disable iff(!rst_ni)
instr_rdata_i[6:0] != OPCODE_BRANCH;
endproperty
property no_custom0;
@(posedge clk_i) disable iff(!rst_ni)
instr_rdata_i[6:0] != OPCODE_CUSTOM_0;
endproperty
property cvend0_only_after_cvstart0;
@(posedge clk_i) disable iff(!rst_ni)
(s_prev_insn != INSTR_CVSTARTI0) & (s_prev_insn != INSTR_CVSTARTI0) |-> (instr_rdata_i != INSTR_CVSENDI0) & (instr_rdata_i != INSTR_CVEND0);
endproperty
property cvcount0_only_after_cvend0;
@(posedge clk_i) disable iff(!rst_ni)
(s_prev_insn != INSTR_CVSENDI0) & (s_prev_insn != INSTR_CVEND0) |-> (instr_rdata_i != INSTR_CVCOUNTI0) & (instr_rdata_i != INSTR_CVCOUNT0);
endproperty
property no_cvsetup0;
@(posedge clk_i) disable iff(!rst_ni)
(instr_rdata_i != INSTR_CVSETUPI0) & (instr_rdata_i != INSTR_CVSETUP0);
endproperty
property no_cvstart0;
@(posedge clk_i) disable iff(!rst_ni)
(instr_rdata_i != INSTR_CVSTARTI0) & (instr_rdata_i != INSTR_CVSTART0);
endproperty
property cvend1_only_after_cvstart1;
@(posedge clk_i) disable iff(!rst_ni)
(s_prev_insn != INSTR_CVSTARTI1) & (s_prev_insn != INSTR_CVSTARTI1) |-> (instr_rdata_i != INSTR_CVSENDI1) & (instr_rdata_i != INSTR_CVEND1);
endproperty
property cvcount1_only_after_cvend1;
@(posedge clk_i) disable iff(!rst_ni)
(s_prev_insn != INSTR_CVSENDI1) & (s_prev_insn != INSTR_CVEND1) |-> (instr_rdata_i != INSTR_CVCOUNTI1) & (instr_rdata_i != INSTR_CVCOUNT1);
endproperty
property no_cvsetup1;
@(posedge clk_i) disable iff(!rst_ni)
(instr_rdata_i != INSTR_CVSETUPI1) & (instr_rdata_i != INSTR_CVSETUP1);
endproperty
property no_cvstart1;
@(posedge clk_i) disable iff(!rst_ni)
(instr_rdata_i != INSTR_CVSTARTI1) & (instr_rdata_i != INSTR_CVSTART1);
endproperty
property no_csr_write_to_hwloop;
@(posedge clk_i) disable iff(!rst_ni)
instr_rdata_i[6:0] == OPCODE_SYSTEM |-> (instr_rdata_i[31:20] != 12'hCC0) & (instr_rdata_i[31:20] != 12'hCC1) & (instr_rdata_i[31:20] != 12'hCC2) & (instr_rdata_i[31:20] != 12'hCC4) & (instr_rdata_i[31:20] != 12'hCC5) & (instr_rdata_i[31:20] != 12'hCC6);
endproperty
assume_no_grnt_when_no_req: assume property(no_grnt_when_no_req);
assume_no_rvalid_if_no_pending_req: assume property(no_rvalid_if_no_pending_req);
// assume_no_compressed: assume property(no_compressed);
// assume_no_jump: assume property(no_jump);
// assume_no_branch: assume property(no_branch);
// assume_no_custom0: assume property(no_custom0);
//hwloop 0 constraints
// assume_cvend0_only_after_cvstart0: assume property(cvend0_only_after_cvstart0);
// assume_cvcount0_only_after_cvend0: assume property(cvcount0_only_after_cvend0);
// assume_no_cvsetup0: assume property(no_cvsetup0);
// assume_no_cvstart0: assume property(no_cvstart0); //This one disables all hwloop0
//hwloop 1 constraints
// assume_cvend1_only_after_cvstart1: assume property(cvend1_only_after_cvstart1);
// assume_cvcount1_only_after_cvend1: assume property(cvcount1_only_after_cvend1);
// assume_no_cvsetup1: assume property(no_cvsetup1);
// assume_no_cvstart1: assume property(no_cvstart1); //This one disables all hwloop1
assume_no_csr_write_to_hwloop: assume property(no_csr_write_to_hwloop);
endmodule6033d2b1bThis file is pinned to the selected release. Download the original to open it in your design tool.