From d3b3f6baf6d7097bec9d6769005f2491c2835405 Mon Sep 17 00:00:00 2001
From: "Emil J. Tywoniak" <emil@tywoniak.eu>
Date: Tue, 18 Feb 2025 13:50:24 +0100
Subject: [PATCH] abstract: test -state

---
 tests/various/abstract.ys | 215 +++++++++++++++++---------------------
 1 file changed, 98 insertions(+), 117 deletions(-)

diff --git a/tests/various/abstract.ys b/tests/various/abstract.ys
index 0892ca1c4c4..30aa8eb3997 100644
--- a/tests/various/abstract.ys
+++ b/tests/various/abstract.ys
@@ -10,15 +10,59 @@ endmodule
 
 EOT
 proc
-# show -prefix before_base
+design -save half_clock
+
+# -----------------------------------------------------------------------------
+# An empty selection causes no change
+select -none
+
+logger -expect log "Abstracted 0 stateful cells" 1
+	abstract -state -enablen magic
+logger -check-expected
+
+logger -expect log "Abstracted 0 init bits" 1
+	abstract -init
+logger -check-expected
+
+logger -expect log "Abstracted 0 driver ports" 1
+	abstract -value -enablen magic
+logger -check-expected
+
+select -clear
+# -----------------------------------------------------------------------------
+design -load half_clock
+# Basic -state test
 abstract -state -enablen magic
 check -assert
-# show -prefix after_base
-
+# Connections to dff D input port
+select -set conn_to_d t:$dff %x:+[D] t:$dff %d
+# The D input port is fed with a mux
+select -set mux @conn_to_d %ci t:$mux %i
+select -assert-count 1 @mux
+# The S input port is fed with the magic wire
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# The A input port is fed with an anyseq
+select -assert-count 1 @mux %x:+[A] %ci t:$anyseq %i
+# The B input port is fed with the negated Q
+select -set not @mux %x:+[B] %ci t:$not %i
+select -assert-count 1 @not %x:+[A] o:Q %i
+
+design -load half_clock
+# Same thing, inverted polarity
+abstract -state -enable magic
+check -assert
+select -set conn_to_d t:$dff %x:+[D] t:$dff %d
+select -set mux @conn_to_d %ci t:$mux %i
+select -assert-count 1 @mux
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# so we get swapped A and B
+select -assert-count 1 @mux %x:+[B] %ci t:$anyseq %i
+select -set not @mux %x:+[A] %ci t:$not %i
+select -assert-count 1 @not %x:+[A] o:Q %i
+# -----------------------------------------------------------------------------
 design -reset
 read_verilog <<EOT
-
-module fff (CLK, DDD, QQQ, Q, magic);
+module wide_flop (CLK, DDD, QQQ, Q, magic);
 	input CLK;
 	input [2:0] DDD;
 	output reg [2:0] QQQ;
@@ -28,14 +72,26 @@ module fff (CLK, DDD, QQQ, Q, magic);
 		QQQ <= DDD;
 	assign Q = QQQ[0];
 endmodule
-
 EOT
 proc
-# show -prefix before_wide
+design -save wide_flop
+# Test that abstracting an output slice muxes an input slice
 abstract -state -enablen magic w:Q
-# show -prefix after_wide
 check -assert
-
+# Connections to dff D input port
+select -set conn_to_d t:$dff %x:+[D] t:$dff %d
+# The D input port is partially fed with a mux
+select -set mux @conn_to_d %ci t:$mux %i
+select -assert-count 1 @mux
+# and also the DDD input
+select -assert-count 1 @conn_to_d w:DDD %i
+# The S input port is fed with the magic wire
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# The A input port is fed with an anyseq
+select -assert-count 1 @mux %x:+[A] %ci t:$anyseq %i
+# The B input port is fed with DDD
+select -assert-count 1 @mux %x:+[B] %ci w:DDD %i
+# -----------------------------------------------------------------------------
 design -reset
 read_verilog <<EOT
 module half_clock_en (CLK, E, Q, magic);
