From 53a4f0fb56f298880c9b91dfa8c2e69a383cd5bc Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Thu, 23 Feb 2023 14:58:02 +0100 Subject: Add test example --- tests/verific/.gitignore | 3 +++ tests/verific/case.sv | 28 ++++++++++++++++++++++++++++ tests/verific/case.ys | 16 ++++++++++++++++ tests/verific/run-test.sh | 4 ++++ 4 files changed, 51 insertions(+) create mode 100644 tests/verific/.gitignore create mode 100644 tests/verific/case.sv create mode 100644 tests/verific/case.ys create mode 100755 tests/verific/run-test.sh diff --git a/tests/verific/.gitignore b/tests/verific/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/verific/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/verific/case.sv b/tests/verific/case.sv new file mode 100644 index 000000000..ed8529b91 --- /dev/null +++ b/tests/verific/case.sv @@ -0,0 +1,28 @@ +module top ( + input clk, + input [5:0] currentstate, + output reg [1:0] o + ); + always @ (posedge clk) + begin + case (currentstate) + 5'd1,5'd2, 5'd3: + begin + o <= 2'b01; + end + 5'd4: + begin + o <= 2'b10; + end + 5'd5,5'd6,5'd7: + begin + o <= 2'b11; + end + default : + begin + o <= 2'b00; + end + endcase + end +endmodule + diff --git a/tests/verific/case.ys b/tests/verific/case.ys new file mode 100644 index 000000000..a181b39cf --- /dev/null +++ b/tests/verific/case.ys @@ -0,0 +1,16 @@ +verific -cfg db_abstract_case_statement_synthesis 0 +read -sv case.sv +verific -import top +prep +rename top gold + +verific -cfg db_abstract_case_statement_synthesis 1 +read -sv case.sv +verific -import top +prep +rename top gate + +miter -equiv -flatten -make_assert gold gate miter +prep -top miter +clk2fflogic +sat -set-init-zero -tempinduct -prove-asserts -verify diff --git a/tests/verific/run-test.sh b/tests/verific/run-test.sh new file mode 100755 index 000000000..2f91cf0fd --- /dev/null +++ b/tests/verific/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../gen-tests-makefile.sh +run_tests --yosys-scripts --bash -- cgit v1.2.3