Add verific/opers/{sel_mux,wide_mux}

Signed-off-by: Clifford Wolf <clifford@clifford.at>

verific/opers/.gitignore

+*.status
+*.log

verific/opers/Makefile

+TESTS := wide_mux sel_mux
+
+all: $(addsuffix .status,$(TESTS))
+
+%.status: %.sv run.sh
+	bash run.sh $(basename $@)
+
+clean:
+	rm -f $(addsuffix .log,$(TESTS))
+	rm -f $(addsuffix .status,$(TESTS))
+
+.PHONY: all clean

verific/opers/run.sh

+#!/bin/bash
+
+set -ex
+trap "echo FAIL > $1.status" ERR
+
+yosys -l $1.log -p "
+	verific -sv $1.sv
+	verific -import -v top
+	synth -flatten -top top
+	design -stash A
+
+	verific -sv $1.sv
+	verific -import -gates -flatten top
+	synth -flatten -top top
+	design -stash B
+
+	design -copy-from A -as A top
+	design -copy-from B -as B top
+	miter -equiv -flatten A B miter
+	sat -verify -prove trigger 0 miter
+"
+
+echo PASS > $1.status
+

verific/opers/sel_mux.sv

+module top (input [2:0] s, input [7:0] a, output y);
+  assign y = a[s];
+endmodule

verific/opers/wide_mux.sv

+module top (input [1:0] s, input [7:0] a, b, c, d, output reg [7:0] y);
+  always @* begin
+    case (s)
+      0: y = a;
+      1: y = b;
+      2: y = c;
+      3: y = d;
+    endcase
+  end
+endmodule