mirror of
https://github.com/YosysHQ/yosys
synced 2025-11-04 05:19:11 +00:00
73e45d29d6
The tests/verilog/*_if_enc.ys scripts instantiate simple encoder modules, both with and without the SystemVerilog priority/unique/unique0 keywords, and check for consistency between the two for the subset of inputs where the priority/unique/unique0 "if" result is well-defined. These tests vacuously succeed at the moment, since priority/unique keywords are silently ignored and therefore the generated logic is trivially identical. But the test cases will be capable of detecting certain types of unsound optimisation if priority/unique handling is introduced later.
41 lines
1.2 KiB
Text
41 lines
1.2 KiB
Text
logger -expect log "SAT proof finished - no model found: SUCCESS" 1
|
|
|
|
read_verilog -sv <<EOF
|
|
// A somewhat contrived model of an encoder, relying on SystemVerilog's
|
|
// strong "if" semantics to guarantee priority encoder behaviour.
|
|
module encoder( input [ 2:0 ] x, output reg [ 1:0 ] y );
|
|
always_comb begin
|
|
y = 2'b00;
|
|
|
|
if( x[ 2 ] ) y = 2'b11;
|
|
else if( x[ 1 ] ) y = 2'b10;
|
|
else if( x[ 0 ] ) y = 2'b01;
|
|
end
|
|
endmodule
|
|
|
|
// Almost the same thing, but by using "unique0 if" we introduce
|
|
// "don't care" states, essentially conveying permission to synthesise
|
|
// a simple encoder instead.
|
|
module dut( input [ 2:0 ] x, output reg [ 1:0 ] y );
|
|
always_comb begin
|
|
y = 2'b00;
|
|
|
|
unique0 if( x[ 2 ] ) y = 2'b11;
|
|
else if( x[ 1 ] ) y = 2'b10;
|
|
else if( x[ 0 ] ) y = 2'b01;
|
|
end
|
|
endmodule
|
|
|
|
// A simple test bench to detect mismatches between the two encoders.
|
|
module compare_encoders( input [ 2:0 ] x, output ok );
|
|
wire [ 1:0 ] encout;
|
|
wire [ 1:0 ] dutout;
|
|
encoder e( x, encout );
|
|
dut d( x, dutout );
|
|
// The "unique0 if" above assumes $onehot0( x ).
|
|
assign ok = encout == dutout || !$onehot0( x );
|
|
endmodule
|
|
EOF
|
|
|
|
synth -flatten -top compare_encoders
|
|
sat -prove ok 1
|