From c8261a040bf328d4d2296f0c91a85a4193195844 Mon Sep 17 00:00:00 2001 From: Warrick Lo Date: Thu, 18 Jun 2026 23:20:11 -0700 Subject: Add formal verification for regfile Successfully verifies the following requirements: * REQ-REGFILE-010 * REQ-REGFILE-020 * REQ-REGFILE-030 * REQ-REGFILE-041 * REQ-REGFILE-042 * REQ-REGFILE-043 * REQ-REGFILE-050 * REQ-REGFILE-051 * REQ-REGFILE-052 * REQ-REGFILE-053 * REQ-REGFILE-060 Verified through construction of regfile: * REQ-REGFILE-040 See-also: #14 Signed-off-by: Warrick Lo --- verif/formal/regfile/regfile.sby | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 verif/formal/regfile/regfile.sby (limited to 'verif/formal/regfile/regfile.sby') diff --git a/verif/formal/regfile/regfile.sby b/verif/formal/regfile/regfile.sby new file mode 100644 index 0000000..89f8884 --- /dev/null +++ b/verif/formal/regfile/regfile.sby @@ -0,0 +1,23 @@ +[tasks] +cover +prove + +[options] +cover: mode cover +prove: mode prove +prove: depth 20 + +[engines] +smtbmc + +[script] +read -formal -sv config_pkg.sv +read -formal -sv regfile.sv +read -formal -sv regfile_ind.sv +prep -top regfile_ind + +[files] +rtl/types.svh +rtl/config_pkg.sv +rtl/regfile.sv +verif/formal/regfile/regfile_ind.sv -- cgit v1.2.3