@@ -48,122 +104,47 @@ module half_clock_en (CLK, E, Q, magic);
             Q <= ~Q;
 endmodule
 EOT
-
 proc
 opt_expr
 opt_dff
-# show -prefix before_en
+design -save half_clock_en
+# Test that abstracting a $dffe unmaps the enable
+select -assert-count 1 t:$dffe
 abstract -state -enablen magic
 check -assert
-# show -prefix after_en
-
+select -assert-count 0 t:$dffe
+select -assert-count 1 t:$dff
+# -----------------------------------------------------------------------------
 design -reset
 read_verilog <<EOT
-module half_clock (CLK, Q);
+module top (CLK, E, Q, Q_EN);
 	input CLK;
-	output reg Q = 1'b1;
-	always @(posedge CLK)
-		Q <= ~Q;
-endmodule
-EOT
-
-proc
-opt_expr
-opt_dff
-dump
-select -none
-abstract -init
-select -clear
-check -assert
-# dump
-
-design -reset
-read_verilog <<EOT
-module main (input [3:0] baz);
-  reg foo;
-  reg bar;
-  assign foo = bar;
-  assign bar = baz[0];
-  reg aaa = 1'b1;
-  always @(posedge bar)
-  	aaa <= ~aaa;
-endmodule
-EOT
-
-proc -noopt
-# show -prefix before_init
-dump
-select -none
-abstract -init
-select -clear
-# show -prefix after_init
-dump
-check -assert
-# dump
-
-
-design -reset
-read_verilog <<EOT
-module this_adff (CLK, ARST, D, Q, magic);
-
-parameter WIDTH = 2;
-parameter CLK_POLARITY = 1'b1;
-parameter ARST_POLARITY = 1'b1;
-parameter ARST_VALUE = 0;
-
-input CLK, ARST, magic;
-input [WIDTH-1:0] D;
-output reg [WIDTH-1:0] Q;
-wire pos_clk = CLK == CLK_POLARITY;
-wire pos_arst = ARST == ARST_POLARITY;
-
-always @(posedge pos_clk, posedge pos_arst) begin
-	if (pos_arst)
-		Q <= ARST_VALUE;
-	else
-		Q <= D;
-end
-
-endmodule
-EOT
-
-proc
-opt_expr
-opt_dff
-# show -prefix before_a
-abstract -state -enablen magic
-check -assert
-# show -prefix after_a
-# opt_clean
-
-design -reset
-read_verilog <<EOT
-module this_adff (CLK, ARST, D, Q, magic);
-
-parameter WIDTH = 2;
-parameter CLK_POLARITY = 1'b1;
-parameter ARST_POLARITY = 1'b1;
-parameter ARST_VALUE = 0;
-
-input CLK, ARST, magic;
-input [WIDTH-1:0] D;
-output reg [WIDTH-1:0] Q;
-wire pos_clk = CLK == CLK_POLARITY;
-wire pos_arst = ARST == ARST_POLARITY;
-
-always @(posedge pos_clk, posedge pos_arst) begin
-	if (pos_arst)
-		Q <= ARST_VALUE;
-	else
-		Q <= D;
-end
-
+	input E;
+	output reg Q;
+	output reg Q_EN;
+	half_clock uut (CLK, Q, 1'b0);
+	half_clock_en uut_en (CLK, E, Q_EN, 1'b0);
 endmodule
 EOT
 proc
-# show -prefix before_value
-abstract -value -enablen magic
-check -assert
-clean
-# show -prefix after_value
-# dump
+design -import half_clock
+design -import half_clock_en
+hierarchy -check -top top
+# Test when the abstraction is disabled (enable is inactive),
+# the equivalence is preserved
+rename top top_gold
+design -save gold
+abstract -state -enable magic half_clock half_clock_en
+flatten
+rename top_gold top_gate
+design -save gate
+design -load gold
+flatten
+design -import gate -as top_gate
+
+equiv_make top_gold top_gate equiv
+equiv_induct equiv
+equiv_status -assert equiv
+# The reader may verify that this model checking is functional
+# by changing -enable to -enablen in the abstract pass invocation above
+# -----------------------------------------------------------------------------