Allow specifying leaf filenames using the 'set filename=' directive. …

…Add a template 'formal' project

src/vte/__main__.py

@@ -87,8 +87,18 @@ def generate(args, parameters, rgy):
             tmpl_e = env.get_template(tmpl)
 
             filename = substitute(global_vars, tmpl_e.name)
+            file_dir = os.path.dirname(filename)
             try:
-                filename = tmpl_e.module.filename;
+                filename_u = tmpl_e.module.filename
+
+                if filename_u.find("/") != -1:
+                    # User has specified a relative path, so we assume 
+                    # this is relative to the output directory
+                    filename = filename_u
+                else:
+                    # Just a simple filename, so we assume it is relative
+                    # to the template file
+                    filename = file_dir + "/" + filename_u
             except:
                 pass
 
@@ -105,8 +115,20 @@ def generate(args, parameters, rgy):
         tmpl_e = env.get_template(tmpl)
 
         filename = substitute(global_vars, tmpl_e.name)
+        file_dir = os.path.dirname(filename)
         try:
             filename = tmpl_e.module.filename;
+
+            filename_u = tmpl_e.module.filename
+
+            if filename_u.find("/") != -1:
+                # User has specified a relative path, so we assume 
+                # this is relative to the output directory
+                filename = filename_u
+            else:
+                # Just a simple filename, so we assume it is relative
+                # to the template file
+                filename = file_dir + "/" + filename_u
         except:
             pass
 

templates/verif/ip/formal/.vte

@@ -0,0 +1,11 @@
+
+[template]
+desc = IP verification environment using formal verification
+
+[parameter:sim]
+desc = Default simulator for the project
+default = vl
+
+[parameter:top]
+desc = Specifies the top-level module
+default = 10

templates/verif/ip/formal/formal/scripts/Makefile

@@ -0,0 +1,34 @@
+#****************************************************************************
+#* {{name}} Makefile
+#****************************************************************************
+include $(PACKAGES_DIR)/packages.mk
+include $(PACKAGES_DIR)/simscripts/mkfiles/plusargs.mk
+
+RUN_TARGETS += run-sby
+CHECKER=$(call get_plusarg,CHECKER,$(PLUSARGS))
+DEPTH=$(call get_plusarg,DEPTH,$(PLUSARGS))
+
+ifeq (,$(DEPTH))
+DEPTH=32
+endif
+
+include $(PACKAGES_DIR)/simscripts/mkfiles/common_sim.mk
+
+
+ifeq (true,$(QUIET))
+REDIRECT= >simx.log 2>&1
+else
+REDIRECT= | tee simx.log 2>&1
+endif
+
+VE_DIR := $(abspath $(SIM_DIR)/..)
+
+# List of variables to substitute in the .sby file
+SBY_VARS += CHECKER TESTNAME DEPTH VE_DIR
+
+run-sby :
+	$(Q)sed $(SIM_DIR)/scripts/{{name}}.sby \
+		$(foreach v,$(SBY_VARS),-e 's%{$(v)}%$($(v))%g') > {{name}}.sby
+	$(Q)sby -f {{name}}.sby $(REDIRECT)
+
+include $(PACKAGES_DIR)/packages.mk

templates/verif/ip/formal/formal/scripts/formal.sby

@@ -0,0 +1,30 @@
+#****************************************************************************
+#* {{name}}.sby
+#*
+#* Formal template script 
+#****************************************************************************
+{% set filename = "{{name}}.sby" %}
+
+[options]
+mode bmc
+depth {DEPTH}
+
+[engines]
+smtbmc boolector
+
+[script]
+# TODO: add in RTL files
+read -sv -formal \
+{{name}}_checker.sv \
+{{name}}_test.sv \
+{{name}}_tb.sv
+prep -top {{name}}_tb
+
+[files]
+# TODO: add in RTL files
+
+{VE_DIR}/tb/{{name}}_tb.sv
+{{name}}_checker.sv {VE_DIR}/tb/{CHECKER}.sv
+{{name}}_test.sv {VE_DIR}/tests/{TESTNAME}_test.sv
+
+

templates/verif/ip/formal/formal/scripts/status.sh

@@ -0,0 +1,24 @@
+#!/bin/sh
+#****************************************************************************
+#* status.sh
+#****************************************************************************
+{% set chmod = "+x" %}
+
+testname=$1
+seed=$2
+
+if test ! -f simx.log; then
+  echo "FAIL: $testname - no simx.log"
+else
+  n_passed=`grep "^SBY" simx.log | grep 'DONE (PASS' | wc -l`
+  n_failed=`grep "^SBY" simx.log | grep 'DONE (FAIL' | wc -l`
+
+  if test $n_passed -eq 1 && test $n_failed -eq 0; then
+    echo "PASSED: $testname"
+  elif test $n_failed -ne 0; then
+    echo "FAILED: $testname ($n_failed)"
+  else
+    echo "FAILED: $testname ($n_passed $n_failed)"
+  fi
+fi
+

templates/verif/ip/formal/formal/testlists/all.f

@@ -0,0 +1,11 @@
+
+{% set filename = "{{name}}_all.f" %}
+
+tests/{{name}}_smoke.f
+tests/fwrisc_mul_div_shift_formal_sra.f
+tests/fwrisc_mul_div_shift_formal_srl.f
+tests/fwrisc_mul_div_shift_formal_mul.f
+tests/fwrisc_mul_div_shift_formal_mulh.f
+tests/fwrisc_mul_div_shift_formal_muls.f
+tests/fwrisc_mul_div_shift_formal_mulsh.f
+

templates/verif/ip/formal/formal/tests/smoke.f

@@ -0,0 +1,5 @@
+
+{% set filename = "{{name}}_smoke.f" %}
+
++CHECKER={{name}}_smoke_checker
+

templates/verif/ip/formal/tb/smoke_checker.sv

@@ -0,0 +1,9 @@
+
+{% set filename = "{{name}}_smoke_checker.sv" %}
+
+module {{name}}_checker(
+		// TODO: fill in port list
+		);
+
+endmodule
+

templates/verif/ip/formal/tb/tb.sv

@@ -0,0 +1,36 @@
+/****************************************************************************
+ * {{name}}_tb.sv
+ ****************************************************************************/
+{% set filename = "{{name}}_tb.sv" %}
+
+/**
+ * Module: {{name}}_tb
+ * 
+ * TODO: Add module documentation
+ */
+module {{name}}_tb(input clock);
+
+	reg[3:0]	reset_cnt = 0;
+	reg 		reset = 1;
+
+	always @(posedge clock) begin
+		if (reset_cnt == 1) begin
+			reset <= 0;
+		end else begin
+			reset_cnt <= reset_cnt + 1;
+		end
+	end
+
+	// TODO: instance checker, test, and DUT
+
+	{{name}}_test u_test(
+			);
+
+	// TODO: instance DUT
+
+	{{name}}_checker u_checker(
+		);
+
+endmodule
+
+

templates/verif/ip/formal/tests/smoke_test.sv

@@ -0,0 +1,9 @@
+
+{% set filename = "{{name}}_smoke_test.sv" %}
+
+module {{name}}_test(
+		// TODO: specify portlist
+		);
+
+
+endmodule