Logi c эквивалентность суб-сигналов логически эквивалентных сигналов

Question

У меня есть два логических c вывода, которые, как я знаю, логически эквивалентны (доказано с использованием SAT-решателей). Теперь я выбираю одинаковые биты из обоих сигналов. Могу ли я сказать, поскольку полные сигналы эквивалентны, тогда суб-сигналы также будут эквивалентны?

например. N-битный сигнал - Сигнал-1 и Сигнал-2 оба они логически эквивалентны. Теперь я извлекаю 0: 1 из Сигнала-1 и 0: 1 из Сигнала-2, теперь я хочу узнать эквивалентность этих двух новых сигналов. Могу ли я с уверенностью сказать, что они будут эквивалентными ?

Я думаю, что они будут эквивалентными, пожалуйста, дайте мне знать, если я что-то упустил, или это может отличаться в любом сценарии.

Answer 1

Подумайте о противозачаточных средствах. Если sig1[1:0] равно , а не эквивалентно sig2[1:0], ваш решатель скажет sig1 == sig2?

По этому аргументу и по "стандартной" интерпретации эквивалентности для многобитовых сигналов, я сказал бы, эквивалентность следует. Это предполагает, что у вас есть двухуровневая логика c (т. Е. Просто 0-1), а не 3- или 4-значная логика c, как это иногда бывает при формальной проверке эквивалентности цепей. Но даже в этих случаях вы должны быть в состоянии привести противоположный аргумент выше.