mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-27 02:45:52 +00:00
abstract: test -state
This commit is contained in:
Emil J. Tywoniak
parent
212224dfe8
commit
d3a90021ad
1 changed files with 97 additions and 116 deletions
|
|
@ -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
|
||||
# -----------------------------------------------------------------------------
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue