| // Copyright lowRISC contributors. |
| // Licensed under the Apache License, Version 2.0, see LICENSE for details. |
| // SPDX-License-Identifier: Apache-2.0 |
| // |
| // Assertions for ${dut.name}. |
| // Intended to be used with a formal tool. |
| |
| `include "prim_assert.sv" |
| |
| % if len(dut.pkgs) > 0: |
| module ${dut.name}_assert_fpv |
| % for pkg in dut.pkgs: |
| import ${pkg}; |
| % endfor |
| % if dut.params: |
| #( |
| % else: |
| ( |
| % endif |
| % else: |
| % if dut.params: |
| module ${dut.name}_assert_fpv #( |
| % else: |
| module ${dut.name}_assert_fpv ( |
| % endif |
| % endif |
| % if dut.params: |
| % for k, param in enumerate(dut.params): |
| <% comma = "" if (k == len(dut.params)-1) else "," %> ${param.style} ${param.datatype} ${param.name} =${param.value}${comma} |
| % endfor |
| ) ( |
| % endif |
| % for k, port in enumerate(dut.ports): |
| <% comma = "" if (k == len(dut.ports)-1) else "," %> input ${port.datatype} ${port.name}${comma} |
| % endfor |
| ); |
| |
| /////////////////////////////// |
| // Declarations & Parameters // |
| /////////////////////////////// |
| |
| ///////////////// |
| // Assumptions // |
| ///////////////// |
| |
| // `ASSUME(MyAssumption_M, ...) |
| |
| //////////////////////// |
| // Forward Assertions // |
| //////////////////////// |
| |
| // `ASSERT(MyFwdAssertion_A, ...) |
| |
| ///////////////////////// |
| // Backward Assertions // |
| ///////////////////////// |
| |
| // `ASSERT(MyBkwdAssertion_A, ...) |
| |
| endmodule : ${dut.name}_assert_fpv |