Skip to content

Commit

Permalink
abstract: test -state
Browse files Browse the repository at this point in the history
  • Loading branch information
@widlarizer
widlarizer committed Feb 18, 2025
1 parent 2fa7076 commit d3b3f6b
Showing 1 changed file with 98 additions and 117 deletions.
215 changes: 98 additions & 117 deletions tests/various/abstract.ys
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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);
Expand All @@ -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
# -----------------------------------------------------------------------------

0 comments on commit d3b3f6b

Please sign in to comment.