Add test example

This commit is contained in:
Miodrag Milanovic 2023-02-23 14:58:02 +01:00
parent a30894e5fa
commit 53a4f0fb56
4 changed files with 51 additions and 0 deletions

3
tests/verific/.gitignore vendored Normal file
View File

@ -0,0 +1,3 @@
/*.log
/*.out
/run-test.mk

28
tests/verific/case.sv Normal file
View File

@ -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

16
tests/verific/case.ys Normal file
View File

@ -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

4
tests/verific/run-test.sh Executable file
View File

@ -0,0 +1,4 @@
#!/usr/bin/env bash
set -eu
source ../gen-tests-makefile.sh
run_tests --yosys-scripts --bash