CODEWITHSUNDEEP
logicsolversat-solvers
instance
instance

Reputation: 1374

Logic equivalence of sub-signals of logically equivalent signals

I have two logic output which I know are logically equivalent (proven using SAT solvers). Now I choose same bits from both signals. Can I say since the complete signals are equivalent then sub-signals will also be equivalent?

eg. N-bit signal - Signal-1 and Signal-2 these both are logically equivalent. Now I extract 0:1 from Signal-1 and 0:1 from Signal-2, now I want to know equivalence of these two new signals. Can I surely say that these will be equivalent?

I think they will be equivalent, please let me know if I am missing something, or it can be different in any scenario.

Upvotes: 0

Views: 40

Answers (1)

alias
alias

Reputation: 30525

Think about the contrapositive. If sig1[1:0] is not equivalent to sig2[1:0] would your solver say sig1 == sig2?

By that argument, and by "standard" interpretation of equivalence on multi-bit signals, I'd say the equivalence follows. This is assuming you have a two-level logic formulation (i.e., just 0-1) and not 3- or 4-valued logic as is sometimes found in formal equivalence checking of circuits. But even in those cases, you should be able to make the contrapositive argument above.

Upvotes: 1

Related Questions