Replaced headers in assume and bind files with the ones in formal dir…

…. Uncommented the row4 trigger_match_i assertion from controller_assert file
openhwgroup · Jun 17, 2024 · 4951be4 · 4951be4
1 parent f700261
commit 4951be4
Show file tree

Hide file tree

Showing 4 changed files with 74 additions and 5 deletions.
diff --git a/scripts/formal/src/cv32e40p_controller_assert.sv b/scripts/formal/src/cv32e40p_controller_assert.sv
@@ -67,8 +67,8 @@ module cv32e40p_controller_assert import cv32e40p_pkg::*;
     assert_all_true_ctrl_1187_1189_and_1191: assert property(all_true_ctrl_1187_1189_and_1191);
     assert_all_true_ctrl_1210_and_1212 : assert property(all_true_ctrl_1210_and_1212);
     //This one is inconclusive with questa formal. To avoid long run keep it disabled
-    // assert_unreachable_ctrl_1241_row_4 : assert property(unreachable_ctrl_1241_row_4);
+     assert_unreachable_ctrl_1241_row_4 : assert property(unreachable_ctrl_1241_row_4);
     assert_unreachable_ctrl_1241_row_5 : assert property(unreachable_ctrl_1241_row_5);
     assert_unreachable_ctrl_1241_row_10: assert property(unreachable_ctrl_1241_row_10);
 
-endmodule
+endmodule
diff --git a/scripts/slec/tb_src/cv32e40p_bind2.sv b/scripts/slec/tb_src/cv32e40p_bind2.sv
@@ -1,5 +1,28 @@
-// Copyright 2024 Cirrus Logic
+// 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>         //
+//               Pascal Gouedo, Dolphin Design <pascal.gouedo@dolphin.fr>         //
+//                                                                                //
+// Description:  CV32E40P binding for formal code analysis                        //
+//                                                                                //
+////////////////////////////////////////////////////////////////////////////////////
+
 bind cv32e40p_top insn_assert u_insn_assert (
     .clk_i(clk_i),
     .rst_ni(rst_ni),

diff --git a/scripts/slec/tb_src/data_assert2.sv b/scripts/slec/tb_src/data_assert2.sv
@@ -1,5 +1,28 @@
-// Copyright 2024 Cirrus Logic
+// 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>         //
+//               Pascal Gouedo, Dolphin Design <pascal.gouedo@dolphin.fr>         //
+//                                                                                //
+// Description:  OBI protocol emulation for CV32E40P data interface               //
+//                                                                                //
+////////////////////////////////////////////////////////////////////////////////////
+
 module data_assert (
     input logic clk_i,
     input logic rst_ni,

diff --git a/scripts/slec/tb_src/insn_assert2.sv b/scripts/slec/tb_src/insn_assert2.sv
@@ -1,5 +1,28 @@
-// Copyright 2024 Cirrus Logic
+// 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>         //
+//               Pascal Gouedo, Dolphin Design <pascal.gouedo@dolphin.fr>         //
+//                                                                                //
+// Description:  OBI protocol emulation for CV32E40P data interface               //
+//                                                                                //
+////////////////////////////////////////////////////////////////////////////////////
+
 module insn_assert (
     input logic clk_i,
     input logic rst_ni,